Tesis doctoral de Pablo Jose Cordero Ortega
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.
Datos académicos de la tesis doctoral «Ideales y filtros de implicantes/implicados en lógicas temporales con tiempo lineal y discreto«
- Título de la tesis: Ideales y filtros de implicantes/implicados en lógicas temporales con tiempo lineal y discreto
- Autor: Pablo Jose Cordero Ortega
- Universidad: Málaga
- Fecha de lectura de la tesis: 13/12/1999
Dirección y tribunal
- Director de la tesis
- Inmaculada Perez De Guzman Molina
- Tribunal
- Presidente del tribunal: Barja perez José María
- jaume Agustí cullell (vocal)
- José Muñoz perez (vocal)
- Fariñas del cerro Luis (vocal)