Ideales y filtros de implicantes/implicados en lógicas temporales con tiempo lineal y discreto

Resumen

Enmarcado en el campo de los Fundamentos Matemáticos de la Demostración Automática, realiza un estudio de las lógicas temporales proposionales, extensiones de la lógica clásica, definidas como álgebras abstractas, que permite la extensión a éstas de la metodología de demostración automática TAS, La metodología TAS se ha consolidado ya como una sólida alternativa a los trabajos existentes en demostración automática no clausal, como los métodos de Resolución y los métodos Tableaux. La herramienta fundamental de los métodos TAS es asociar a cada subfórmula de una fórmula en la lógica considerada una lista de implicantes e implicados; la información recogida en estas listas, se usará posteriormente para eldiseño de transformaciones de reducción. Por esta razón, en este trabajo desarrollamos una teoria de cierre completamente novedosa, sobre los Ideales/Filtros de literales Implicantes/Implicados de una fórmula, introduciendo las nociones de conjuntos a-cerrados y B-cerrados de literales y el concepto de base de estos conjuntos. Demostramos la unicidad de las bases y su propiedad de maximalidad sobre la cantidad de información por ellas recogida. Puesto que el objeto final es la aplicabilidad de nuestra investigación, en el desarrollo de este trabajo se estudian los aspectos computacionales de la teoría introducida, diseñando, en particular, algoritmos de gestión de los Ideales/Filtros de literales Implicantes/Implicados y del cálculo de las bases que, como se demuestra, tienen coste lineal.