Ithaca pretende ser una aplicación educativa.Dentro del mundo de la lógica, resulta necesario prestar
atención no solamente a los avances y descubrimientos, sino también a las personas que se inician en este apasionante mundo.
Para ayudar a estas personas, esta herramienta trata de servir de apoyo en el aprendizaje y uso de
cuantificadores en la construcción de fórmulas lógicas. Las senténcias lógicas (fórmulas) son un paso fundamental en la formalización de conceptos e ideas
que aparecen en la docencia y uso de la lógica clásica y otras superiores.
El modelo fundamental y el diseño de Ithaca está fuertemente ligado a la forma de trabajo de la
conocida aplicación Tarski's World(Si conoce el funcionamiento de esta, no tendrá problema en utilizar Ithaca). Sin embargo, gracias a la
experiencia lograda por el equipo de desarrollo en el uso de dicha herramienta gemela, se ha perfeccionado más su modelo en los campos más
interesantes para los posibles alumnos. Ideas como la satisfacibilidad de fórmulas en mundos vacíos o cambiantes son los principales.
La satisfacibilidad de las fórmulas se hace sobre un mundo ficticio finito, representado por una malla
sobre la que se colocan elementos de diferentes características. Lás fórmulas o sentencias se construyen mediante precicados simples que dicen algo
de los elementos que hay en esa malla.
La ventana principal de usuario es la siguiente:
En la parte inferior izquierda se representa el "mundo" (la malla). Cuando no hemos introducido ningún
elemento en el mundo, sobre la malla aparece flotando la imagen de un "fantasma".
Esto se debe a que en la lógica clásica no puede existir un mundo sin elementos sobre el que se puedan
preguntar cosas. Cuando no hay ningún elemento introducido por el usuario la malla no va a estar "formalmente" vacía. Al menos va a tener un elemento
abstracto sobre el que todos los predicados siples van a ser falsos. Esto nos permite descubrir qué fórmulas son tautológicas.
En la parte inferior derecha está el espacio para introducir sentencias lógicas y analizarlas. En cada area
de texto se puede introducir una y analizarla sobre el mundo disponible usando su botón asociado.
En la parte superior se encuentra un teclado. Su misión es simplificar la construcción de sentencias con
clicks de ratón. También pueden ser tecleadas a mano aunque algunos símbolos (como los cuantificadores) dificilmente se encuentran en los teclados
estandar. La mayoría de componentes ofrecen ayuda al usuario sin más que dejar el puntero del ratón sobre el mismo.
La apariencia de la interfaz de usuario puede ser cambiada en el menú herramientas.
Theme Motif en lugar el clásico Metall
Normalmente querrá intruducir y modificar los elementos de la malla a fin de adaptarlo a diferentes casos de
estudio. Los elementos que puede contener la malla son:
Además todos los elementos pueden tener dos tamaños diferentes (grandes o pequeños) y tres colores (rojo,
amarillo y azul). Para introducir elementos en la maya se deben utilizar los controles que hay a la derecha de la barra de herramientas superior.
En las dos primeras cajas combo se pueden seleccionar las características de colos y tamaño. Los botones
permiten insertar, en una posición aleatoria del mundo, el tipo de elementos seleccionado.El límite máximo es de 15 elementos.
Las casillas de la malla son sensibles a las pulsaciones del ratón; de forma que al hacer click sobre
cualquiera de ellas, queda iluminada y en selección.
La selección de casillas permite cambiar casillas de posición, darles nombre y eliminarlas de la malla.
Para eliminar un objeto debe seleccionarlo haciendo click sobre la casilla que ocupa y después sobre la imagen de la "papelera" que hay a
la izquierda de la malla
Para cambiar de lugar un objeto seleccione (en cualquier orden) las casillas de origen y de destino
del mismo.
Los objetos por defecto no tienen nombre, pero es posible asignarles uno. El nombre será único en el mundo
y puede ser cualquiera de los caracteres "a,b,c,d,e,f,g,h". Para asignar nombre a un objeto seleccione la casilla que ocupa y después sobre los
botones de la barra de herramientas superior que representa los nombres.
Las fórmulas se han de introducir una a una en los campos de texto. Se pueden teclear a mano pero resulta
más eficiente usar el teclado de ayuda.
Se pueden analizar las sentencias una a una o todas a la vez usando el botón "ANALIZAR TODAS" (también
disponible en el menú "Herramientas").
Para representar el resultado del análisis se utiliza un código de colores sobre el area de texto analizada
que contiene la sentencia. Es el siguiente:
El que una sentencia sea una F.B.F. (Fórmula Bien Formada) es diferente a que sea evaluable. A continuación
se describen las reglas de la gramática que se deben utilizar para crear correctamente las fórmulas y analizarlas.
FORMULA = expresion * Los espacios no influyen.
expresion = ( expr ^ expr )
ó ( expresion v expresion )
ó NOT expresion
ó ( expresion --> expresion )
ó ( expresion <-> expresion )
ó CUANTIFICADOR expresion
ó FUNCION
ó ( expr )
FUNCCION= GRANDE ( PARAMETRO )
ó PEQUENHO ( PARAMETRO )
ó ROJO ( PARAMETRO )
ó AZUL ( PARAMETRO )
ó AMARILLO ( PARAMETRO )
ó ESFERA ( PARAMETRO )
ó CUBO ( PARAMETRO )
ó PIRAMIDE ( PARAMETRO )
ó MASGRANDE ( PARAMETRO , PARAMETRO )
ó MASPEQUENHO ( PARAMETRO , PARAMETRO )
ó MISMAFORMA ( PARAMETRO , PARAMETRO )
ó MISMOCOLOR ( PARAMETRO , PARAMETRO )
ó MISMOTAMANHO ( PARAMETRO , PARAMETRO )
ó MISMAFILA ( PARAMETRO , PARAMETRO )
ó MISMACOLUMNA ( PARAMETRO , PARAMETRO )
ó IZQUIERDA ( PARAMETRO , PARAMETRO )
ó DERECHA ( PARAMETRO , PARAMETRO )
ó ARRIBA ( PARAMETRO , PARAMETRO )
ó ABAJO ( PARAMETRO , PARAMETRO )
ó ALREDEDOR ( PARAMETRO , PARAMETRO )
ó ENTRE ( PARAMETRO , PARAMETRO , PARAMETRO )
ó TAUTO ( )
ó FALSE ( )
ó ( PARAMETRO EQUAL PARAMETRO )
CUANTIFICADOR = CUANTIFICADOR_UNIVERSAL VARIABLE
ó CUANTIFICADOR_EXISTENCIAL VARIABLE
ó NO_CUANTIFICADOR CUANTIFICADOR
PARAMETRO = NOMBRE
ó VARIABLE
La mayoría de errores de sintaxis se deben a la ausencia de los paréntesis necesarios. De esta
forma son sentencias:
CORRECTAS:
(( A v B) v C)
((A^B)-->(CvD))
INCORRECTAS:
( A v B v C)
(A^B)-->(CvD)
Una posibilidad interesante a la hora de evaluar sentencias es poder modificar el "mundo" sobre el que
se hace. Normalmente la verdad o falsedad de una fórmula suele estar ligada a las características del mundo en que se evalua. Sin embargo, ciertas fórmulas,
llamadas "verdades lógicas" o "falsedades lógicas" no dependen del mundo en que se analicen y serán verdaderas o falsas en cualquiera de ellos
(idealmente en los infinitos mundos posibles). Como demostrar que una determinada fórmula es una verdad lógica es formalmente muy complicado y
computacionalmente caro, esa posiblidad no está implementada en Ithaca.
Hay tres mundos alternativos sobre los que también se pueden analizar las fórmulas. Para hacer esto la sentencia
en cuestión debe estar previamente analizada sobre la malla. Los botones que realizan los análisis alternativos se encuentran en la parte
inferior derecha:
Puede almacenar el trabajo realizado (el estado de la "malla" y las fórmulas introducidas) en archivos de
extensión .itk