Trabajo Fin de Grado
Lógica computacional desde el punto de vista de la programación funcional : eliminación de cuantificadores
Autor/es | Mateo Ceballos, María Dolores |
Director | Alonso Jiménez, José Antonio
Hidalgo Doblado, María José |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la computación e Inteligencia artificial |
Fecha de publicación | 2022-06-15 |
Fecha de depósito | 2022-06-15 |
Titulación | Universidad de Sevilla. Grado en Matemáticas |
Resumen | 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 ... 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. |
Cita | Mateo Ceballos, M.D. (2022). Lógica computacional desde el punto de vista de la programación funcional : eliminación de cuantificadores. (Trabajo Fin de Grado Inédito). Universidad de Sevilla, Sevilla. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
María Dolores Mateo Ceballos.pdf | 488.0Kb | [PDF] | Ver/ | |