Semántica del modelo estable

El concepto de modelo estable , o conjunto de respuestas , se utiliza para definir una semántica declarativa para programas lógicos con negación como falla . Este es uno de los varios enfoques estándar para el 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 estuvo 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 familiares de la lógica proposicional clásica . Consideremos, por ejemplo, el programa

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p,\operatorname {not} q.}$

Dado este programa, la consulta p tendrá éxito, porque el programa incluye p como un hecho; la consulta q fallará, porque no ocurre en la cabecera de ninguna de las reglas. La consulta r también fallará, porque la única regla con r en la cabecera contiene el subobjetivo q en su cuerpo; como hemos visto, ese subobjetivo falla. Finalmente, la consulta s tiene éxito, porque cada uno de los subobjetivos p tiene éxito. (El último tiene éxito porque el objetivo positivo correspondiente q falla. ) En resumen, el comportamiento de la resolución SLDNF en el programa dado se puede representar mediante la siguiente asignación de verdad: ${\displaystyle \operatorname {not} q}$

Por otra parte, las reglas del programa dado pueden ser vistas como fórmulas proposicionales si identificamos la coma con la conjunción , el símbolo con la negación y acordamos tratarla como la implicación escrita al revés. Por ejemplo, la última regla del programa dado es, desde este punto de vista, una notación alternativa para la fórmula proposicional ${\displaystyle \land }$ ${\displaystyle \operatorname {not} }$ ${\displaystyle \neg }$ ${\displaystyle F\leftarrow G}$ ${\displaystyle G\rightarrow F}$

${\displaystyle p\land \neg q\rightarrow s.}$

Si calculamos los valores de verdad de las reglas del programa para la asignación de verdad mostrada arriba, 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

Por lo 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 definición de un modelo estable proporciona una respuesta a esta pregunta.

Relación con la lógica no monótona

El significado de la negación en los programas lógicos está estrechamente relacionado con dos teorías de razonamiento no monótono : la lógica autoepistémica y la lógica por defecto . 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 permite distinguir entre lo que es verdad y lo que se sabe. Michael Gelfond [1987] propuso leer en el cuerpo de una regla como " no se sabe", y entender una regla con 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. ${\displaystyle \operatorname {not} p}$ ${\displaystyle p}$

En la lógica por defecto, un defecto 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. Un defecto puede usarse para derivar su conclusión bajo el supuesto de que sus justificaciones son consistentes con lo que se conoce actualmente. Nicole Bidoit y Christine Froidevaux [1987] propusieron tratar los átomos negados en los cuerpos de las reglas como justificaciones. Por ejemplo, la regla

${\displaystyle s\leftarrow p,\operatorname {not} q}$

puede entenderse como el valor predeterminado que nos permite derivar de suponer que es consistente. La semántica del modelo estable utiliza la misma idea, pero no se refiere explícitamente a la lógica predeterminada. ${\displaystyle s}$ ${\displaystyle p}$ ${\displaystyle \neg q}$

Modelos estables

La definición de un modelo estable que se muestra 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 verdad

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 asignación de verdad más pequeña es la que hace que cada átomo sea falso; la asignación de verdad más grande hace que cada átomo sea verdadero. ${\displaystyle \{p,s\}}$ ${\displaystyle \emptyset }$

En segundo lugar, un programa lógico con variables se considera como una forma abreviada de designar el conjunto de todas las instancias básicas de sus reglas, es decir, el 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

${\displaystyle \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(X))\leftarrow \operatorname {not} \operatorname {even} (X)}$

se entiende como el resultado de reemplazar X en este programa por los términos fundamentales

${\displaystyle 0,s(0),s(s(0)),\dots .}$

De todas las formas posibles. El resultado es el programa de suelo infinito.

${\displaystyle \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(0))\leftarrow \operatorname {not} \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(s(0)))\leftarrow \operatorname {not} \operatorname {even} (s(0))}$

${\displaystyle \dots }$

Definición

Sea P un conjunto de reglas de la forma

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

