Negazione come fallimento

Da Wikipedia, l'enciclopedia libera.
Jump to navigation Jump to search

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 dal fallimento nel derivare , dove è un atomo che non si può dedurre automaticamente dal programma (poiché non è conseguenza logica dei fatti e delle regole contenute nel programma).

Questo metodo è la tipica implementazione della closed-world assumption (CWA), secondo cui ogni atomo che non è conseguenza logica diretta del programma è considerato falso. Quest'ultima non può essere implementata alla lettera poiché, in generale, la deduzione logica di un atomo a partire da un programma dato è un problema non risolvibile in tempo finito.

Ad esempio, dato un knowledge base:

in teoria, è impossibile valutare a priori la dichiarazione , poiché è impossibile dire a priori se è 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 (ovvero, per verificare che non è derivabile) utilizza la risoluzione SLD esaminando soltanto i cosiddetti alberi di fallimento finito con radice . Per questo motivo, la regola è detta più propriamente negazione come fallimento finito.

Prolog[modifica | modifica wikitesto]

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 | modifica wikitesto]

  1. ^ Russel-Norvig, p. 453

Bibliografia[modifica | modifica wikitesto]

Voci correlate[modifica | modifica wikitesto]

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