Implementación de un demostrador automático de teoremas interactivo mediante el método de eliminación de modelos

Abstract

En este proyecto se ha desarrollado la herramienta de demostración automática interactiva de teoremas DATEM (Demostrador Automático Interactivo por Eliminación de Modelos) en el lenguaje de programación lógica Prolog. Mediante esta herramienta es posible demostrar la validez de las fórmulas lógicas a partir de teorías. Tanto las teorías como las fórmulas a demostrar se pueden introducir como conjuntos de cláusulas o como fórmulas de la lógica de primer orden. El sistema emplea el método de eliminación de modelos para intentar demostrar que una cierta fórmula es consecuencia lógica de un conjunto de premisas; si esto se consigue, además se obtiene una demostración de ello. DATEM es una herramienta altamente configurable y que ofrece una gran versatilidad a la hora de efectuar sus demostraciones, permitiendo al usuario configurar el proceso de demostración a su gusto para obtener los mejores resultados. Además cuenta con una interfaz gráfica amigable que facilita todas las acciones necesarias para llevar a cabo los procesos de demostración y la interpretación de los resultados obtenidos. [ABSTRACT] In this project a tool for automatic interactive theorem proving using the model elimination method called DATEM (Demostrador Automático Interactivo por Eliminación de Modelos) has been developed. This tool is written in the logic programming language Prolog. Using this application it is possible to prove the truth of logical theorems from a theory. Theories and theorems to prove can be written as set of clauses or using full first order logic formulas. This system employs the model elimination method to try to prove that a certain theorem is a logical consequence of a set of premises; if this goal is achieved the program shows an actual prove that fact. DATEM is a very customizable tool that offers great versatility to do demostrations of theorems, allowing the user to custom the demostration process to produce the best available results. Also it has a very friendly graphical user interface that makes it easy to perform all actions necessary to make the demostration and the interpretation of the output.