Lógica computacional desde el punto de vista de la programación funcional : eliminación de cuantificadores

Abstract

Computational Logic is a wide interdisciplinary field having its theoretical and practical roots in mathematics, computer science, logic, and artificial intelligence. Computational Logic try to produce efficient and powerful algorithms for deciding the satisfiability of formulas in logical theories. This work is about propositional and first order logic, and its implementation in the functional language Ocaml. In particular, the aim of this work is to explain the quantifier elimination algorithm. As an example, we develop the quantifier elimination algorithm for the Theory of dense linear orders. Quantifier elimination is an algorithm supported by some logical theories. By eliminating quantifiers from a formula, it makes it possible to test its satisfiability in the sense of propositional logic.