Tesis doctoral de Gloria Gutierrez Barranco
El grupo de investigacion gimac ha desarrollado la metodología de demostracion automatica de teoremas tas, tanto para logica clasica proposicional como para logicas no clasicas, en particular para la logicas temporales. la metodología tas esta basada en recoger la maxima informacion de una formula, con el minimo coste, esta informacion se recoge en terminos de literales implicantes e implicados de una formula. los ultimos avances en la metodología tas, junto con el hecho de que los conjuntos de literales implicantes e implicados de una formula pueden ser infinitos, ponen de manifiesto la necesidad de realizar un estudio teorico sobre las restricciones de ideales y filtros en multirreticulos. la propiedad de «agrupabilidad» permite definir los ideales y filtros restingidos como clausura inductiva para un operador no determinista binario, y es indispensable para que el manejo de los literales temporales que son implicantes o implicados de una formula sea eficiente. la teoria de bases finitas de ideales restringidos desarrollados en esta tesis permiten obtener toda la informacion de una formula, de la forma mas eficiente posible. Dicha teoria nos permite manipular los ideales y filtros restringidos, utilizando solo conjuntos finitos. utilizando los conceptos de base de un ideal/filtro restringido se generalizan para la logica fnext las delta-listas de literales implicantes e implicados de la logica clasica proposicional. Por ultimo, utilizando las delta-listas, se generalizan para la logica fnext los delta-arboles de la logica clasica proposicional, lo que permite no solo representar las formulas, sino diseñar e implementar algoritmos de reduccion sobre ellas. aunque los desarrollos teoricos se aplican a la logica fnext, son extensibles a cualquier logica temporal proposional.
Datos académicos de la tesis doctoral «Bases de ideales en multirreticulos y delta-arboles«
- Título de la tesis: Bases de ideales en multirreticulos y delta-arboles
- Autor: Gloria Gutierrez Barranco
- Universidad: Málaga
- Fecha de lectura de la tesis: 14/09/2001
Dirección y tribunal
- Director de la tesis
- Inmaculada Perez De Guzman Molina
- Tribunal
- Presidente del tribunal: Barja perez José María
- José Muñoz perez (vocal)
- Quesada molina Juan José (vocal)
- Manuel Enciso garcia-oliveros (vocal)