Algoritmo di risoluzione
L'algoritmo di risoluzione è un algoritmo utilizzato per dimostrare un teorema e per risolvere un problema tramite l'inferenza per risoluzione. Data una conseguenza logica ( A 
B ), l'algoritmo trasforma la logica proposizionale in un insieme di clausole ( A ∧ ¬B ) è , in formato CNF ( forma normale congiuntiva ), e verifica l'eventuale insoddisfacibilità seguendo il metodo della risoluzione ( regola della risoluzione ) sulle clausole. Ogni coppia di clausole con letterali complementari viene confrontata per produrre una nuova clausola da aggiungere all'insieme ( fattorizzazione ).
- Se durante il processo emerge come risultato una clausola vuota, ciò significa che l'insieme di clausole è insoddisfacibile. La clausola vuota implica che la disgiunzione è falsa, poiché una disgiunzione è vera soltanto se almeno uno dei letterali disgiunti è vero. È quindi una contraddizione. Se l'insieme di clausole ( A ∧ ¬B ) è insoddisfacibile, allora la conseguenza logica ( A B ) è vera.
- Se il processo di fattorizzazione continua fino a concludere tutte le combinazioni di confronto tra le clausole, senza trovare una clausola vuota, allora l'insieme è soddisfacibile e la conseguenza logica ( A B ) è falsa.
L'algoritmo di risoluzione utilizza la tecnica logica della dimostrazione per assurdo. L'algoritmo di risoluzione è utilizzato nei sistemi esperti e nei software di ragionamento automatico ( intelligenza artificiale ) per attuare processi di inferenza logica su una base di conoscenza.
- Completezza dell'algoritmo. L'algoritmo di risoluzione è completo poiché, dato un insieme X di clausole, analizza tutte le coppie di clausole fino al momento in cui non è possibile produrre una nuova clausola da aggiungere all'insieme X ( insieme soddisfacibile ) o fino al momento in cui individua una clausola vuota ( insieme insoddisfacibile ).
