Proof procedures for multiple-valued propositional logics
- Autores: Felip Manyà Serres
- Directores de la Tesis: Gonzalo Escalada Imaz (dir. tes.)
- Lectura: En la Universitat Autònoma de Barcelona ( España ) en 1997
- Idioma: inglés
- Tribunal Calificador de la Tesis: Francesc Esteva i Massaguer (presid.) , Lluis Godo Lacasa (secret.) , Buenaventura Verdú i Solans (voc.) , Reiner Hahnle (voc.) , Jaume Agustí i Cullell (voc.)
- Texto completo no disponible (Saber más ...)
- Resumen
En esta tesis se presentan procedimientos de prueba para logicas proposicionales multivaluadas, se definen calculos completos, estructuras de datos eficientes, heuristicas para controlar el espacio de busqueda y tecnicas para ahorrar calculos no necesarios. En primer lugar, se diseñan algoritmos para comprobar la satisfactibilidad de formulas signadas (generales y regulares), los cuales sirven para resolver el problema de la satisfactibilidad en cualquier logica finitamente-valuada. Luego, se demuestra que el problema de la satisfactibilidad de formulas horn regulares tiene una complejidad lineal, y que el problema de la 2-satisfactibilidad para formulas signadas arbitrarias es np-completo, aunque admite soluciones polinomiles si las formulas son regulares o los signos son singletons. Finalmente, se diseña un interprete lineal para una amplia familia de logicas infinitamente-valuadas, el cual esta basado en una regla de inferencia modus-ponens e incorpora una regla de negacion por fallo finito multivaluada y un operador de corte multivaluado.
