El concepto de modelo estable , o conjunto de respuestas , se usa para definir una semántica declarativa para programas lógicos con negación como falla . Este es uno de los varios enfoques estándar del significado de la negación en la programación lógica, junto con la finalización del programa y la semántica bien fundada . La semántica del modelo estable es la base de la programación de conjuntos de respuestas .
Motivación
La investigación sobre la semántica declarativa de la negación en la programación lógica fue motivada por el hecho de que el comportamiento de la resolución SLDNF - la generalización de la resolución SLD utilizada por Prolog en presencia de negación en los cuerpos de reglas - no coincide completamente con las tablas de verdad conocidas de lógica proposicional clásica . Considere, por ejemplo, el programa
Dado este programa, la consulta p tendrá éxito, porque el programa incluye p como un hecho; la consulta q fallará, porque no se produce en la cabecera de ninguna de las reglas. La consulta r también fallará, porque la única regla con r en la cabeza contiene el subobjetivo q en su cuerpo; como hemos visto, ese subobjetivo fracasa. Finalmente, la consulta s tiene éxito, porque cada uno de los subobjetivos p ,tiene éxito. (Este último tiene éxito porque falla la meta positiva q correspondiente ). En resumen, el comportamiento de la resolución SLDNF en el programa dado se puede representar mediante la siguiente asignación de verdad:
pag q r s T F F T .
Por otro lado, las reglas del programa dado pueden verse como fórmulas proposicionales si identificamos la coma con la conjunción, el símbolo con negación y acepta tratar como la implicación escrito al revés. Por ejemplo, la última regla del programa dado es, desde este punto de vista, la notación alternativa para la fórmula proposicional
Si calculamos los valores de verdad de las reglas del programa para la asignación de verdad se muestra arriba a continuación, veremos que cada regla obtiene el valor T . En otras palabras, esa asignación es un modelo del programa. Pero este programa también tiene otros modelos, por ejemplo
pag q r s T T T F .
Por tanto, uno de los modelos del programa dado es especial en el sentido de que representa correctamente el comportamiento de la resolución SLDNF. ¿Cuáles son las propiedades matemáticas de ese modelo que lo hacen especial? La respuesta a esta pregunta la proporciona la definición de modelo estable.
Relación con la lógica no monotónica
El significado de la negación en los programas lógicos está estrechamente relacionado con dos teorías de razonamiento no monotónico : la lógica autoepistémica y la lógica predeterminada . El descubrimiento de estas relaciones fue un paso clave hacia la invención de la semántica del modelo estable.
La sintaxis de la lógica autoepistémica utiliza un operador modal que nos permite distinguir entre lo que es verdadero y lo que se cree. Michael Gelfond [1987] propuso leer en el cuerpo de una regla como " no se cree ", y entender una regla con la negación como la fórmula correspondiente de la lógica autoepistémica. La semántica del modelo estable, en su forma básica, puede verse como una reformulación de esta idea que evita referencias explícitas a la lógica autoepistémica.
En la lógica predeterminada, una regla predeterminada es similar a una regla de inferencia , excepto que incluye, además de sus premisas y conclusión, una lista de fórmulas llamadas justificaciones. Se puede usar un incumplimiento para derivar su conclusión bajo el supuesto de que sus justificaciones son consistentes con lo que se cree actualmente. Nicole Bidoit y Christine Froidevaux [1987] propusieron tratar los átomos negados en los cuerpos de reglas como justificaciones. Por ejemplo, la regla
puede entenderse como el valor predeterminado que nos permite derivar de asumiendo que es consistente. La semántica del modelo estable usa la misma idea, pero no se refiere explícitamente a la lógica predeterminada.
Modelos estables
La definición de modelo estable a continuación, reproducida de [Gelfond y Lifschitz, 1988], utiliza dos convenciones. En primer lugar, una asignación de verdad se identifica con el conjunto de átomos que obtienen el valor T . Por ejemplo, la asignación de la verdad
pag q r s T F F T .
se identifica con el conjunto . Esta convención nos permite usar la relación de inclusión de conjuntos para comparar asignaciones de verdad entre sí. La más pequeña de todas las asignaciones de verdades el que hace que todo átomo sea falso; la asignación de verdad más grande hace que cada átomo sea verdadero.
En segundo lugar, un programa lógico con variables se considera una abreviatura del conjunto de todas las instancias básicas de sus reglas, es decir, del resultado de sustituir términos libres de variables por variables en las reglas del programa de todas las formas posibles. Por ejemplo, la definición de programación lógica de números pares
se entiende como el resultado de reemplazar X en este programa por los términos básicos
de todas las formas posibles. El resultado es el programa de suelo infinito
Definición
Sea P un conjunto de reglas de la forma
dónde son átomos de tierra. Si P no contiene negación (en cada regla del programa) entonces, por definición, el único modelo estable de P es su modelo que es mínimo en relación con la inclusión de conjuntos. [1] (Cualquier programa sin negación tiene exactamente un modelo mínimo). Para extender esta definición al caso de programas con negación, necesitamos el concepto auxiliar del reducto, definido como sigue.
Para cualquier conjunto I de átomos terrestres, la reducción de P con respecto a I es el conjunto de reglas sin negación que se obtiene de P al descartar primero todas las reglas tales que al menos uno de los átomos en su cuerpo
pertenece a I , y luego dejar caer las piezas de los cuerpos de todas las reglas restantes.
Decimos que I es un modelo estable de P si lo es el modelo estable del reducto de P con respecto a I . (Dado que el reduct no contiene negación, su modelo estable ha sido ya definido.) Como el término "modelo estable" indica, cada modelo estable de P es un modelo de P .
Ejemplo
Para ilustrar estas definiciones, comprobemos que es un modelo estable del programa
La reducción de este programa en relación con es
(De hecho, desde , la reducción se obtiene del programa soltando la pieza ) El modelo estable del reducto es . (De hecho, este conjunto de átomos satisface todas las reglas del reducto y no tiene subconjuntos propios con la misma propiedad). Por tanto, después de calcular el modelo estable del reducto llegamos al mismo conjuntocon el que empezamos. En consecuencia, ese conjunto es un modelo estable.
Comprobando de la misma forma los otros 15 conjuntos que constan de los átomos muestra que este programa no tiene otros modelos estables. Por ejemplo, la reducción del programa en relación con es
El modelo estable del reducto es , que es diferente del conjunto con el que empezamos.
Programas sin un modelo estable único
Un programa con negación puede tener muchos modelos estables o ningún modelo estable. Por ejemplo, el programa
tiene dos modelos estables , . El programa de una sola regla
no tiene modelos estables.
Si pensamos en la semántica del modelo estable como una descripción del comportamiento de Prolog en presencia de negación, entonces los programas sin un modelo estable único pueden considerarse insatisfactorios: no proporcionan una especificación inequívoca para la respuesta a consultas al estilo Prolog. Por ejemplo, los dos programas anteriores no son razonables como programas Prolog: la resolución SLDNF no termina en ellos.
Pero el uso de modelos estables en la programación de conjuntos de respuestas proporciona una perspectiva diferente sobre dichos programas. En ese paradigma de programación, un problema de búsqueda dado está representado por un programa lógico de modo que los modelos estables del programa correspondan a las soluciones. Entonces, los programas con muchos modelos estables corresponden a problemas con muchas soluciones, y los programas sin modelos estables corresponden a problemas sin solución. Por ejemplo, el rompecabezas de las ocho reinas tiene 92 soluciones; para resolverlo mediante la programación de conjuntos de respuestas, lo codificamos mediante un programa lógico con 92 modelos estables. Desde este punto de vista, los programas lógicos con exactamente un modelo estable son bastante especiales en la programación de conjuntos de respuestas, como los polinomios con exactamente una raíz en álgebra.
Propiedades de la semántica del modelo estable
En esta sección, como en la definición de modelo estable anterior, por programa lógico nos referimos a un conjunto de reglas de la forma
dónde son átomos de tierra.
- Átomos de cabeza
- Si un átomo A pertenece a un modelo estable de un programa de lógica de P entonces A es la cabeza de una de las reglas de P .
- Minimidad
- Cualquier modelo estable de un programa lógico P es mínimo entre los modelos de P en relación con la inclusión de conjuntos.
- La propiedad antichain
- Si I y J son modelos estables del mismo programa de lógica entonces yo no es un subconjunto propio de J . En otras palabras, el conjunto de modelos estables de un programa es un antichain .
- NP-completitud
- Probar si un programa de lógica de tierra finita tiene un modelo estable es NP-completo .
Relación con otras teorías de la negación como fracaso
Finalización del programa
Cualquier modelo estable de un programa de terreno finito no es sólo un modelo del programa en sí, sino también un modelo de su finalización [Marek y Subrahmanian, 1989]. Sin embargo, lo contrario no es cierto. Por ejemplo, la finalización del programa de una regla
es la tautología . El modelo de esta tautología es un modelo estable de , pero su otro modelo no es. François Fages [1994] encontró una condición sintáctica en los programas lógicos que elimina tales contraejemplos y garantiza la estabilidad de cada modelo de finalización del programa. Los programas que satisfacen su condición se denominan ajustados .
Fangzhen Lin y Yuting Zhao [2004] mostraron cómo fortalecer la finalización de un programa no nocturno para que todos sus modelos no estables sean eliminados. Las fórmulas adicionales que agregan a la finalización se denominan fórmulas de bucle .
Semántica bien fundada
El modelo bien fundado de un programa lógico divide todos los átomos de tierra en tres conjuntos: verdadero, falso y desconocido. Si un átomo es verdadero en el modelo bien fundado de entonces pertenece a todo modelo estable de . Lo contrario, en general, no se sostiene. Por ejemplo, el programa
tiene dos modelos estables, y . Aunquepertenece a ambos, se desconoce su valor en el modelo bien fundado .
Además, si un átomo es falso en el modelo bien fundado de un programa, entonces no pertenece a ninguno de sus modelos estables. Así, el modelo bien fundado de un programa lógico proporciona un límite inferior en la intersección de sus modelos estables y un límite superior en su unión.
Fuerte negación
Representando información incompleta
Desde la perspectiva de la representación del conocimiento , un conjunto de átomos fundamentales puede considerarse como una descripción de un estado completo de conocimiento: se sabe que los átomos que pertenecen al conjunto son verdaderos, y los átomos que no pertenecen al conjunto son conocido por ser falso. Un estado de conocimiento posiblemente incompleto puede describirse utilizando un conjunto de literales consistente pero posiblemente incompleto; si un átomo no pertenece al conjunto y su negación tampoco pertenece al conjunto, entonces no se sabe si es verdadero o falso.
En el contexto de la programación lógica, esta idea conduce a la necesidad de distinguir entre dos tipos de negación: la negación como falla , discutida anteriormente, y la negación fuerte , que aquí se denota por. [2] El siguiente ejemplo, que ilustra la diferencia entre los dos tipos de negación, pertenece a John McCarthy . Un autobús escolar puede cruzar las vías del tren con la condición de que no se acerque ningún tren. Si no sabemos necesariamente si se acerca un tren, entonces la regla que usa la negación como falla
no es una representación adecuada de esta idea: dice que está bien cruzar en ausencia de información sobre un tren que se aproxima. Es preferible la regla más débil, que usa una fuerte negación en el cuerpo:
Dice que está bien cruzar si sabemos que no se acerca ningún tren.
Modelos estables coherentes
Para incorporar la negación fuerte en la teoría de modelos estables, Gelfond y Lifschitz [1991] permitieron que cada una de las expresiones , , en una regla
ser un átomo o un átomo prefijado con el símbolo de negación fuerte. En lugar de modelos estables, esta generalización utiliza conjuntos de respuestas , que pueden incluir tanto átomos como átomos con el prefijo de negación fuerte.
Un enfoque alternativo [Ferraris y Lifschitz, 2005] trata la negación fuerte como parte de un átomo y no requiere ningún cambio en la definición de un modelo estable. En esta teoría de la negación fuerte, distinguimos entre átomos de dos tipos, positivos y negativos , y asumimos que cada átomo negativo es una expresión de la forma, dónde es un átomo positivo. Un conjunto de átomos se llama coherente si no contiene pares de átomos "complementarios". Los modelos estables coherentes de un programa son idénticos a sus conjuntos de respuestas coherentes en el sentido de [Gelfond y Lifschitz, 1991].
Por ejemplo, el programa
tiene dos modelos estables, y . El primer modelo es coherente; el segundo no lo es, porque contiene tanto el átomo y el átomo .
Supuesto de mundo cerrado
Según [Gelfond y Lifschitz, 1991], el supuesto de mundo cerrado para un predicado puede ser expresado por la regla
(la relación no es válido para una tupla si no hay evidencia de que lo haga). Por ejemplo, el modelo estable del programa
consta de 2 átomos positivos
y 14 átomos negativos
es decir, las fuertes negaciones de todos los demás átomos de tierra positivos formados a partir de .
Un programa lógico con una fuerte negación puede incluir las reglas de suposición de mundo cerrado para algunos de sus predicados y dejar los otros predicados en el ámbito de la suposición de mundo abierto .
Programas con limitaciones
La semántica del modelo estable se ha generalizado a muchos tipos de programas lógicos distintos de las colecciones de reglas "tradicionales" discutidas anteriormente: reglas de la forma
dónde son átomos. Una extensión simple permite que los programas contengan restricciones : reglas con la cabeza vacía:
Recuerde que una regla tradicional puede verse como una notación alternativa para una fórmula proposicional si identificamos la coma con la conjunción , el símbolo con negación y acepta tratar como la implicación escrito al revés. Para extender esta convención a las restricciones, identificamos una restricción con la negación de la fórmula correspondiente a su cuerpo:
Ahora podemos extender la definición de un modelo estable a programas con restricciones. Como en el caso de los programas tradicionales, comenzamos con programas que no contienen negación. Tal programa puede ser inconsistente; entonces decimos que no tiene modelos estables. Si tal programa es consistente entonces tiene un modelo mínimo único, y ese modelo se considera el único modelo estable de .
A continuación, se definen modelos estables de programas arbitrarios con restricciones usando reducts, formados de la misma manera que en el caso de los programas tradicionales (ver la definición de un modelo estable más arriba). Un conjuntode átomos es un modelo estable de un programa con restricciones si la reducción de relativo a tiene un modelo estable, y ese modelo estable es igual .
Las propiedades de la semántica del modelo estable indicadas anteriormente para los programas tradicionales también se mantienen en presencia de restricciones.
Las restricciones juegan un papel importante en la programación de conjuntos de respuestas porque agregar una restricción a un programa lógico afecta la colección de modelos estables de de una manera muy simple: elimina los modelos estables que violan la restricción. En otras palabras, para cualquier programa con restricciones y cualquier restricción , los modelos estables de pueden caracterizarse como los modelos estables de que satisfacen .
Programas disyuntivos
En una regla disyuntiva , la cabeza puede ser la disyunción de varios átomos:
(el punto y coma se considera una notación alternativa para la disyunción ). Las reglas tradicionales corresponden ay restricciones a. Para extender la semántica del modelo estable a programas disyuntivos [Gelfond y Lifschitz, 1991], primero definimos que en ausencia de negación (en cada regla) los modelos estables de un programa son sus modelos mínimos. La definición del reducto para programas disyuntivos sigue siendo la misma que antes . Un conjuntode átomos es un modelo estable de Si es un modelo estable de la reducción de relativo a .
Por ejemplo, el conjunto es un modelo estable del programa disyuntivo
porque es uno de los dos modelos mínimos de la reducción
El programa anterior tiene un modelo más estable, .
Como en el caso de los programas tradicionales, cada elemento de cualquier modelo estable de un programa disyuntivo es un átomo de cabeza de , en el sentido de que ocurre en la cabeza de una de las reglas de . Como en el caso tradicional, los modelos estables de un programa disyuntivo son mínimos y forman un antichain. Probar si un programa disyuntivo finito tiene un modelo estable es-completa [Eiter y Gottlob, 1993].
Modelos estables de un conjunto de fórmulas proposicionales
Las reglas, e incluso las reglas disyuntivas , tienen una forma sintáctica bastante especial, en comparación con las fórmulas proposicionales arbitrarias . Cada regla disyuntiva es esencialmente una implicación tal que su antecedente (el cuerpo de la regla) es una conjunción de literales , y su consecuente (cabeza) es una disyunción de átomos. David Pearce [1997] y Paolo Ferraris [2005] mostraron cómo extender la definición de un modelo estable a conjuntos de fórmulas proposicionales arbitrarias. Esta generalización tiene aplicaciones para responder a la programación de conjuntos .
La formulación de Pearce se ve muy diferente de la definición original de un modelo estable . En lugar de reducciones, se refiere a la lógica de equilibrio , un sistema de lógica no monotónica basado en los modelos de Kripke . La formulación de Ferraris, en cambio, se basa en reductos, aunque el proceso de construcción del reducto que utiliza difiere del descrito anteriormente . Los dos enfoques para definir modelos estables para conjuntos de fórmulas proposicionales son equivalentes entre sí.
Definición general de un modelo estable
Según [Ferraris, 2005], la reducción de una fórmula proposicional relativo a un conjunto de átomos es la fórmula obtenida de reemplazando cada subfórmula máxima que no es satisfecha por con la constante lógica (falso). El reducto de un conjunto de fórmulas proposicionales relativas a consiste en las reducciones de todas las fórmulas de relativo a . Como en el caso de los programas disyuntivos, decimos que un conjuntode átomos es un modelo estable de Si es mínima (con respecto a la inclusión de conjuntos) entre los modelos de reducción de relativo a .
Por ejemplo, la reducción del conjunto
relativo a es
Desde es un modelo del reducto, y los subconjuntos propios de ese conjunto no son modelos del reducto, es un modelo estable del conjunto de fórmulas dado.
Hemos visto esoes también un modelo estable de la misma fórmula, escrito en notación de programación lógica, en el sentido de la definición original . Este es un ejemplo de un hecho general: en aplicación a un conjunto de (fórmulas correspondientes a) reglas tradicionales, la definición de un modelo estable según Ferraris es equivalente a la definición original. Lo mismo es cierto, de manera más general, para los programas con restricciones y para los programas disyuntivos .
Propiedades de la semántica del modelo estable general
El teorema que afirma que todos los elementos de cualquier modelo estable de un programa son átomos de cabeza de puede extenderse a conjuntos de fórmulas proposicionales, si definimos los átomos principales de la siguiente manera. Un átomoes un átomo de cabeza de un conjunto de fórmulas proposicionales si al menos una ocurrencia de en una fórmula de no está ni en el ámbito de una negación ni en el antecedente de una implicación. (Suponemos aquí que la equivalencia se trata como una abreviatura, no como un conectivo primitivo).
La propiedad de minimidad y antichain de los modelos estables de un programa tradicional no se sostiene en el caso general. Por ejemplo, (el conjunto singleton que consiste en) la fórmula
tiene dos modelos estables, y . Este último no es mínimo, y es un superconjunto adecuado del primero.
Probar si un conjunto finito de fórmulas proposicionales tiene un modelo estable es Σ 2 PAG {\ Displaystyle \ Sigma _ {2} ^ {\ rm {P}}} -completo , como en el caso de los programas disyuntivos .
Ver también
- Programación del conjunto de respuestas
- Programación lógica
- Negación como fracaso
Notas
- ↑ Este enfoque de la semántica de los programas lógicos sin negación se debe a Maarten van Emden y Robert Kowalski [1976].
- ↑ Gelfond y Lifschitz [1991] llaman clásica a la segunda negacióny la denotan por.
Referencias
- N. Bidoit y C. Froidevaux [1987] El minimalismo subsume la lógica y la circunscripción por defecto . En: Actas de LICS-87, páginas 89–97.
- T. Eiter y G. Gottlob [1993] Resultados de complejidad para la programación de lógica disyuntiva y su aplicación a lógicas no monotónicas . En: Proceedings of ILPS-93, páginas 266–278.
- M. van Emden y R. Kowalski [1976] La semántica de la lógica de predicados como lenguaje de programación . Revista de ACM, vol. 23, páginas 733–742.
- F. Fages [1994] Consistencia de la finalización de Clark y existencia de modelos estables . Revista de métodos de lógica en ciencias de la computación, vol. 1, páginas 51–60.
- P. Ferraris [2005] Conjuntos de respuestas para teorías proposicionales . En: Actas de LPNMR-05, páginas 119-131.
- P. Ferraris y V. Lifschitz [2005] Fundamentos matemáticos de la programación de conjuntos de respuestas . En: ¡Les mostraremos! Ensayos en honor a Dov Gabbay, Publicaciones de King's College, páginas 615–664.
- M. Gelfond [1987] Sobre teorías autoepistémicas estratificadas . En: Actas de AAAI-87, páginas 207–211.
- M. Gelfond y V. Lifschitz [1988] La semántica del modelo estable para la programación lógica . En: Actas de la Quinta Conferencia Internacional sobre Programación Lógica (ICLP), páginas 1070–1080.
- M. Gelfond y V. Lifschitz [1991] Negación clásica en programas lógicos y bases de datos disyuntivas . Computación de nueva generación, vol. 9, páginas 365–385.
- S. Hanks y D. McDermott [1987] Lógica no monotónica y proyección temporal . Inteligencia artificial, vol. 33, páginas 379–412.
- F. Lin y Y. Zhao [2004] ASSAT: Computación de conjuntos de respuestas de un programa lógico mediante solucionadores SAT . Inteligencia artificial, vol. 157, páginas 115-137.
- V. Marek y VS Subrahmanian [1989] La relación entre la semántica del programa lógico y el razonamiento no monótono . En: Actas de ICLP-89, páginas 600–617.
- D. Pearce [1997] Una nueva caracterización lógica de modelos estables y conjuntos de respuestas . En: Extensiones no monotónicas de la programación lógica (Lecture Notes in Artificial Intelligence 1216), páginas 57–70.
- R. Reiter [1980] Una lógica para el razonamiento predeterminado . Inteligencia artificial, vol. 13, páginas 81-132.