FOLST

Una herramienta didáctica para la Lógica de Predicados de Primer Orden

FOLST es una herramienta que busca permitir a los estudiantes experimentar los alcances de la Lógica de Predicados de Primer Orden. Otorga al usuario la posibilidad de crear modelos particulares para luego evaluar la validez de fórmulas en ellos, enfoque que contrasta con la evaluación de fórmulas de manera genérica. Los modelos pueden ser creados bajo ciertos frames predefinidos, y la extensión de la herramienta para agregar nuevos frames es sencilla. Actualmente cuenta con dos frames: Granja y Mundo.

Características de la herramienta

Didáctica, visual e interactiva, para ser utilizada por los estudiantes en un curso de Lógica.
Emplea la misma notación que emplea la bibliografía en general.
Permite al usuario trabajar con varios modelos a la vez y evaluar las mismas fórmulas en distintos modelos.
Asiste de manera didáctica en la construcción y evaluación de las fórmulas.
Permite cargar y guardar modelos y fórmulas.

Para complementar el proceso de aprendizaje/enseñanza de la Lógica de Predicados de Primer Orden (LdPPO) se buscó desarrollar una herramienta didáctica, que fuera intuitiva y cuya notación se correspondiera con aquella vista en clase.
La LdPPO es una extensión de la lógica proposicional en la que se incluyen predicados y funciones (que se aplican sobre un dominio), lo que constituye al modelo o interpretación. También se adiciona la posibilidad de cuantificar variables.
Las fórmulas en LdPPO dependen de la definición del modelo sobre el cual se las evalúa, lo que le agrega dificultad en comparación con la lógica proposicional. Existen numerosos algoritmos que buscan, por ejemplo, encontrar contradicciones en las fórmulas. Sin embargo, por ser éstos indecidibles, a veces es necesario realizar una evaluación semántica de la fórmula en el modelo.

La idea de FOLST es permitir la evaluación de fórmulas en modelos construidos por el usuario, y así experimentar el significado de la LdPPO en situaciones realistas y conocer sus alcances y limitaciones.

Se desarrolló como trabajo final para dos materias del segundo año de la carrera de Ingeniería de Sistemas de la Facultad de Ciencias Exactas de la UNCPBA: Análisis y Diseño de Algoritmos I y Ciencias de la Computación II. En esta última se dictan los contenidos en LdPPO, para los cuales FOLST busca dar soporte didáctico.

Implementación:

C++
Análisis sintáctico-léxico usando Flex y Bison
Interfaz gráfica empleando Librerías Qt (haciendo uso extensivo de QGraphicsView).

Autores: Luciano Gervasoni y Emmanuel Maggiori