donde son átomos fundamentales. 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 del conjunto. ^[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 de reduct, definido de la siguiente manera. ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$ ${\displaystyle n=0}$

Para cualquier conjunto I de átomos fundamentales, la reducción de P relativa a I es el conjunto de reglas sin negación obtenidas a partir de P eliminando primero cada regla tal que al menos uno de los átomos en su ${\displaystyle C_{i}}$ cuerpo

${\displaystyle B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

pertenece a I , y luego eliminar las partes de los cuerpos de todas las reglas restantes. ${\displaystyle \operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

Decimos que I es un modelo estable de P si I es el modelo estable de la reducción de P relativa a I . (Dado que la reducción no contiene negación, su modelo estable ya ha sido definido.) Como sugiere el término "modelo estable", todo modelo estable de P es un modelo de P .

Ejemplo

Para ilustrar estas definiciones, verifiquemos que es un modelo estable del programa. ${\displaystyle \{p,s\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p,\operatorname {not} q.}$

La reducción de este programa en relación a es ${\displaystyle \{p,s\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p.}$

(De hecho, dado que , el reduct se obtiene del programa eliminando la parte ) El modelo estable del reduct es . (De hecho, este conjunto de átomos satisface todas las reglas del reduct y no tiene subconjuntos propios con la misma propiedad). Por lo tanto, después de calcular el modelo estable del reduct, llegamos al mismo conjunto con el que comenzamos. En consecuencia, ese conjunto es un modelo estable. ${\displaystyle q\not \in \{p,s\}}$ ${\displaystyle \operatorname {not} q.}$ ${\displaystyle \{p,s\}}$ ${\displaystyle \{p,s\}}$

Al comprobar de la misma forma los otros 15 conjuntos formados por átomos, se observa que este programa no tiene otros modelos estables. Por ejemplo, la reducción del programa relativa a es ${\displaystyle p,q,r,s}$ ${\displaystyle \{p,q,r\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q.}$

El modelo estable de la reducción es , que es diferente del conjunto con el que comenzamos. ${\displaystyle \{p\}}$ ${\displaystyle \{p,q,r\}}$

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

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

tiene dos modelos estables , . El programa de una regla ${\displaystyle \{p\}}$ ${\displaystyle \{q\}}$

${\displaystyle p\leftarrow \operatorname {not} p}$

No tiene modelos estables.

Si consideramos 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 tales programas. En ese paradigma de programación, un problema de búsqueda dado se representa mediante un programa lógico de modo que los modelos estables del programa corresponden a soluciones. Entonces, los programas con muchos modelos estables corresponden a problemas con muchas soluciones, y los programas sin modelos estables corresponden a problemas irresolubles. Por ejemplo, el rompecabezas de las ocho reinas tiene 92 soluciones; para resolverlo utilizando 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 entendemos un conjunto de reglas de la forma

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

¿Dónde están los átomos fundamentales? ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$

Átomos de cabeza

Si un átomo A pertenece a un modelo estable de un programa lógico P entonces A es la cabeza de una de las reglas de P.

Minimalismo

Cualquier modelo estable de un programa lógico P es mínimo entre los modelos de P relativos a la inclusión del conjunto.

La propiedad anticadena

Si I y J son modelos estables del mismo programa lógico, entonces I no es un subconjunto propio de J. En otras palabras, el conjunto de modelos estables de un programa es una anticadena .

NP-completitud

Probar si un programa de lógica fundamental finito 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 básico 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 inverso no es cierto. Por ejemplo, la finalización del programa de una regla

${\displaystyle p\leftarrow p}$

es la tautología . El modelo de esta tautología es un modelo estable de , pero su otro modelo no lo 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 completitud del programa. Los programas que satisfacen su condición se denominan ajustados . ${\displaystyle p\leftrightarrow p}$ ${\displaystyle \emptyset }$ ${\displaystyle p\leftarrow p}$ ${\displaystyle \{p\}}$

Fangzhen Lin y Yuting Zhao [2004] demostraron cómo fortalecer la terminación de un programa no estricto de modo que se eliminen todos sus modelos inestables. Las fórmulas adicionales que agregan a la terminación se denominan fórmulas de bucle .

Semántica bien fundamentada

El modelo bien fundado de un programa lógico divide todos los átomos fundamentales en tres conjuntos: verdadero, falso y desconocido. Si un átomo es verdadero en el modelo bien fundado de entonces pertenece a cada modelo estable de . La inversa, por lo general, no se cumple. Por ejemplo, el programa ${\displaystyle P}$ ${\displaystyle P}$

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

${\displaystyle r\leftarrow p}$

${\displaystyle r\leftarrow q}$

tiene dos modelos estables, y . Aunque pertenece a ambos, se desconoce su valor en el modelo bien fundado . ${\displaystyle \{p,r\}}$ ${\displaystyle \{q,r\}}$ ${\displaystyle r}$

Además, si un átomo es falso en el modelo bien fundado de un programa, entonces no pertenece a ninguno de sus modelos estables. Por lo tanto, el modelo bien fundado de un programa lógico proporciona un límite inferior para la intersección de sus modelos estables y un límite superior para su unión.

Negación fuerte

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 se sabe que los átomos que no pertenecen al conjunto son falsos. 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. ${\displaystyle p}$ ${\displaystyle p}$

En el contexto de la programación lógica, esta idea lleva a la necesidad de distinguir entre dos tipos de negación: la negación como fallo , analizada anteriormente, y la negación fuerte , que se denota aquí 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 aproxime ningún tren. Si no sabemos necesariamente si se aproxima un tren, entonces la regla que utiliza la negación como fallo ${\displaystyle \sim }$

${\displaystyle {\hbox{Cross}}\leftarrow {\hbox{not Train}}}$

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. La regla más débil, que utiliza la negación fuerte en el cuerpo, es preferible:

${\displaystyle {\hbox{Cross}}\leftarrow \,\sim {\hbox{Train}}.}$

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 cada una de las expresiones , , en una regla ${\displaystyle A}$ ${\displaystyle B_{i}}$ ${\displaystyle C_{i}}$

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

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 prefijados con el símbolo 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 , donde es un átomo positivo. Un conjunto de átomos se llama coherente si no contiene pares "complementarios" de átomos . Los modelos estables coherentes de un programa son idénticos a sus conjuntos de respuestas consistentes en el sentido de [Gelfond y Lifschitz, 1991]. ${\displaystyle {\sim }A}$ ${\displaystyle A}$ ${\displaystyle A,{\sim }A}$

Por ejemplo, el programa

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

${\displaystyle r}$

${\displaystyle {\sim }r\leftarrow \operatorname {not} p}$

tiene dos modelos estables, y . El primer modelo es coherente; el segundo no lo es, porque contiene tanto el átomo como el átomo . ${\displaystyle \{p,r\}}$ ${\displaystyle \{q,r,{\sim }r\}}$ ${\displaystyle r}$ ${\displaystyle {\sim }r}$

Supuesto de mundo cerrado

Según [Gelfond y Lifschitz, 1991], el supuesto de mundo cerrado para un predicado puede expresarse mediante la regla ${\displaystyle p}$

${\displaystyle \sim p(X_{1},\dots ,X_{n})\leftarrow \operatorname {not} p(X_{1},\dots ,X_{n})}$

(la relación no se cumple para una tupla si no hay evidencia de que así sea). Por ejemplo, el modelo estable del programa ${\displaystyle p}$ ${\displaystyle X_{1},\dots ,X_{n}}$

${\displaystyle p(a,b)}$

${\displaystyle p(c,d)}$

${\displaystyle \sim p(X,Y)\leftarrow \operatorname {not} p(X,Y)}$

consta de 2 átomos positivos

${\displaystyle p(a,b),p(c,d)}$

y 14 átomos negativos

${\displaystyle \sim p(a,a),{\sim }p(a,c),\dots }$

es decir, las fuertes negaciones de todos los demás átomos de tierra positivos formados a partir de . ${\displaystyle p,a,b,c,d}$

Un programa lógico con negación fuerte puede incluir las reglas del supuesto de mundo cerrado para algunos de sus predicados y dejar los otros predicados en el ámbito del supuesto de mundo abierto .

Programas con restricciones

La semántica del modelo estable se ha generalizado a muchos tipos de programas lógicos distintos de las colecciones de reglas "tradicionales" analizadas anteriormente (reglas de la forma

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

¿Dónde están los átomos? Una extensión sencilla permite que los programas contengan restricciones (reglas con la cabeza vacía): ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$

${\displaystyle \leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}.}$

Recordemos que una regla tradicional puede ser vista como una notación alternativa para una fórmula proposicional si identificamos la coma con la conjunción , el símbolo con la negación y acordamos tratarla como la implicación escrita 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: ${\displaystyle \land }$ ${\displaystyle \operatorname {not} }$ ${\displaystyle \neg }$ ${\displaystyle F\leftarrow G}$ ${\displaystyle G\rightarrow F}$

${\displaystyle \neg (B_{1}\land \cdots \land B_{m}\land \neg C_{1}\land \cdots \land \neg C_{n}).}$

Ahora podemos extender la definición de un modelo estable a programas con restricciones. Como en el caso de los programas tradicionales, para definir modelos estables, comenzamos con programas que no contienen negación. Un programa de este tipo puede ser inconsistente; entonces decimos que no tiene modelos estables. Si un programa de este tipo es consistente, entonces tiene un modelo mínimo único, y ese modelo se considera el único modelo estable de . ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$

A continuación, se definen modelos estables de programas arbitrarios con restricciones utilizando reducciones, formadas de la misma manera que en el caso de los programas tradicionales (véase la definición de un modelo estable más arriba). Un conjunto de átomos es un modelo estable de un programa con restricciones si la reducción de relativa a tiene un modelo estable, y ese modelo estable es igual a . ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle I}$

Las propiedades de la semántica del modelo estable mencionadas 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 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 . ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle C}$ ${\displaystyle P\cup \{C\}}$ ${\displaystyle P}$ ${\displaystyle C}$

Programas disyuntivos

En una regla disyuntiva , la cabeza puede ser la disyunción de varios átomos:

${\displaystyle A_{1};\dots ;A_{k}\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

(el punto y coma se considera una notación alternativa para la disyunción ). Las reglas tradicionales corresponden a , y las restricciones a . Para extender la semántica del modelo estable a los 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 reduct para programas disyuntivos sigue siendo la misma que antes. Un conjunto de átomos es un modelo estable de si es un modelo estable del reduct de relativo a . ${\displaystyle \lor }$ ${\displaystyle k=1}$ ${\displaystyle k=0}$ ${\displaystyle n=0}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$

Por ejemplo, el conjunto es un modelo estable del programa disyuntivo ${\displaystyle \{p,r\}}$

${\displaystyle p;q}$

${\displaystyle r\leftarrow \operatorname {not} q}$

porque es uno de los dos modelos mínimos de la reducción

${\displaystyle p;q}$

${\displaystyle r.}$

El programa anterior tiene un modelo más estable, . ${\displaystyle \{q\}}$

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 se encuentra 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 una anticadena. La comprobación de si un programa disyuntivo finito tiene un modelo estable es -completa [Eiter y Gottlob, 1993]. ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle \Sigma _{2}^{\rm {P}}}$

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 parece muy diferente de la definición original de un modelo estable. En lugar de reducciones, se refiere a la lógica del equilibrio , un sistema de lógica no monótona basado en los modelos de Kripke . La formulación de Ferraris, por otro lado, se basa en reducciones, aunque el proceso de construcción de la reducción 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 relativa a un conjunto de átomos es la fórmula obtenida de reemplazando cada subfórmula máxima que no se satisface por con la constante lógica (falso). La reducción de un conjunto de fórmulas proposicionales relativas a consiste en las reducciones de todas las fórmulas de relativas a . Como en el caso de los programas disyuntivos, decimos que un conjunto de átomos es un modelo estable de si es mínimo (con respecto a la inclusión del conjunto) entre los modelos de la reducción de relativa a . ${\displaystyle F}$ ${\displaystyle I}$ ${\displaystyle F}$ ${\displaystyle I}$ ${\displaystyle \bot }$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$

Por ejemplo, la reducción del conjunto

${\displaystyle \{p,p\land q\rightarrow r,p\land \neg q\rightarrow s\}}$

relativo a es ${\displaystyle \{p,s\}}$

${\displaystyle \{p,\bot \rightarrow \bot ,p\land \neg \bot \rightarrow s\}.}$

Dado que es un modelo de la reducción, y los subconjuntos propios de ese conjunto no son modelos de la reducción, es un modelo estable del conjunto dado de fórmulas. ${\displaystyle \{p,s\}}$ ${\displaystyle \{p,s\}}$

Hemos visto que también es un modelo estable de la misma fórmula, escrita en notación de programación lógica, en el sentido de la definición original. Se trata de 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 forma más general, para los programas con restricciones y para los programas disyuntivos. ${\displaystyle \{p,s\}}$

Propiedades de la semántica del modelo general estable

El teorema que afirma que todos los elementos de cualquier modelo estable de un programa son átomos cabeza de se puede extender a conjuntos de fórmulas proposicionales, si definimos los átomos cabeza de la siguiente manera. Un átomo es un átomo cabeza de un conjunto de fórmulas proposicionales si al menos una ocurrencia de en una fórmula de no está en el ámbito de una negación ni en el antecedente de una implicación. (Aquí asumimos que la equivalencia se trata como una abreviatura, no como un conectivo primitivo). ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle A}$ ${\displaystyle P}$ ${\displaystyle A}$ ${\displaystyle P}$

La propiedad de minimalidad y anticadena de los modelos estables de un programa tradicional no se cumple en el caso general. Por ejemplo, (el conjunto singleton que consiste en) la fórmula

${\displaystyle p\lor \neg p}$

tiene dos modelos estables, y . El último no es mínimo y es un superconjunto adecuado del primero. ${\displaystyle \emptyset }$ ${\displaystyle \{p\}}$

Probar si un conjunto finito de fórmulas proposicionales tiene un modelo estable es -completo , como en el caso de los programas disyuntivos. ${\displaystyle \Sigma _{2}^{\rm {P}}}$

Véase también

• Programación de conjuntos de respuestas
• Programación lógica
• La negación como fracaso

Notas

1. Este enfoque de la semántica de los programas lógicos sin negación se debe a Maarten van Emden y Robert Kowalski —van Emden & Kowalski 1976.
2. Gelfond y Lifschitz 1991 llaman clásica a la segunda negación y la denotan por . ${\displaystyle \neg }$

Referencias

• Bidoit, N.; Froidevaux, C. (1987). "El minimalismo subsume la lógica por defecto y la circunscripción". Actas: Simposio sobre lógica en informática , Ithaca, Nueva York, 22-25 de junio de 1987. IEEE Computer Society Press. págs. 89–97. ISBN 978-0-8186-0793-6.87CH2464-6.
• Eiter, T.; Gottlob, G. (1993). "Resultados de complejidad para programación lógica disyuntiva y aplicación a lógicas no monótonas". ILPS '93: Actas del simposio internacional de 1993 sobre programación lógica . MIT Press. págs. 266–278. ISBN 978-0-262-63152-5.
• van Emden, M.; Kowalski, R. (1976). "La semántica de la lógica de predicados como lenguaje de programación" (PDF) . Revista de la ACM . 23 (4): 733–742. CiteSeerX  10.1.1.64.9246 . doi :10.1145/321978.321991. S2CID  11048276.
• Fages, F. (1994). "Consistencia de la completitud de Clark y existencia de modelos estables". Revista de métodos de lógica en ciencias de la computación . 1 : 51–60. CiteSeerX  10.1.1.48.2157 .
• Ferraris, P. (2005). "Conjuntos de respuestas para teorías proposicionales". Programación lógica y razonamiento no monótono. LPNMR 2005. Lecture Notes in Computer Science. Vol. 3662. Springer. pp. 119–131. CiteSeerX  10.1.1.129.5332 . doi :10.1007/11546207_10. ISBN. 978-3-540-31827-9.
• Ferraris, P.; Lifschitz, V. (2005). "Fundamentos matemáticos de la programación de conjuntos de respuestas". ¡ Les mostraremos! Ensayos en honor a Dov Gabbay . King's College Publications. págs. 615–664. CiteSeerX  10.1.1.79.7622 .
• Gelfond, M. (1987). "Sobre las teorías autoepistémicas estratificadas" (PDF) . AAAI'87: Actas de la sexta conferencia nacional sobre inteligencia artificial . pp. 207–211. ISBN 978-0-934613-42-2.
• Gelfond, M.; Lifschitz, V. (1988). "La semántica del modelo estable para la programación lógica". Actas de la Quinta Conferencia Internacional sobre Programación Lógica (ICLP) . MIT Press. págs. 1070–80. ISBN 978-0-262-61054-4.
• Gelfond, M.; Lifschitz, V. (1991). "Negación clásica en programas lógicos y bases de datos disyuntivas". Computación de nueva generación . 9 (3–4): 365–385. CiteSeerX  10.1.1.49.9332 . doi :10.1007/BF03037169. S2CID  13036056.
• Hanks, S.; McDermott, D. (1987). "Lógica no monotónica y proyección temporal". Inteligencia Artificial . 33 (3): 379–412. doi :10.1016/0004-3702(87)90043-9.
• Lin, F.; Zhao, Y. (2004). "ASSAT: cálculo de conjuntos de respuestas de un programa lógico mediante solucionadores SAT" (PDF) . Inteligencia artificial . 157 (1–2): 115–137. doi :10.1016/j.artint.2004.04.004. S2CID  514581.
• Marek, V.; Subrahmanian, V.S. (1989). "La relación entre la semántica de los programas lógicos y el razonamiento no monótono". Programación lógica: Actas de la Sexta Conferencia Internacional . MIT Press. págs. 600–617. ISBN 978-0-262-62065-9.
• Pearce, D. (1997). "Una nueva caracterización lógica de modelos estables y conjuntos de respuestas" (PDF) . Extensiones no monótonas de la programación lógica . Apuntes de clase sobre inteligencia artificial. Vol. 1216. págs. 57–70. doi :10.1007/BFb0023801. ISBN. 978-3-540-68702-3.
• Reiter, R. (1980). "Una lógica para el razonamiento por defecto" (PDF) . Inteligencia Artificial . 13 (1–2): 81–132. doi :10.1016/0004-3702(80)90014-4.