Negazione come fallimento

La negazione come fallimento (nota anche come NaF, dall'inglese negation as failure, o negation by default) è una regola di inferenza non monotòna utilizzata nella programmazione logica per derivare $n o t p$ dal fallimento nel derivare $p$ , dove $p$ è un atomo che non si può dedurre automaticamente dal programma (poiché non è conseguenza logica dei fatti e delle regole contenute nel programma). Ciò dipende dalla completezza della procedura di dimostrazione, quindi anche dal sistema logico formale di riferimento.

Il concetto di negation as failure è stato introdotto da Keith L. Clark nell'omonimo articolo del 1978. Più in generale, questo tipo di negazione è nota come negazione debole (in inglese weak negation), in contrapposizione alla negazione forte $\neg$ , tipica della logica classica.

Descrizione

Questo metodo è la tipica implementazione in Prolog della assunzione del mondo chiuso (CWA), secondo cui ogni atomo che non è conseguenza logica del programma è considerato falso. Quest'ultima non può essere implementata sic et simpliciter, poiché conseguenza logica e dimostrazione sono interscambiabili solo se la procedura di dimostrazione è corretta e completa e, in generale, la deduzione logica di un atomo a partire da un qualsiasi programma dato è un problema non risolvibile in tempo finito.

Ad esempio, data la seguente base di conoscenza logica:

K B := {C a n e (p l u t o), C a n e (l a s s i e), C a n e (r e x), G a t t o (s i l v e s t r o)}

in teoria, è impossibile valutare a priori la formula logica $\neg C a n e (s i l v e s t r o)$ , poiché è impossibile derivare $C a n e (s i l v e s t r o)$ dalle altre asserzioni (non essendone conseguenza logica).

Per questo motivo, nei linguaggi di programmazione logica sono state implementate nelle procedure di dimostrazione forme più limitate della CWA che garantiscono risposte corrette in tempo finito. La NaF, infatti, per verificare $n o t p$ (ovvero, per verificare che $p$ non è derivabile) utilizza la risoluzione SLD esaminando soltanto i cosiddetti alberi di fallimento finito con radice $p$ . Per questo motivo, la regola è detta più propriamente negazione come fallimento finito.

Prolog

Ad esempio, dato il seguente programma Prolog:

nonno(X,Z) :- padre(X,Y), genitore(Y,Z).
genitore(X,Y) :- padre(X,Y).
genitore(X,Y) :- madre(X,Y).
padre(a,b).
madre(b,c).

per rispondere alla domanda ?- not nonno(a,b)., dovrà espandere l'albero con radice nonno(a,b), da cui segue padre(a,X), genitore(X,b) e poi, indeterministicamente, padre(X,b) e madre(X,b). Entrambi i rami dell'albero falliscono: il primo perché non esiste alcuna X che soddisfi contemporaneamente padre(a,X) e padre(X,b); il secondo perché madre(X,b) non si unifica con alcun fatto (o testa).

Segue che nonno(a,b) risulta falso e la risposta a

?- not nonno(a,b).

sarà

yes.

Note

↑ Russel-Norvig, p. 453.
↑ John C. Shepherdson, Negation as failure: a comparison of Clark's completed data base and Reiter's closed world assumption, in The Journal of Logic Programming, vol. 1, n. 1, 1984, pp. 51–79, DOI:10.1016/0743-1066(84)90023-2.
↑ M. Bílková, A. Colacito. Proof Theory for Positive Logic with Weak Negation. Studia Logica, Springer, 108, pages 649–686 (2020).
↑ (EN) G. Wagner, Web Rules Need Two Kinds of Negation, in F. Bry,, N. Henze e J. Maluszynski (a cura di), Principles and Practice of Semantic Web Reasoning. Proc. of the 1st International Workshop, PPSW3 '03, collana LNCS, vol. 2901, Springer-Verlag, 2003, pp. 33–50, DOI:10.1007/978-3-540-24572-8_3.

Bibliografia

(EN) K.L. Clark, Negation as failure (PDF), in Logic and Data Bases, Gallaire and Minker, 1978, ISBN 978-1-4684-3386-9.
Stuart Russel, Peter Norvig, Intelligenza artificiale - Un approccio moderno, vol. 1, 2ª ed., Milano, Pearson Education Italia, 2005, ISBN 88-7192-228-X.

Voci correlate

Portale Informatica: accedi alle voci di Wikipedia che trattano di informatica

[1] Russel-Norvig, p. 453.

[2] John C. Shepherdson, Negation as failure: a comparison of Clark's completed data base and Reiter's closed world assumption, in The Journal of Logic Programming, vol. 1, n. 1, 1984, pp. 51–79, DOI:10.1016/0743-1066(84)90023-2.

[3] M. Bílková, A. Colacito. Proof Theory for Positive Logic with Weak Negation. Studia Logica, Springer, 108, pages 649–686 (2020).

[4] (EN) G. Wagner, Web Rules Need Two Kinds of Negation, in F. Bry,, N. Henze e J. Maluszynski (a cura di), Principles and Practice of Semantic Web Reasoning. Proc. of the 1st International Workshop, PPSW3 '03, collana LNCS, vol. 2901, Springer-Verlag, 2003, pp. 33–50, DOI:10.1007/978-3-540-24572-8_3.