Manual de uso - manugunther/sat GitHub Wiki
La pantalla
La pantalla se divide en tres áreas principales, a la izquierda hay un tablero donde se pueden ubicar figuras geométricas; a la derecha arriba están los controles que nos permiten configurar las figuras geómetricas que habrá en el tablero; debajo de esos controles hay una lista de fórmulas.
Manipulación de figuras
La forma de agregar una figura al tablero es haciendo click en el casillero donde se quiera ubicar; esa figura tendrá la forma, tamaño y color que se muestra a la izquierda de todos los controles. Esos controles están divididos en tres grupos: forma, tamaño y color; para cada uno de esos grupos hay que elegir una alternativa, simplemente cliqueando en la opción deseada.
Una vez que se ha puesto una figura en el tablero podemos eliminarla, para eso utilizamos el botón derecho; también podemos mover la figura de lugar arrastrándola hasta la nueva casilla. Si hacemos doble-click en una figura se abre un cuadro de texto donde se definen nombres para la figura; estos nombres corresponden a símbolos de constantes. Los nombres son una o dos letras en mayúscula; si queremos definir más de un nombre para una figura, debemos separarlos mediante espacio: A B XY.
Manipulación de fórmulas
El espacio a la derecha es para ingresar fórmulas cuya satisfacción queremos comprobar. Si queremos agregar más fórmulas podemos usar el botón + y para eliminar la fórmula seleccionada tenemos el botón - (también podemos utilizar las teclas Ins y Del respectivamente). Para editar una fórmula hacemos doble-click en el renglón correspondiente. Para acceder a los símbolos que no están en el teclado, podemos hacer click-derecho y buscar los símbolos en el menú contextual. Allí también se encuentran los nombres de los predicados y relaciones que podemos utilizar para construir nuestras fórmulas.
Para terminar de editar una fórmula utilizamos la tecla Enter (o Intro); puede ser que haya algún error en la escritura de la fórmula, en ese caso en la barra de estado se nos indica el error; en caso de dudas consultá la sección sintaxis. Las constantes que se pueden usar son las que se han definido en el modelo geométrico.
Para comprobar la satisfacción de las fórmulas se usa el botón ✓ (una tilde); solamente se comprobarán las fórmulas que no tengan variables libres. Cada fórmula es satisfecha o no satisfecha; en el primer caso se muestra un tilde a la derecha de la fórmula, y una cruz roja en el otro caso.
Sintaxis
La aplicación de símbolos de predicados y relaciones es con puntos: lo que habitualmente se escribe arriba(x,y) en Sat se escribe arriba.x.y La notación para cuantificadores que hay en el menú derecho también es rara: 〈∀x : P.x : R.x 〉 corresponde a (∀ x . P.x ⇒ R.x); en tanto 〈∃x : P.x : R.x 〉 corresponde a (∃ x . P.x ∧ R.x). En la notación 〈∀ x: P.x : R.x 〉 a P.x se le llama rango y término a R.x. Para omitir el rango podemos utilizar la constante True: 〈∀x : True : R.x 〉 y 〈∃x : True : R.x 〉; es un ejercicio fácil ver que (∀x . True ⇒ R.x) es equivalente a (∀x . R.x). También se pueden escribir los cuantificadores tradicionales (∀x . R.x) y (∃x. R.x); sin embargo estas construcciones no están en el menú.
Lista de símbolos
A continuación se muestran los símbolos Unicode que se deben utilizar para escribir fórmulas
- Comienzo de una cuantificación:
〈 - Fin de una cuantificación:
〉 - Símbolo para la cuantificación universal:
∀ - Símbolo para la cuantificación universal:
∃ - Símbolo para la conjunción:
∧ - Símbolo para la disyunción:
∨ - Símbolo para la implicación:
⇒ - Símbolo para la negación:
¬ - Símbolo para la equivalencia:
≡
Ejemplos de fórmulas
- Toda figura es un cuadrado:
〈∀ x : True : Cuad.x 〉 - Todo triángulo es rojo:
〈∀ x : Tr.x : Rojo.x 〉 - La figura A está a la derecha de la figura B:
der.A.B - Todo tríangulo tiene un círculo verde a su izquierda:
〈∀ x : Tr.x : 〈∃ y : Circ.y : Verde.y ∧ izq.x.y 〉