La negación como falla ( NAF , para abreviar) es una regla de inferencia no monótona en la programación lógica , utilizada para derivar (es decir, que se supone que no se cumple) por no derivar . Tenga en cuenta que puede ser diferente de la declaración 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.
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 utilizando construcciones extralogicas 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 se podría implementar de la siguiente manera:
if (not (goal p)), then (assert ¬p)
que dice que si una búsqueda exhaustiva para probar p
falla, entonces afirme ¬p
. [3] Esto establece que la proposición p
se 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 anterior sigue siendo oscura.
Semántica de prólogo
En Prolog puro, los literales NAF de la forma puede aparecer en el cuerpo de las cláusulas y se puede utilizar para derivar otros literales NAF. Por ejemplo, dadas solo las cuatro cláusulas
NAF deriva , y así como y .
Semántica de finalización
La semántica de NAF siguió siendo un tema abierto hasta 1978, cuando Keith Clark demostró que es correcto con respecto a la finalización del programa lógico, donde, en términos generales, "sólo" y se interpretan como "si y solo si", escritos como "si" o "".
Por ejemplo, completar las cuatro cláusulas anteriores es
La regla de inferencia NAF simula el razonamiento explícitamente con la terminación, donde se niegan ambos lados de la equivalencia y la negación del lado derecho se distribuye en fórmulas atómicas . Por ejemplo, para mostrar, NAF simula el razonamiento con las equivalencias
En el caso no proposicional, la compleción debe aumentarse con axiomas de igualdad, para formalizar el supuesto de que los individuos con nombres distintos son distintos. NAF simula esto por falla de unificación. Por ejemplo, dadas solo las dos cláusulas
- t
NAF deriva .
La finalización del programa es
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 del mundo cerrado .
Semántica autoepistémica
La semántica de finalización 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 mostrar "," no se conoce "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 .
La semántica autoepistémica de un programa Prolog puro P con literales NAF se obtiene "expandiendo" P con un conjunto de literales NAF fundamentales (libres de variables) Δ que es estable en el sentido de que
- Δ = { | no está implícito en P ∪ Δ}
En otras palabras, un conjunto de supuestos Δ sobre lo que no se puede mostrar es estable si y solo si Δ es el conjunto de todas las oraciones que realmente no se pueden mostrar desde el programa P expandido por Δ. Aquí, debido a la sintaxis simple de los programas Prolog puros, "implícito por" puede entenderse muy simplemente como derivabilidad usando modus ponens y instanciación universal solamente.
Un programa puede tener cero, una o más expansiones estables. Por ejemplo,
no tiene expansiones estables.
tiene exactamente una expansión estable Δ = {}
tiene exactamente dos expansiones estables Δ 1 = {} y Δ 2 = {}.
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
- (la suposición del mundo cerrado) y
- ( se mantiene por defecto).
Notas al pie
- ^ M. Bílková, A. Colacito. Teoría de la prueba para lógica positiva con negación débil . Studia Logica , Springer, 108, páginas 649–686 (2020).
- ^ G. Wagner. Las reglas web necesitan dos tipos de negación . Universidad Tecnológica de Eindhoven, Facultad de Gestión Tecnológica. En F. Bry, N. Henze y J. Maluszynski (Eds.), Principles and Practice of Semantic Web Reasoning. Proc. del 1er Taller Internacional, PPSW3 '03. Springer-Verlag LNCS 2901, 2003.
- ^ Clark, Keith (1978). Bases de datos y lógica (PDF) . Springer-Verlag . págs. 293–322 (La negación como un fracaso). doi : 10.1007 / 978-1-4684-3384-5_11 .
Referencias
- K. Clark [1978, 1987]. Negación como fracaso . Lecturas en razonamiento no monotónico , Morgan Kaufmann Publishers, páginas 311-325.
- M. Gelfond [1987] Sobre teorías autoepistémicas estratificadas Proc. AAAI 1987, páginas 207-211.
- M. Gelfond y V. Lifschitz [1988] La semántica del modelo estable para el proceso de programación lógica . Quinta Conferencia y Simposio Internacional sobre Programación Lógica (R. Kowalski y K. Bowen, eds), MIT Press, páginas 1070-1080.
- JC Shepherdson [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 , Journal of Logic Programming, vol 1, 1984, páginas 51–81.
- JC Shepherdson [1985] Negation as Failure II , Journal of Logic Programming, vol 3, 1985, páginas 185-202.
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).