Modelos formales de explicación en lógica e inteligencia artificial

Resumo

La abducción es el tipo de razonamiento en que, dada una teoría T (habitualmente un conjunto de fórmulas del lenguaje con el que se trabaje) y una observación O (generalmente una fórmula), tales que ni O ni su negación son consecuencia lógica de T, se trata de buscar una explicación E (una fórmula) tal que O sea consecuencia lógica de la unión de T y E, El razonamiento abductivo, que no puede ser reducido a deducción, plantea interesantes problemas que van más allá de los aspectos lógicos, como la distinción entre las concepciones de "abducción como producto" y "abducción como proceso" o los diferentes estadios de "generación" y "selección" de las hipótesis explicativas. El razonamiento abductivo encuentra aplicaciones en numerosas disciplinas, desde la Inteligencia Artificial a la Lingüística, pasando por las Ciencias Cognitivas o la Filosofía de la Ciencia. En este trabajo proponemos un cálculo abductivo, que llamamos delta-resolución, dual a la resolución clásica (Robinson, 1965) que tiene la virtud de generar hipótesis "de modo directo". Además, integra las nociones de abdución como "producto" y como "proceso", así como las etapas de "generación" y "selección". Igualmente, se apunta que la extensión a lógicas no clásicas resulta más prometedora en este que en otros acercamientos. Tras comparar la eficiencia con el sistema de Aliseda (1997), que emplea tablas semánticas para comenzar la búsqueda abductiva, se constata que nuestro sistema rinde notablemente mejor, sobre todo en los problemas más complejos, debido a que la heurística que sigue resulta computacionalmente mucho más ventajosa en los problemas abductivos más comunes en Programación Lógica y Representación del Conocimiento. En este sentido, se proporcionan implementaciones en SWI-Prolog de los algoritmos definidos. Finalmente, proponemos una extensión a lógica de primer orden que muestra que, aunque la abducción en estas l