La negación como fracaso

Regla de inferencia que trata la no demostrabilidad como falsedad

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 , que se utiliza para derivar (es decir, que se supone que no se cumple) del fallo para derivar . Nótese que puede ser diferente del enunciado de la negación lógica de , dependiendo de la completitud del algoritmo de inferencia y, por lo 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 falla 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 mediante 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 fracaso 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 asevere ¬p. ^[3] Esto establece que la proposición pse asumirá como "no verdadera" en cualquier procesamiento posterior. Sin embargo, como Planner no se basa en un modelo lógico, una interpretación lógica de lo precedente sigue siendo oscura.

Semántica de Prolog

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 solo 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 así como 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 y solo si" o " ". ${\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ícitamente con la completitud, donde ambos lados de la equivalencia se niegan y la negación en el lado derecho se distribuye hasta las 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, la compleción debe ser aumentada con axiomas de igualdad, para formalizar el supuesto de que los individuos con nombres distintos son distintos. NAF simula esto mediante el fracaso de la unificación. Por ejemplo, dadas solo 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}$

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 el supuesto de mundo cerrado .

Semántica autoepistémica

La semántica de completitud justifica la interpretación del resultado de una inferencia NAF como la negación clásica de . Sin embargo, en 1987, Michael Gelfond demostró que también es posible interpretar 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 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 (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 suposiciones Δ acerca de lo que no se puede demostrar es estable si y solo si Δ es el conjunto de todas las oraciones que verdaderamente no se pueden demostrar a partir del programa P desarrollado por Δ. Aquí, debido a la sintaxis simple de los programas Prolog puros, "implícito por" se puede entender muy simplemente como derivabilidad usando solo modus ponens e 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}$(el supuesto del mundo cerrado) y

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

Notas al pie

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 clase en informática. Vol. 2901. Apuntes de clase en 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 un fracaso" (PDF) . Lógica y bases de datos . Springer-Verlag . pp. 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 sobre razonamiento no monótono . Morgan Kaufmann. pp. 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 . AAAI Press. 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. 5th International Conference and Symposium on Logic Programming . MIT Press. 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 entre el supuesto de datos completos de Clark y el supuesto de mundo cerrado de Reiter". Journal of Logic Programming . 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).