Negazione come fallimento

La negazione come fallimento^[1] (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 $\mathrm {not} ~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).

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, tipica della logica classica.^[2]^[3]

Descrizione modifica

Questo metodo è la tipica implementazione in Prolog della closed-world assumption (CWA), secondo cui ogni atomo che non è conseguenza logica diretta del programma è considerato falso. Quest'ultima, in generale, non può essere implementata alla lettera, poiché 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:

KB:=\{Cane(pluto),Cane(lassie),Cane(rex),Gatto(silvestro)\}

in teoria, è impossibile valutare a priori la dichiarazione $\neg Cane(silvestro)$ , poiché è impossibile dire a priori se $Cane(silvestro)$ è derivabile (quindi vero) o non derivabile (quindi falso, per la CWA) dalle altre asserzioni.

Per questo motivo, nei linguaggi di programmazione logica sono stati implementati modelli più limitati della CWA ma che garantiscono la terminazione del programma e la correttezza della risposta. La negation as failure, infatti, per verificare $\mathrm {not} ~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 modifica

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 ha alcun riferimento nell'extensional database.

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

?- not nonno(a,b).

sarà

yes.

Note modifica

^ Russel-Norvig, p. 453.
^ M. Bílková, A. Colacito. Proof Theory for Positive Logic with Weak Negation. Studia Logica, Springer, 108, pages 649–686 (2020).
^ G. Wagner. Web Rules Need Two Kinds of Negation. Eindhoven University of Technology, Faculty of Technology Managem. In F. Bry, N. Henze and J. Maluszynski (Eds.), Principles and Practice of Semantic Web Reasoning. Proc. of the 1st International Workshop, PPSW3 '03. Springer-Verlag LNCS 2901, 2003.

Bibliografia modifica

(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 modifica

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

[1] Russel-Norvig, p. 453.

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

[3] G. Wagner. Web Rules Need Two Kinds of Negation. Eindhoven University of Technology, Faculty of Technology Managem. In F. Bry, N. Henze and J. Maluszynski (Eds.), Principles and Practice of Semantic Web Reasoning. Proc. of the 1st International Workshop, PPSW3 '03. Springer-Verlag LNCS 2901, 2003.

[1]

[2]

[3]