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 varios enfoques estándar sobre el significado de la negación en la programación lógica, junto con la finalización del programa y la semántica bien fundamentada . 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 familiares de 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 el encabezado de ninguna de las reglas. La consulta r también fallará, porque la única regla con r en el encabezado 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. (Este último tiene éxito porque el correspondiente objetivo positivo 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 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 la negación , y acordamos tratarlo como la implicación escrita al revés. Por ejemplo, la última regla del programa dado es, desde este punto de vista, 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 que se muestra arriba, veremos que cada regla obtiene el valor T. En otras palabras, esa tarea es un modelo del programa. Pero este programa también tiene otros modelos, por ejemplo

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 monótona

El significado de la negación en los programas lógicos está estrechamente relacionado con dos teorías del 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 nos permite distinguir entre lo verdadero y lo conocido. Michael Gelfond [1987] propuso leer el cuerpo de una regla como " no se conoce" 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. Se puede utilizar un incumplimiento para derivar su conclusión bajo el supuesto de que sus justificaciones son consistentes con lo que se sabe actualmente. Nicole Bidoit y Christine Froidevaux [1987] propusieron tratar los átomos negados en los cuerpos de reglas como justificaciones. Por ejemplo, la regla

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

Puede entenderse como el valor predeterminado que nos permite derivar del supuesto de 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 modelo estable que aparece a continuación, reproducida de [Gelfond y Lifschitz, 1988], utiliza dos convenciones. Primero, se identifica una asignación de verdad 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 utilizar 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 verdad 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 una abreviatura del conjunto de todas las instancias básicas de sus reglas, es decir, del resultado de sustituir variables por términos libres de 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 sustituir X en este programa por los términos básicos

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

de todas las formas posibles. El resultado es el programa terrestre 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}}$

¿Dónde están los átomos terrestres? 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 de reducción, 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 con respecto a I es el conjunto de reglas sin negación que se obtiene de P eliminando primero todas las reglas de modo que al menos uno de los átomos ⁠ ⁠ ${\displaystyle C_{i}}$ en su cuerpo

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

pertenece a I y luego eliminando 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 del reducto de P respecto de I. (Dado que el reducto 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, comprobemos 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 respecto a es ${\displaystyle \{p,s\}}$

${\displaystyle p}$

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

${\displaystyle s\leftarrow p.}$

(De hecho, desde , la reducción se obtiene del programa eliminando la pieza ) El modelo estable de la reducción es . (De hecho, este conjunto de átomos satisface todas las reglas del reducto y no tiene subconjuntos propios con la misma propiedad). Así, después de calcular el modelo estable del reducto 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\}}$

