Hispanopedia Wiki
Articulo de referencia

Semántica de modelos estables

El concepto de modelo estable , o conjunto de respuestas , se utiliza para definir una semántica declarativa para programas lógicos donde la negación se considera un fallo . Est...

Hispanopedia WikiContenido en espanolLectura gratuita

El concepto de modelo estable , o conjunto de respuestas , se utiliza para definir una semántica declarativa para programas lógicos donde la negación se considera un fallo . Este es uno de los 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 fundamentada . La semántica del modelo estable es la base de la programación con conjuntos de respuestas .

Motivación

La investigación sobre la semántica declarativa de la negación en la programación lógica se motivó 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 las reglas— no coincide completamente con las tablas de verdad familiares de la lógica proposicional clásica . Consideremos, por ejemplo, el programa

pag{\displaystyle p}
r←pag,q{\displaystyle r\leftarrow p,q}
s←pag,no⁡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 aparece 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 ,no⁡q{\displaystyle \operatorname {not} q}tiene éxito. (Este ú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:

Por otro lado, las reglas del programa dado pueden verse como fórmulas proposicionales si identificamos la coma con la conjunción.∧{\displaystyle \land }, el símbolono{\displaystyle \operatorname {not} }con negación¬{\displaystyle \neg }y aceptan tratarF←GRAMO{\displaystyle F\leftarrow G}como implicaciónGRAMO→F{\displaystyle G\rightarrow F}escrito 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.

pag∧¬q→s.{\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 anteriormente, 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

Así pues, uno de los modelos del programa en cuestión 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 del razonamiento no monótono : la lógica autoepistémica y la lógica por defecto . El descubrimiento de estas relaciones fue un paso fundamental hacia la invención de la semántica de modelos estables.

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 conoce. Michael Gelfond [1987] propuso leerno⁡pag{\displaystyle \operatorname {not} p}en el cuerpo de una regla como "pag{\displaystyle p}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 considerarse una reformulación de esta idea que evita referencias explícitas a la lógica autoepistémica.

En lógica de 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

s←pag,no⁡q{\displaystyle s\leftarrow p,\operatorname {not} q}

puede entenderse como el valor predeterminado que nos permite derivars{\displaystyle s}depag{\displaystyle p}suponiendo que¬q{\displaystyle \neg q}es consistente. La semántica del modelo estable utiliza la misma idea, pero no hace referencia explícita a la lógica predeterminada.

Modelos estables

La definición de un modelo estable que se presenta a continuación, reproducida de [Gelfond y Lifschitz, 1988], utiliza dos convenciones. Primero, 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{pag,s}{\displaystyle \{p,s\}}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∅{\displaystyle \emptyset }es la que hace que cada á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 forma abreviada de referirse al conjunto de todas las instancias básicas de sus reglas, es decir, al resultado de sustituir términos sin variables por variables en las reglas del programa de todas las maneras posibles. Por ejemplo, la definición de programación lógica de números pares.

incluso⁡(0){\displaystyle \operatorname {even} (0)}
incluso⁡(s(incógnita))←no⁡incluso⁡(incógnita){\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 básicos.

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

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

incluso⁡(0){\displaystyle \operatorname {even} (0)}
incluso⁡(s(0))←no⁡incluso⁡(0){\displaystyle \operatorname {even} (s(0))\leftarrow \operatorname {not} \operatorname {even} (0)}
incluso⁡(s(s(0)))←no⁡incluso⁡(s(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

A←B1,…,Bmetro,no⁡do1,…,no⁡donorte{\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

dóndeA,B1,…,Bmetro,do1,…,donorte{\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}son átomos fundamentales. Si P no contiene negación (norte=0{\displaystyle n=0}en cada regla del programa) entonces, por definición, el único modelo estable de P es su modelo que es mínimo con respecto a 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 reducto, definido como sigue.

Para cualquier conjunto I de átomos fundamentales, el reducto de P con respecto a I es el conjunto de reglas sin negación que se obtiene de P eliminando primero todas las reglas tales que al menos uno de los átomosdoi{\displaystyle C_{i}}en su cuerpo

B1,…,Bmetro,no⁡do1,…,no⁡donorte{\displaystyle B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

pertenece a mí , y luego dejando caer las partesno⁡do1,…,no⁡donorte{\displaystyle \operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}de los cuerpos de todas las reglas restantes.

Decimos que I es un modelo estable de P si I es el modelo estable del reducto de P con respecto a I. (Como el reducto no contiene negación, su modelo estable ya está 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{pag,s}{\displaystyle \{p,s\}}es un modelo estable del programa

pag{\displaystyle p}
r←pag,q{\displaystyle r\leftarrow p,q}
s←pag,no⁡q.{\displaystyle s\leftarrow p,\operatorname {not} q.}

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

pag{\displaystyle p}
r←pag,q{\displaystyle r\leftarrow p,q}
s←pag.{\displaystyle s\leftarrow p.}

(De hecho, ya queq∉{pag,s}{\displaystyle q\not \in \{p,s\}}, el reducto se obtiene del programa eliminando la parteno⁡q.{\displaystyle \operatorname {not} q.}) El modelo estable del reducto es{pag,s}{\displaystyle \{p,s\}}. (De hecho, este conjunto de átomos satisface todas las reglas del reducto, y no tiene subconjuntos propios con la misma propiedad.) Por lo tanto, después de calcular el modelo estable del reducto llegamos al mismo conjunto{pag,s}{\displaystyle \{p,s\}}con el que empezamos. Por consiguiente, ese conjunto es un modelo estable.

Comprobando de la misma manera los otros 15 conjuntos que constan de los átomospag,q,r,s{\displaystyle p,q,r,s}muestra que este programa no tiene otros modelos estables. Por ejemplo, el reducto del programa en relación con{pag,q,r}{\displaystyle \{p,q,r\}}es

pag{\displaystyle p}
r←pag,q.{\displaystyle r\leftarrow p,q.}

El modelo estable del reducto es{pag}{\displaystyle \{p\}}, que es diferente del conjunto{pag,q,r}{\displaystyle \{p,q,r\}}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

pag←no⁡q{\displaystyle p\leftarrow \operatorname {not} q}
q←no⁡pag{\displaystyle q\leftarrow \operatorname {not} p}

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

pag←no⁡pag{\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 ofrece una perspectiva diferente sobre este tipo de programas. En este 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. Así, 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 mediante 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 una sola 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

A←B1,…,Bmetro,no⁡do1,…,no⁡donorte{\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

dóndeA,B1,…,Bmetro,do1,…,donorte{\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}son átomos fundamentales.

á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 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 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 básica finita tiene un modelo estable es un problema NP-completo .

Relación con otras teorías de la negación como fracaso.

Finalización del programa

Cualquier modelo estable de un programa base finito no es solo 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

pag←pag{\displaystyle p\leftarrow p}

es la tautologíapag↔pag{\displaystyle p\leftrightarrow p}El modelo∅{\displaystyle \emptyset }de esta tautología es un modelo estable depag←pag{\displaystyle p\leftarrow p}pero su otro modelo{pag}{\displaystyle \{p\}}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 la 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 compleción de un programa no ajustado para eliminar todos sus modelos inestables. Las fórmulas adicionales que agregan a la compleción se denominan fórmulas de bucle .

Semántica bien fundamentada

El modelo bien fundamentado 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 fundamentado dePAG{\displaystyle P}entonces pertenece a todo modelo estable dePAG{\displaystyle P}Lo contrario, en general, no es cierto. Por ejemplo, el programa

pag←no⁡q{\displaystyle p\leftarrow \operatorname {not} q}
q←no⁡pag{\displaystyle q\leftarrow \operatorname {not} p}
r←pag{\displaystyle r\leftarrow p}
r←q{\displaystyle r\leftarrow q}

tiene dos modelos estables,{pag,r}{\displaystyle \{p,r\}}y{q,r}{\displaystyle \{q,r\}}. A pesar der{\displaystyle r}pertenece a ambos, su valor en el modelo bien fundamentado es desconocido .

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

Negación fuerte

Representación de información incompleta

Desde la perspectiva de la representación del conocimiento , un conjunto de átomos básicos 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 átomopag{\displaystyle p}si no pertenece al conjunto y su negación tampoco pertenece al conjunto, entonces no se sabe sipag{\displaystyle p}es verdadero o falso.

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 , discutida anteriormente, y la negación fuerte , que se denota aquí por∼{\displaystyle \sim }[ 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 utiliza la negación como fallo

Cruz←no es un tren{\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 una negación fuerte en el cuerpo, es preferible:

Cruz←∼Tren.{\displaystyle {\hbox{Cross}}\leftarrow \,\sim {\hbox{Train}}.}

Dice que se puede 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 expresionesA{\displaystyle A},Bi{\displaystyle B_{i}},doi{\displaystyle C_{i}}en una regla

A←B1,…,Bmetro,no⁡do1,…,no⁡donorte{\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 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∼A{\displaystyle {\sim }A}, dóndeA{\displaystyle A}es un átomo positivo. Un conjunto de átomos se denomina coherente si no contiene pares de átomos "complementarios".A,∼A{\displaystyle A,{\sim }A}. Los modelos estables coherentes de un programa son idénticos a sus conjuntos de respuestas consistentes en el sentido de [Gelfond y Lifschitz, 1991].

Por ejemplo, el programa

pag←no⁡q{\displaystyle p\leftarrow \operatorname {not} q}
q←no⁡pag{\displaystyle q\leftarrow \operatorname {not} p}
r{\displaystyle r}
∼r←no⁡pag{\displaystyle {\sim }r\leftarrow \operatorname {not} p}

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

Suposición de mundo cerrado

Según [Gelfond y Lifschitz, 1991], la suposición de mundo cerrado para un predicadopag{\displaystyle p}puede expresarse mediante la regla

∼pag(incógnita1,…,incógnitanorte)←no⁡pag(incógnita1,…,incógnitanorte){\displaystyle \sim p(X_{1},\dots ,X_{n})\leftarrow \operatorname {not} p(X_{1},\dots ,X_{n})}

(la relaciónpag{\displaystyle p}no se cumple para una tuplaincógnita1,…,incógnitanorte{\displaystyle X_{1},\dots ,X_{n}}si no hay evidencia de que lo haga). Por ejemplo, el modelo estable del programa

pag(a,b){\displaystyle p(a,b)}
pag(do,d){\displaystyle p(c,d)}
∼pag(incógnita,Y)←no⁡pag(incógnita,Y){\displaystyle \sim p(X,Y)\leftarrow \operatorname {not} p(X,Y)}

consta de 2 átomos positivos

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

y 14 átomos negativos

∼pag(a,a),∼pag(a,do),…{\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 depag,a,b,do,d{\displaystyle p,a,b,c,d}.

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

Programas con restricciones

La semántica de modelos estables se ha generalizado a muchos tipos de programas lógicos distintos de las colecciones de reglas "tradicionales" discutidas anteriormente: reglas de la forma

A←B1,…,Bmetro,no⁡do1,…,no⁡donorte{\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

dóndeA,B1,…,Bmetro,do1,…,donorte{\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}son átomos. Una extensión simple permite que los programas contengan restricciones : reglas con la cabeza vacía:

←B1,…,Bmetro,no⁡do1,…,no⁡donorte.{\displaystyle \leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}.}

Recordemos que una regla tradicional puede considerarse una notación alternativa para una fórmula proposicional si identificamos la coma con la conjunción.∧{\displaystyle \land }, el símbolono{\displaystyle \operatorname {not} }con negación¬{\displaystyle \neg }y aceptan tratarF←GRAMO{\displaystyle F\leftarrow G}como implicaciónGRAMO→F{\displaystyle G\rightarrow F}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:

¬(B1∧⋯∧Bmetro∧¬do1∧⋯∧¬donorte).{\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. Al igual que en el caso de los programas tradicionales, para definir modelos estables, comenzamos con programas que no contienen negación. Dicho programa puede ser inconsistente; entonces decimos que no tiene modelos estables. Si tal programaPAG{\displaystyle P}es consistente entoncesPAG{\displaystyle P}tiene un modelo mínimo único, y ese modelo se considera el único modelo estable dePAG{\displaystyle P}.

A continuación, se definen modelos estables de programas arbitrarios con restricciones utilizando reductos, formados 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 conjuntoI{\displaystyle I}de átomos es un modelo estable de un programaPAG{\displaystyle P}con restricciones si el reducto dePAG{\displaystyle P}relativo aI{\displaystyle I}tiene un modelo estable, y ese modelo estable es igual aI{\displaystyle I}.

Las propiedades de la semántica del modelo estable mencionadas anteriormente para los programas tradicionales se mantienen también 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ógicoPAG{\displaystyle P}afecta la colección de modelos estables dePAG{\displaystyle P}De una manera muy simple: elimina los modelos estables que violan la restricción. En otras palabras, para cualquier programaPAG{\displaystyle P}con restricciones y cualquier restriccióndo{\displaystyle C}, los modelos estables dePAG∪{do}{\displaystyle P\cup \{C\}}pueden caracterizarse como los modelos estables dePAG{\displaystyle P}que satisfacendo{\displaystyle C}.

Programas disyuntivos

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

A1;…;Ak←B1,…,Bmetro,no⁡do1,…,no⁡donorte{\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)∨{\displaystyle \lor }). Las reglas tradicionales corresponden ak=1{\displaystyle k=1}y restricciones ak=0{\displaystyle k=0}. Para extender la semántica del modelo estable a programas disyuntivos [Gelfond y Lifschitz, 1991], primero definimos que en ausencia de negación (norte=0{\displaystyle n=0}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 conjuntoI{\displaystyle I}de átomos es un modelo estable dePAG{\displaystyle P}siI{\displaystyle I}es un modelo estable del reducto dePAG{\displaystyle P}relativo aI{\displaystyle I}.

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

pag;q{\displaystyle p;q}
r←no⁡q{\displaystyle r\leftarrow \operatorname {not} q}

porque es uno de los dos modelos mínimos del reducto

pag;q{\displaystyle p;q}
r.{\displaystyle r.}

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

Al igual que en el caso de los programas tradicionales, cada elemento de cualquier modelo estable de un programa disyuntivoPAG{\displaystyle P}es un átomo de cabeza dePAG{\displaystyle P}, en el sentido de que aparece en la cabecera de una de las reglas dePAG{\displaystyle P}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Σ2PAG{\displaystyle \Sigma _{2}^{\rm {P}}}-completo [ Eiter y Gottlob, 1993].

Modelos estables de un conjunto de fórmulas proposicionales

Las reglas, incluso las disyuntivas , poseen una forma sintáctica bastante particular en comparación con las fórmulas proposicionales arbitrarias . Cada regla disyuntiva es esencialmente una implicación cuyo antecedente (el cuerpo de la regla) es una conjunción de literales , y cuyo consecuente (cabeza) es una disyunción de átomos. David Pearce [1997] y Paolo Ferraris [2005] demostraron cómo extender la definición de un modelo estable a conjuntos de fórmulas proposicionales arbitrarias. Esta generalización tiene aplicaciones en la programación de conjuntos .

La formulación de Pearce difiere notablemente de la definición original de modelo estable . En lugar de reductos, se refiere a la lógica de equilibrio , un sistema de lógica no monótona basado en modelos de Kripke . La formulación de Ferraris, por otro lado, se basa en reductos, aunque el proceso de construcción del reducto que utiliza difiere del descrito anteriormente . Ambos enfoques para definir modelos estables para conjuntos de fórmulas proposicionales son equivalentes.

Definición general de un modelo estable

Según [Ferraris, 2005], la reducción de una fórmula proposicionalF{\displaystyle F}relativo a un conjuntoI{\displaystyle I}de átomos es la fórmula obtenida deF{\displaystyle F}reemplazando cada subfórmula máxima que no se satisface porI{\displaystyle I}con la constante lógica⊥{\displaystyle \bot }(falso). El reducto de un conjuntoPAG{\displaystyle P}de fórmulas proposicionales relativas aI{\displaystyle I}consiste en los reductos de todas las fórmulas dePAG{\displaystyle P}relativo aI{\displaystyle I}. Como en el caso de los programas disyuntivos, decimos que un conjuntoI{\displaystyle I}de átomos es un modelo estable dePAG{\displaystyle P}siI{\displaystyle I}es mínimo (con respecto a la inclusión de conjuntos) entre los modelos del reducto dePAG{\displaystyle P}relativo aI{\displaystyle I}.

Por ejemplo, el reducto del conjunto

{pag,pag∧q→r,pag∧¬q→s}{\displaystyle \{p,p\land q\rightarrow r,p\land \neg q\rightarrow s\}}

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

{pag,⊥→⊥,pag∧¬⊥→s}.{\displaystyle \{p,\bot \rightarrow \bot ,p\land \neg \bot \rightarrow s\}.}

Desde{pag,s}{\displaystyle \{p,s\}}es un modelo del reducto, y los subconjuntos propios de ese conjunto no son modelos del reducto,{pag,s}{\displaystyle \{p,s\}}es un modelo estable del conjunto de fórmulas dado.

Hemos visto que{pag,s}{\displaystyle \{p,s\}}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 . Este es un ejemplo de un hecho general: al aplicarse 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 ocurre, de forma más general, con programas con restricciones y con 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 programaPAG{\displaystyle P}son átomos de cabeza dePAG{\displaystyle P}puede extenderse a conjuntos de fórmulas proposicionales, si definimos los átomos de cabeza de la siguiente manera. Un átomoA{\displaystyle A}es un átomo de cabeza de un conjuntoPAG{\displaystyle P}de fórmulas proposicionales si al menos una ocurrencia deA{\displaystyle A}en una fórmula dePAG{\displaystyle P}No se encuentra ni dentro del 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 conector primitivo).

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

pag∨¬pag{\displaystyle p\lor \neg p}

tiene dos modelos estables,∅{\displaystyle \emptyset }y{pag}{\displaystyle \{p\}}. Este último no es mínimo, y es un superconjunto propio del primero.

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

Véase también

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

Referencias

  • Bidoit, N.; Froidevaux, C. (1987). «El minimalismo engloba la lógica por defecto y la circunscripción». Actas del Simposio sobre Lógica en Ciencias de la Computación , 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 la programación 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 . MIT Press. pp. 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) . Journal of the 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" . Journal of Methods of Logic in Computer Science . 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" . ¡Se los mostraremos! Ensayos en honor a Dov Gabbay . Publicaciones del 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 . pp. 207–211 . ISBN  978-0-934613-42-2.
  • Gelfond, M.; Lifschitz, V. (1988). «La semántica de modelos estables 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" . New Generation Computing . 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: 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, VS (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 . Notas de clase en inteligencia artificial. Vol.  1216. pp. 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 .