Esempio di risoluzione nella logica del primo ordine
Il seguente esempio mostra tutti i passi necessari per svolgere un processo di inferenza in un problema tramite l'applicazione del metodo della risoluzione nella logica del primo ordine. L'esempio è tratto dal libro Artificial Intelligence di Russel-Norvig di cui consiglio la lettura. La base di conoscenza iniziale è composta da una serie di espressioni in linguaggio naturale.
Chiunque ami gli animali è amato da qualcuno
Chi uccide un animale non è amato da nessuno
John ama tutti gli animali
I gatti sono animali
Un gatto si chiama Tom
Tom è stato ucciso da John o dalla curiosità
A questo punto ci chiediamo... chi ha ucciso il gatto? È stato John o la curiosità? In una frazione di secondo un essere umano ottiene la risposta. È un problema banale. Per giungere alla stessa conclusione un computer deve seguire un processo inferenziale e utilizzare un metodo di ragionamento. Per risolvere questo problema si utilizzerà il metodo della risoluzione ovvero la dimostrazione per assurdo.
Conversione nella logica del primo ordine
Come prima cosa è necessario convertire le espressioni del linguaggio naturale in formule della logica del primo ordine. Per farlo utilizziamo dei predicati in sostituzione dei verbi, dei quantificatori e delle variabili.
Questa forma è però difficilmente elaborabile da un computer. È necessario trasformarla nella forma congiuntiva CNF che consente all'algoritmo informatica di computare ogni espressione più facilmente. La forma CNF è equivalente a quella della logica del primo ordine, quindi se è vera la prima è vera anche la seconda, e viceversa.
La base di conoscenza rappresentata nella forma normale congiuntiva è la seguente:
Ipotesi da dimostrare
A questo punto interroghiamo la base di conoscenza con la seguente domanda: "è stata la curiosità a uccidere Tom?". Anche in questo caso è necessario trasformare la domanda nella logica del primo ordine nella forma normale congiuntiva CNF.
Uccide(Curiosità, Tom)
Per rispondere a questa domanda utilizziamo il metodo della risoluzione seguendo un ragionamento per assurdo.
Metodo della risoluzione
Il metodo della risoluzione consente di dimostrare un'ipotesi per refutazione. Per rispondere alla domanda "è stata la curiosità a uccidere Tom?" si parte dall'ipotesi opposta che non sia stata la curiosità a ucciderlo e si verifica se questa è una conseguenza logica delle premesse o meno. Nella forma CNF della logica del primo ordine l'ipotesi assurda può essere scritta nel seguente modo:
¬Uccide(Curiosità, Tom)
La clausola viene poi aggiunta alla base di conoscenza. Nella rappresentazione seguente l'ipotesi assurda è l'ultima clausola di colore rosso.
A questo punto il metodo della risoluzione unisce le varie clausole per eliminare i letterali complementari e quelli ridondanti. Dal confronto viene prodotta una nuova clausola risolvente che si aggiunge alla base di conoscenza.
Non essendo dimostrabile l'ipotesi contraria ( "la curiosità non ha ucciso Tom" ) si può, quindi, dedurre che l'ipotesi originale ( "la curiosità ha ucciso Tom" ) è vera in quanto è una conseguenza logica delle premesse di partenza. E così anche il computer ha capito che la curiosità ha ucciso il gatto...
