Tableaux
Resolución de Tableaux
Resolucin de Tableaux(Lgica proposicional)
El objetivo de este proyecto es resolver un tableaux semntico de lgica proposicional(L0)
NDICE:
- Estructura del proyecto
- Descarga y uso bsico
- Nota importante
- Cmo escribir expresiones
- Configuracin adicional
- La salida
- Compilando
- Ejemplos
- Implementacin
- Compilado con
- Notas
Estructura del proyecto
doc.pdf
flex.supp
Makefile
pruebas
1-16
complejas
1-11
README.md
src
common
basename.h
Controlador.h
Formula.c
Formula.h
Global.c
Global.h
grammar.y
SVG.c
SVG.h
Tree.c
Tree.h
unix
basename.c
Config.c
Config.h
Controlador.c
Fuente.h
lex.l
main.c
windows
basename.c
Controlador.c
Fuente.h
lex.l
main.c
Descarga y uso bsico
Para descargar el software, ve a releases(pulsando en la parte de arriba en github, o yendo aqui). Si quieres compilarlo t mismo, puedes echarle un vistazo al apartado de Haciendo pruebas
Para ejecutar el programa, es necesario siempre pasarle un fichero cualquiera(fichero de configuracin) como parmetro donde se incluya, al menos, una expresin, aunque tambin puede usarse para escribir operadores personalizados y otras opciones extra de configuracin.
Por ejemplo,
./tableaux prueba
donde prueba es el fichero en el que est la expresin. Para ver cmo escribir dicha expresin, ve al apartado Cmo escribir expresiones
Nota importante
En esta gua se habla de fichero de configuracin. Dicho fichero, incluye tanto la expresin o frmula, como la configuracin adicional. Dicha configuracin, por motivos de implementacin, no puede usarse desde Windows. Cualquier intento provocar un error.
Cmo escribir expresiones
En el fichero de configuracin hay que escribir la expresin lgica(en la ltima lnea) que se quiera resolver. Para esto, existen dos opciones; Es posible utilizar expresiones personalizadas, mediante el uso del fichero de configuracin, o usar las expresiones por defecto. A continuacin se detallan las dos opciones, siendo el primer punto para aquellas cuestiones que son comunes para ambas.
- Expresiones comunes a ambas formas
Los atomos deben especificarse mediante cualquier letra, siempre y cuando sea solo una y en minscula. El separador permite separar la expresin en distintas frmulas, mientras que los parntesis permiten modificar el orden y la asociatividad y las llaves delimitan el conjunto(con el mismo significado que los parntesis). Dichos operadores, cuya sintaxis se detalla, no pueden modificarse:
| Operador | Sintaxis |
|---|---|
| Parentesis Izq | ) |
| Parentesis Der | ( |
| Parentesis Der | { |
| Parentesis Der | } |
| Separador | , |
- Expresiones personalizadas
Para especificar los operadores de forma persoanlizada, es necesario seguir el siguiente esquema:
OPERADOR = operador_personalizado
Por ejemplo, si quisieramos cambiar el operador AND, sera:
and = ^
De esta forma, cuando en la expresin aparezca '^' se entiende que es un and lgico. Los espacios entre OPERADOR y operador_personalizado son opcionales. Para especificar los operadores, hay que seguir la sintaxis que se detalla en la siguiente tabla
| Operador | Sintaxis |
|---|---|
| AND | and |
| OR | or |
| NOT | not |
| Implicacin | imp |
| Doble Implicacin | dimp |
Dicho esto, una especificacin completa y correcta sera una como la siguiente:
and = ^
or = |
not = ~
imp = ->
dimp = <->
a ^ ~(b | c <-> a)
Es decir, la ltima lnea es la frmula en s, mientras que lo de arriba es la especificacin de los operadores. Estos siempre debern escribirse as pues no pueden modificarse(Los espacios que hay entre lneas no afectan en nada al funcionamiento)
- Expresiones predeterminadas
En la tabla anterior puede verse tambin como escribir cada operador. En este caso, la misma expresin del apartado anterior, en este caso sera:
a and not(b or c dimp a)
Configuracin adicional
Es posible especificar otras opciones de configuracin, como son:
| Opcin | Sintaxis |
|---|---|
| stdout=(yes|no) | Mediante yes se le dice al programa que siempre muestre el rbol resultado por la salida estndar(por terminal) mientras que no fuerza a no mostrar el rbol(por defecto, yes
|
| svg=(yes|no) | Igual que la opcin stdout, pero para el fichero SVG(por defecto yes) |
| svg_name=nombre | Especifica el nombre del fichero SVG generado (por defecto el nombre del fichero de entrada-sol.svg(p e.j prueba1-sol.svg) |
Entonces, un fichero de configuracin completo, con todas las opciones, sera uno como el siguiente:
and = ^
or = |
not = ~
imp = ->
dimp = <->
stdout=no
svg=yes
svg_name=salida.svg
a ^ ~(b | c <-> a)
en el que estamos expresando que no queremos que se muestre el rbol por la salida estndar, que genere siempre un svg cuyo nombre sea salida.svg
La salida
A partir de la frmula inicial, el programa mostrar una salida(un rbol en cualquier caso), que saldr por:
- La salida estndar(terminal)
Si el programa considera que el rbol generado cabe en la terminal en un tamao razonable, lo imprimir, en caso contrario, no lo har(excepto si se ha usado una opcin de configuracin que fuerze a hacerlo)
- Fichero SVG
Se genera siempre(excepto si se ha usado una opcin de configuracin que fuerze a no hacerlo)un fichero SVG donde se encuentra el rbol dibujado. Dicho fichero puede visualizarse con cualquier navegador, o mediante un visor de imgenes
Compilando
Para compilar el proyecto es necesario tener ciertas cosas instaladas, como se detalla unas cuantas secciones ms abajo, en Compilado con. Para descargar el proyecto, puedes hacerlo desde la propia pgina web, o mediante git, con:
git clone https://github.com/Dr-Noob/Logica
Una vez dentro del directorio del proyecto, que incluye un makefile, es suficiente con ejecutar
make
Esto genera un fichero ejecutable llamado 'tableaux'(si todo ha ido bien) Suponiendo que el fichero de configuracin se llama 'ejemplo':
./tableaux ejemplo
Resolvera la frmula escrita en el fichero. Si la expresin no es correcta, se avisar con un mensaje de error. Los nodos hoja en rojo son nodos cerrados, mientras que los verdes son nodos abiertos.
Ejemplos
A continuacin se muestran unos cuantos ejemplos de cmo es el rbol por la salida estndar;
La expresin
not(p dimp a),a or s,not a
genera
~(p <-> a)(a v s)(~a)
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
~(p -> a)(a v s)(~a) ~(a -> p)(a v s)(~a)
| |
(p)(~a)(a v s)(~a) (a)(~p)(a v s)(~a)
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
(p)(~a)(a)(~a) (p)(~a)(s)(~a) (a)(~p)(a)(~a) (a)(~p)(s)(~a)
La expresin
p imp q,q imp p and r,p imp (p imp q) imp r
genera
(p -> q)(q -> (p ^ r))((p -> (p -> q)) -> r)
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
/ \
(~p)(q -> (p ^ r))((p -> (p -> q)) -> r) (q)(q -> (p ^ r))((p -> (p -> q)) -> r)
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ / \
/ \ (q)(~q)((p -> (p -> q)) -> r) (q)(p ^ r)((p -> (p -> q)) -> r)
(~p)(~q)((p -> (p -> q)) -> r) (~p)(p ^ r)((p -> (p -> q)) -> r) / \ |
/ \ | / \ (q)(p)(r)((p -> (p -> q)) -> r)
/ \ (~p)(p)(r)((p -> (p -> q)) -> r) / \ / \
/ \ / \ / \ / \
/ \ / \ / \ / \
/ \ / \ / \ / \
/ \ / \ / \ / \
/ \ / \ / \ / \
/ \ / \ / \ / \
/ \ / \ (q)(~q)~(p -> (p -> q)) (q)(~q)(r) / \
(~p)(~q)~(p -> (p -> q)) (~p)(~q)(r) / \ | / \
| / \ (q)(~q)(p)~(p -> q) / \
(~p)(~q)(p)~(p -> q) / \ | (q)(p)(r)~(p -> (p -> q)) (q)(p)(r)(r)
| (~p)(p)(r)~(p -> (p -> q)) (~p)(p)(r)(r) (q)(~q)(p)(p)(~q) |
(~p)(~q)(p)(p)(~q) | (q)(p)(r)(p)~(p -> q)
(~p)(p)(r)(p)~(p -> q) |
| (q)(p)(r)(p)(p)(~q)
(~p)(p)(r)(p)(p)(~q)
Implementacin
Debido a distintos factores, se ha dividido el desarrollo entre Windows y Unix. De forma resumida:
- Los cdigos escape ANSI no estn soportados por la terminal en
Windowspor defecto en todas las versiones, mientras que s sucede(en la mayora) enUnix(LinuxyMacOS) - Ciertas funciones son dependientes de cada plataforma(
basenameenUnix/_splitpathenWindows) - Para analizar el fichero de configuracin, se usan expresiones regulares, con ayuda de
regex.hpara C. Dicha cabecera no se encuentra de forma sencilla en una instalacin deWindows
Una gua ms en detalle de la implementacin puede encontrarse en este pdf, aunque ciertos detalles pueden quedarse desactualizados en nuevas versiones, por lo que se recomenda acudir siempre al cdigo fuente.
En grandes rasgos, el funcionamiento es:
-
Flexlee la ltima lnea del fichero que se pasa como parmetro y va pasando tokens aBison. -
Bisonreliza el anlisis semntico y va construyendo la estructura de datos que representa el tableaux. - Dicha estructura se desarrolla y resuelve.
- Esta estructura se pasa a una funcin que la imprimir por pantalla, y otra que la imprimir en un fichero svg.
Compilado con
viva gnu D:
Notas
- Para dibujar el rbol(fichero Tree.c)me he apoyado de cdigo que encontr en esta web