La negación como fracaso

La negación como fallo ( NAF , por sus siglas en inglés) es una regla de inferencia no monótona en programación lógica , utilizada para derivar${\displaystyle \mathrm {no} ~p}$(es decir que${\displaystyle p}$se supone que no se cumple) por no derivar${\displaystyle p}$. Tenga en cuenta que${\displaystyle \mathrm {no} ~p}$puede ser diferente de la afirmación${\displaystyle \neg p}$de la negación lógica de${\displaystyle p}$, dependiendo de la exhaustividad del algoritmo de inferencia y, por lo tanto, también del sistema lógico formal.

La negación como fallo ha sido una característica importante de la programación lógica desde los inicios de Planner y Prolog . En Prolog, se suele implementar utilizando las construcciones extralógicas de Prolog.

En términos más generales, este tipo de negación se conoce como negación débil , ^{[ 1 ] [ 2 ]} en contraste con la negación fuerte (es decir, explícita, demostrable).

En Planner, la negación como fallo podría implementarse de la siguiente manera:

if (not (goal p)), then (assert ¬p)

que dice que si una búsqueda exhaustiva para probar pfalla, entonces afirmar ¬p. ^{[ 3 ]} Esto establece que la proposición pse asumirá como "no verdadera" en cualquier procesamiento posterior. Sin embargo, dado que Planner no se basa en un modelo lógico, una interpretación lógica de lo anterior sigue siendo oscura.

En Prolog puro, literales NAF de la forma${\displaystyle \mathrm {no} ~p}$puede aparecer en el cuerpo de las cláusulas y puede usarse para derivar otros literales NAF. Por ejemplo, dadas solo las cuatro cláusulas

${\displaystyle p\leftarrow q\land \mathrm {not} ~r}$

${\displaystyle q\leftarrow s}$

${\displaystyle q\leftarrow t}$

${\displaystyle t\leftarrow }$

NAF se deriva${\displaystyle \mathrm {not} ~s}$,${\displaystyle \mathrm {not} ~r}$y${\displaystyle p}$así como${\displaystyle t}$y${\displaystyle q}$.

La semántica de NAF siguió siendo un tema abierto hasta 1978, cuando Keith Clark demostró que es correcta con respecto a la finalización del programa lógico, donde, en términos generales, "solo" y${\displaystyle \leftarrow }$se interpretan como "si y solo si", escrito como "si y solo si" o "${\displaystyle \equiv }$".

Por ejemplo, la finalización de las cuatro cláusulas anteriores es

${\displaystyle p\equiv q\land \mathrm {not} ~r}$

${\displaystyle q\equiv s\lor t}$

${\displaystyle t\equiv \mathrm {true} }$

${\displaystyle r\equiv \mathrm {false} }$

${\displaystyle s\equiv \mathrm {false} }$

La regla de inferencia NAF simula el razonamiento explícitamente con la completitud, donde ambos lados de la equivalencia se niegan y la negación del lado derecho se distribuye hasta las fórmulas atómicas . Por ejemplo, para demostrar${\displaystyle \mathrm {not} ~p}$, NAF simula el razonamiento con las equivalencias

${\displaystyle \mathrm {not} ~p\equiv \mathrm {not} ~q\lor r}$

${\displaystyle \mathrm {not} ~q\equiv \mathrm {not} ~s\land \mathrm {not} ~t}$

${\displaystyle \mathrm {not} ~t\equiv \mathrm {false} }$

${\displaystyle \mathrm {not} ~r\equiv \mathrm {true} }$

${\displaystyle \mathrm {not} ~s\equiv \mathrm {true} }$

En el caso no proposicional, la compleción debe ampliarse con axiomas de igualdad para formalizar la suposición de que los individuos con nombres distintos son distintos. NAF simula esto mediante la falta de unificación. Por ejemplo, dadas solo las dos cláusulas

${\displaystyle p(a)\leftarrow }$

${\displaystyle p(b)\leftarrow t}$

NAF se deriva${\displaystyle \mathrm {not} ~p(c)}$.

La finalización del programa es

${\displaystyle p(X)\equiv X=a\lor X=b}$

ampliado con axiomas de nombres únicos y axiomas de cierre de dominio.

La semántica de completitud está estrechamente relacionada tanto con la circunscripción como con la suposición de mundo cerrado .

La semántica de finalización justifica la interpretación del resultado.${\displaystyle \mathrm {not} ~p}$de una inferencia NAF como la negación clásica${\displaystyle \neg p}$de${\displaystyle p}$Sin embargo, en 1987, Michael Gelfond demostró que también es posible interpretar${\displaystyle \mathrm {not} ~p}$literalmente como "${\displaystyle p}$no se puede mostrar",${\displaystyle p}$"no se sabe" o "${\displaystyle p}$no se cree", como en la lógica autoepistémica . La interpretación autoepistémica fue desarrollada aún más por Gelfond y Lifschitz en 1988, y es la base de la programación de conjuntos de respuestas .

La semántica autoepistémica de un programa Prolog puro P con literales NAF se obtiene "expandiendo" P con un conjunto de literales NAF básicos (libres de variables) Δ que es estable en el sentido de que

Δ = {no p | p no está implícito en P ∪ Δ}

En otras palabras, un conjunto de supuestos Δ sobre lo que no se puede demostrar es estable si y solo si Δ es el conjunto de todas las sentencias que realmente no se pueden demostrar a partir del programa P expandido por Δ. Aquí, debido a la sintaxis simple de los programas Prolog puros, "implícito por" puede entenderse de forma muy sencilla como derivabilidad utilizando únicamente el modus ponens y la instanciación universal .

Un programa puede tener cero, una o más expansiones estables. Por ejemplo,

${\displaystyle p\leftarrow \mathrm {not} ~p}$

no tiene expansiones estables.

${\displaystyle p\leftarrow \mathrm {not} ~q}$

tiene exactamente una expansión estable Δ = {no q }

${\displaystyle p\leftarrow \mathrm {not} ~q}$

${\displaystyle q\leftarrow \mathrm {not} ~p}$

tiene exactamente dos expansiones estables Δ ₁ = {no p } y Δ ₂ = {no q }.

La interpretación autoepistémica de NAF se puede combinar con la negación clásica, como en la programación lógica extendida y la programación de conjuntos de respuestas . Combinando las dos negaciones, es posible expresar, por ejemplo

${\displaystyle \neg p\leftarrow \mathrm {not} ~p}$ (la suposición del mundo cerrado) y

${\displaystyle p\leftarrow \mathrm {not} ~\neg p}$ (${\displaystyle p}$se mantiene por defecto).

• Informe del taller del W3C sobre lenguajes de reglas para la interoperabilidad. Incluye notas sobre NAF y SNAF (negación con alcance como fallo).