La negación como fracaso

Regla de inferencia que trata la no demostrabilidad como falsedad

La negación como fracaso ( NAF , para abreviar) es una regla de inferencia no monótona en programación lógica , que se utiliza para derivar (es decir, que se supone que no se cumple) a partir de una falla en la derivación . Tenga en cuenta que puede ser diferente del enunciado de la negación lógica de , dependiendo de la integridad del algoritmo de inferencia y, por tanto, también del sistema lógico formal. ${\displaystyle \mathrm {not} ~p}$ ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle \mathrm {not} ~p}$ ${\displaystyle \neg p}$ ${\displaystyle p}$

La negación como fracaso ha sido una característica importante de la programación lógica desde los primeros días de Planner y Prolog . En Prolog, generalmente se implementa utilizando construcciones extralógicas de Prolog.

De manera más general, 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).

Semántica del planificador

En Planner, la negación como falla 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 "falsa" 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.

Semántica del prólogo

En Prolog puro, los literales NAF de la forma pueden aparecer en el cuerpo de las cláusulas y pueden usarse para derivar otros literales NAF. Por ejemplo, dadas sólo las cuatro cláusulas ${\displaystyle \mathrm {not} ~p}$

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

${\displaystyle q\leftarrow s}$

${\displaystyle q\leftarrow t}$

${\displaystyle t\leftarrow }$

NAF deriva , y además de y . ${\displaystyle \mathrm {not} ~s}$ ${\displaystyle \mathrm {not} ~r}$ ${\displaystyle p}$ ${\displaystyle t}$ ${\displaystyle q}$

Semántica de finalización

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, "sólo" y se interpretan como "si y sólo si", escrito como "Si por " ". ${\displaystyle \leftarrow }$ ${\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ícito con la finalización, donde ambos lados de la equivalencia se niegan y la negación del lado derecho se distribuye hasta fórmulas atómicas . Por ejemplo, para mostrar , NAF simula el razonamiento con las equivalencias ${\displaystyle \mathrm {not} ~p}$

${\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, es necesario aumentar la compleción con axiomas de igualdad, para formalizar la suposición de que los individuos con nombres distintos son distintos. La NAF simula esto por el fracaso de la unificación. Por ejemplo, dadas sólo las dos cláusulas

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

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

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

La finalización del programa es

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

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

La semántica de compleción está estrechamente relacionada tanto con la circunscripción como con el supuesto de mundo cerrado .

Semántica autoepistémica

La semántica de compleción justifica interpretar el resultado de una inferencia NAF como la negación clásica de . Sin embargo, en 1987, Michael Gelfond demostró que también es posible interpretarlo literalmente como " no se puede demostrar", " no se sabe" o " 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 . ${\displaystyle \mathrm {not} ~p}$ ${\displaystyle \neg p}$ ${\displaystyle p}$ ${\displaystyle \mathrm {not} ~p}$ ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle p}$

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 (sin 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 mostrar es estable si y sólo si Δ es el conjunto de todas las oraciones que realmente no se pueden mostrar a partir del programa P expandido por Δ. Aquí, debido a la sintaxis simple de los programas Prolog puros, "implícito por" puede entenderse de manera muy simple como derivabilidad usando modus ponens y instanciación universal únicamente.

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}$(el supuesto del mundo cerrado) y

${\displaystyle p\leftarrow \mathrm {not} ~\neg p}$( se mantiene de forma predeterminada). ${\displaystyle p}$

Notas a pie de página

1. Bílková, M.; Colacito, A. (2020). "Teoría de la prueba de la lógica positiva con negación débil". Estudios Lógica . 108 (4): 649–686. arXiv : 1907.05411 . doi :10.1007/s11225-019-09869-y. S2CID  195886568.
2. Wagner, G. (2003). "Las reglas web necesitan dos tipos de negación" (PDF) . En Bry, F.; Henze, N.; Maluszynski, J. (eds.). Principios y práctica del razonamiento de la web semántica. PPSW3 2003 . Apuntes de conferencias sobre informática. vol. 2901. Apuntes de conferencias sobre informática: Springer. págs. 33–50. doi :10.1007/978-3-540-24572-8_3. ISBN 978-3-540-24572-8.
3. Clark, Keith (1978). «La negación como fracaso» (PDF) . Lógica y Bases de Datos . Springer-Verlag . págs. 293–322. doi :10.1007/978-1-4684-3384-5_11. ISBN 978-1-4684-3384-5.

Referencias

• Clark, K. (1987) [1978]. "La negación como fracaso". En Ginsberg, ML (ed.). Lecturas de razonamiento no monótono . Morgan Kaufman. págs. 311–325. ISBN 978-0-934613-45-3.
• Gelfond, M. (1987). "Sobre las teorías autoepistémicas estratificadas" (PDF) . AAAI'87: Actas de la sexta conferencia nacional sobre inteligencia artificial . Prensa AAAI. 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". En Kowalski, R.; Bowen, K. (eds.). Proc. V Congreso y Simposio Internacional sobre Programación Lógica . Prensa del MIT. págs. 1070–80. CiteSeerX  10.1.1.24.6050 . ISBN 978-0-262-61054-4.
• Shepherdson, JC (1984). "La negación como fracaso: una comparación de la base de datos completada de Clark y el supuesto de mundo cerrado de Reiter". Revista de programación lógica . 1 : 51–81. doi :10.1016/0743-1066(84)90023-2.
• Shepherdson, JC (1985). "La negación como fracaso II". Revista de programación lógica . 2 (3): 185–202. doi :10.1016/0743-1066(85)90018-4.

enlaces externos

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