Inicio

Guacarí Modal es un demostrador automático por el método del tableaux desarrollado en C#, para sistemas modales normales y no normales. Actualmente contamos con la implementación de los sistemas K y S2. La primera versión de Guacarí Modal fue desarrollada por un grupo de docentes y estudiantes del Programa de Matemáticas de la Fundación Universitaria Konrad Lorenz en Bogotá, Colombia, en colaboración con Alfredo Burrieza en la Universidad de Málaga, España. El software se distribuye como software libre y abierto a modificaciones, con miras al beneficio de la comunidad científica.

Este trabajo de investigación inició con la indagación de distintos programas y herramientas de programación para ampliar las expresiones de otros conectivos fuera de la lógica clásica. Esta búsqueda se mantuvo por distintas vías con programas que permitieran expresar orden en la lectura y aplicación de los conectivos lógicos, dicha necesidad estaba presente para garantizar la aplicación del algoritmo del método de tableaux.

Basados en un código libre realizado en C++, el cual se modificó para generar un nuevo código para la lectura de los conectivos, donde se realizó la programación conserva la idea de Melvin Fitting de la indización de las líneas y mundos posibles asociados a cada fórmula. El método del tableaux para las lógicas K y S2 garantizaban la terminación, completitud y corrección del algoritmo; la programación sigue el paso a paso evidenciando el orden en la aplicación de los distintitos tipos de fórmulas.

Instalación

Para hacer uso del demostrador Guacarí modal se requiere una computadora con con SO Windows y seguir los siguientes pasos:

1. Instale Microsoft .NET Framework 4 (Standalone Installer)
   +Página de descarga
2. Descargue Guacarí Modal:
   +Página de descarga (formato RAR)
3. Descomprima el archivo RAR Guacarí Modal y ejecutar:
   ML Viewer > Bin > Release > ML Viewer Application