Verificando de la misma manera los otros 15 conjuntos formados por átomos se ve 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 del reducto 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 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 responder 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 de 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 corresponden 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 usando 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 anterior de modelo estable, por programa lógico nos referimos a 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 terrestres? ${\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.

Minimalidad

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 anticadena

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

NP-integridad

Probar si un programa lógico 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 terrestre 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

${\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 finalización del programa. Los programas que satisfacen su condición se llaman ajustados . ${\displaystyle p\leftrightarrow p}$ ${\displaystyle \emptyset }$ ${\displaystyle p\leftarrow p}$ ${\displaystyle \{p\}}$

Fangzhen Lin y Yuting Zhao [2004] mostraron cómo fortalecer la finalización de un programa no estricto para que se eliminen todos sus modelos inestables. Las fórmulas adicionales que añaden a la finalización se denominan fórmulas de bucle .

Semántica bien fundada

El modelo bien fundamentado de un programa lógico divide todos los átomos terrestres en tres conjuntos: verdadero, falso y desconocido. Si un átomo es verdadero en el modelo bien fundamentado de entonces pertenece a todo modelo estable de . Lo contrario, en 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 . Si bien pertenece a ambos, se desconoce su valor en el modelo fundamentado . ${\displaystyle \{p,r\}}$ ${\displaystyle \{q,r\}}$ ${\displaystyle r}$

Además, si un átomo es falso en el modelo bien fundamentado de un programa entonces no pertenece a ninguno de sus modelos estables. Así, el modelo bien fundamentado 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.

Negación fuerte

Representar 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 verdaderos. se sabe que es falso. Un estado de conocimiento posiblemente incompleto se puede describir 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 conduce a la necesidad de distinguir entre dos tipos de negación: la negación como fracaso , analizada 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 siempre que no se aproxime ningún tren. Si no sabemos necesariamente si se acerca un tren, entonces la regla que usa la negación como falla ${\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. Es preferible la regla más débil, que utiliza una fuerte negación en el cuerpo:

${\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 una fuerte negación en la teoría de modelos estables, Gelfond y Lifschitz [1991] permitieron que 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 con el prefijo del 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 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 hay 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 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 es válida 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 fundamentales positivos formados a partir de . ${\displaystyle p,a,b,c,d}$

Un programa lógico con negación fuerte puede incluir las reglas de 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 simple permite que los programas contengan restricciones : reglas con el encabezado vacío: ${\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}.}$

Recuerde que una regla tradicional puede verse como 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 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 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 así puede ser inconsistente; entonces decimos que no tiene modelos estables. Si dicho programa 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, los modelos estables de programas arbitrarios con restricciones se definen mediante reducciones, formadas de la misma manera que en el caso de los programas tradicionales (consulte la definición de modelo estable más arriba). Un conjunto de á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 a . ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle I}$

Las propiedades de la semántica del modelo estable mencionadas anteriormente para 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 y las restricciones . 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 de la reducción para programas disyuntivos sigue siendo la misma que antes. Un conjunto de átomos es un modelo estable de si es un modelo estable del reducto 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 del reducto

${\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 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 una anticadena. Probar si un programa disyuntivo finito tiene un modelo estable es completo [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 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 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, 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 relativa a un conjunto de átomos es la fórmula que se obtiene reemplazando cada subfórmula máxima que no se satisface 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 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 reducción de relativo 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 del reducto y los subconjuntos propios de ese conjunto no son modelos del reducto, es un modelo estable del conjunto de fórmulas dado. ${\displaystyle \{p,s\}}$ ${\displaystyle \{p,s\}}$

Hemos visto que también es 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 modelo estable según Ferraris es equivalente a la definición original. Lo mismo ocurre, en términos más generales, con los programas con restricciones y con los programas disyuntivos. ${\displaystyle \{p,s\}}$

Propiedades de la semántica general del modelo estable.

El teorema que afirma que todos los elementos de cualquier modelo estable de un programa son átomos principales puede extenderse a conjuntos de fórmulas proposicionales, si definimos los átomos principales de la siguiente manera. Un átomo es un átomo principal de un conjunto de fórmulas proposicionales si al menos una aparición de en una fórmula de no está en el alcance 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 minimalidad y la propiedad anticadena de los modelos estables de un programa tradicional no se mantienen en el caso general. Por ejemplo, (el conjunto singleton que consta de) la fórmula

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

tiene dos modelos estables, y . Este ú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}}}$

Ver también

• Programación del conjunto 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. clásica a la segunda negación y la denotan por . ${\displaystyle \neg }$

Referencias

• Bidoit, N.; Froidevaux, C. (1987). "El minimalismo incluye la lógica y la circunscripción predeterminadas". Actas: Simposio sobre lógica en informática , Ithaca, Nueva York, 22 al 25 de junio de 1987 . Prensa de la Sociedad de Computación IEEE. págs. 89–97. ISBN 978-0-8186-0793-6. 87CH2464-6.
• Eiter, T.; Gottlob, G. (1993). "Resultados de complejidad para la programación de lógica disyuntiva y su aplicación a lógicas no monótonas". ILPS '93: Actas del simposio internacional de 1993 sobre programación lógica . Prensa del MIT. 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 finalización de Clark y existencia de modelos estables". Revista de Métodos de Lógica en Informática . 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 . Apuntes de conferencias sobre informática. vol. 3662. Saltador. págs. 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". ¡Se los mostraremos! Ensayos en honor a Dov Gabbay . Publicaciones de King's College. 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 . págs. 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) . Prensa del MIT. 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 monótona y proyección temporal". Inteligencia artificial . 33 (3): 379–412. doi :10.1016/0004-3702(87)90043-9.
• Lin, F.; Zhao, Y. (2004). "ASSAT: Computación 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, VS (1989). "La relación entre la semántica del programa lógico y el razonamiento no monótono". Programación lógica: Actas de la Sexta Conferencia Internacional . Prensa del MIT. 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 conferencias 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 predeterminado" (PDF) . Inteligencia artificial . 13 (1–2): 81–132. doi :10.1016/0004-3702(80)90014-4.