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 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). 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 , tipica della logica classica.M. Bílková, A. Colacito. Proof Theory for Positive Logic with Weak Negation. Studia Logica, Springer, 108, pages 649–686 (2020).
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:
in teoria, è impossibile valutare a priori la formula logica , poiché è impossibile derivare 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 (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 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
Bibliografia
Voci correlate Regola di inferenza Assunzione del mondo chiuso
Categoria:Programmazione logica Categoria:Rappresentazione della conoscenza Categoria:Ragionamento automatico