Risoluzione del primo ordine

La risoluzione del primo ordine è una tecniche di inferenza basata sull'applicazione del metodo della risoluzione ai problemi della logica del primo ordine. Il metodo della risoluzione è un processo di inferenza logica in base al quale a partire da un insieme di premesse si giunge a una o più conclusioni ( conseguenza logica ) per refutazione. La risoluzione del primo ordine è simile alla risoluzione della logica proposizionale ( metodo della risoluzione ). Le formule logiche della base di conoscenza di partenza sono rappresentate nella forma normale congiuntiva ( CNF ). Per dimostrare la veridicità di un'ipotesi, quest'ultima viene negata per verificare la soddisfacibilità dell'ipotesi contraria ( dimostrazione per refutazione ). Se l'ipotesi contraria non è vera, allora l'ipotesi originale deve necessariamente esserlo.

Nel processo di risoluzione del primo ordine l'ipotesi da dimostrare viene aggiunta, nella sua forma negata, alla base di conoscenza. Successivamente ogni clausola viene posta a confronto ( unificazione ) con un'altra clausola, ossia viene "risolta", per eliminare gli eventuali letterali complementari ( opposti ). Un letterale è detto complementare se è l'esatta negazione di un altro letterale. Ad esempio, il letterale A è la negazione del letterale ¬A, e viceversa. Gli eventuali letterali ridondanti sono eliminati ( fattorizzazione ).

L'operazione di unificazione produce una nuova clausola risolvente che sostituisce le precedenti ( sostituzione ). Il processo di risoluzione termina quando nessun'altra clausola può essere risolta con un'altra, oppure quando il processo di unificazione/sostituzione giunge a una clausola vuota.

• Clausola vuota. Quando il processo di risoluzione giunge a una clausola vuota, viene provato che l'ipotesi contraria ( ragionamento per assurdo ) non è una conseguenza logica e, pertanto, può essere affermato che l'ipotesi originale è conseguenza logica delle premesse.
• Assenza clausola vuota. Quando il processo di risoluzione giunge a un punto morto in cui nessun'altra clausola può essere risolta con un'altra, senza aver trovato una clausola vuota, è possibile affermare che l'ipotesi contraria ( ragionamento per assurdo ) è soddisfacibile logicamente e, pertanto, non si può affermare che l'ipotesi originale è una conseguenza logica delle premesse.

Nel seguente esempio è rappresentato il processo di risoluzione applicato a due formule del primo ordine. La base di conoscenza di partenza è composta dalla formula di premessa "i gatti sono mammiferi" e dalla formula di conclusione "le code dei gatti sono code di mammiferi". La risoluzione viene applicata per dimostrare se la conclusione è una conseguenza logica della premessa, o meno. Per ottenere questa risposta è necessario trasformare le formule nella forma CNF, negare la conclusione e verificare se quest'ultima ( conclusione negata ) è soddisfacibile per assurdo.

Il processo di risoluzione giunge a una clausola vuota. Seguendo il ragionamento per assurdo l'ipotesi "le code dei gatti non sono code di mammiferi" non è soddisfacibile logicamente ossia non è una conseguenza logica della premessa. È quindi possibile affermare l'esatto contrario, la formula originale "le code dei gatti sono code di mammiferi" è una conseguenza logica della premessa "i gatti sono mammiferi".

Inferenza logica. Il processo di risoluzione può essere utilizzato come processo di inferenza logica per trovare nuove informazioni a partire dalla base di conoscenza di partenza. Il processo di risoluzione può essere anche utilizzato per rispondere a specifiche domande ( query ) poste dall'utente alla base di conoscenza.

---

• Euristica della clausola unitaria. L'euristica della clausola unitaria determina l'ordine di scelta delle clausole a cui applicare la risoluzione, dando la preferenza a quelle composte da un solo letterale ( clausole unitarie ). Le clausole unitarie hanno maggiore probabilità di produrre una clausola vuota e, quindi, possono ridurre notevolmente il processo di inferenza logica. Ad esempio, data la seguente formula composta da quattro clausole A ∧ ( ¬A ∨ C ) ∧ ¬A ∧ ¬C, è evidente che unificando le due clausole unitarie complementari A e ¬A si genera immediatamente una clausola vuota, senza alcun ulteriore confronto.
• Funzione euristica di selezione delle clausole. Con lo stesso criterio possono essere selezionate tutte le clausole che, sulla base di una funzione euristica legata alla dimensione dei letterali o alla difficoltà di computo, forniscono maggiore probabilità di giungere a una clausola vuota ( insoddisfacibilità ). Ad esempio, un'euristica vincola la selezione delle clausole alla presenza all'interno di uno o più letterali strategici. Generalmente si utilizzano i letterali della query negata, in quanto sono quelli che consentono di giungere in modo diretto a una clausola vuota.
• Funzione euristica della risoluzione unitaria. L'euristica della risoluzione unitaria consiste nel confrontare tra loro soltanto le clausole unitarie di una formula logica. L'euristica è efficace, in particolar modo nelle clausole di Horn, in quanto consente di aumentare le performance del processo di risoluzione. Tuttavia, in generale l'euristica non garantisce la completezza di analisi ( non completezza ). d esempio, nella seguente formula A ∧ ( ¬A ∨ C ) ∧ ¬C sono confrontate soltanto le clausole unitarie A e ¬C senza generare nessuna clausola vuota. Per giungere alla clausola vuota è, invece, necessario unificare una delle due clausole unitarie ( es. A ) con la clausola centrale ( ¬A ∨ C ) e, subito dopo, la clausola risultante ( C ) con l'altra clausola unitaria ( ¬C ).