Resumen:
La lógica H(@) es la que se obtiene al agregar nominales y el operador de satisfacción @ a la lógica modal básica. Ambas lógicas son decidibles para el problema de la validez de una fórmula, y su complejidad es PSPACE-complete. Tradicionalmente, los demostradores de teoremas para la lógica modal básica estuvieron basados en algoritmos de tableau, con los cuales se obtuvieron muy buenos resultados. Sin embargo, la lógica 1i(@) introduce una noción de igualdad que degrada la performance de este algoritmo; por esta razón resulta interesante investigar qué sucede con otras familias de algoritmos. En [Areces et al., 2001] se propone un cálculo basado en resolución para esta lógica. Este cálculo, si bien consistente y completo, carece de las estrategias de orden y selección que son estándar en resolución para lógica de primer orden. Es necesario contar con un mecanismo como este, que regule la generación de nuevas cláusulas, si se desea implementar en forma realista un demostrador basado en este cálculo. En este trabajo incorporamos orden y selección al cálculo propuesto en [Areces et al., 2001], y demostramos que este agregado preserva completitud refutacional. Además, proponemos un manejo más cuidadoso en la generación de nuevos nominales y en el manejo de la paramodulación; con esto podemos garantizar que el cálculo genera un número finito de cláusulas y, por lo tanto, que constituye un método de decisión para el problema de la validez de una fórmula de 1i(@). Finalmente, incorporamos estos resultados a HyLoRes, una implementación experimental del cálculo de [Areces et al., 2001], y hacemos una breve comparación de la performance de ambas versiones.
Citación:
---------- APA ----------
Gorín, Daniel Alejandro. (2004). Resolución con orden y selección para la lógica H(@). (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000783_Gorin
---------- CHICAGO ----------
Gorín, Daniel Alejandro. "Resolución con orden y selección para la lógica H(@)". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2004.https://hdl.handle.net/20.500.12110/seminario_nCOM000783_Gorin
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000783_Gorin.pdf
Distrubución geográfica
