Il metodo di risoluzione (o calcolo per risoluzione) è un sistema di prova (calcolo logico) che è basato sostanzialmente su un’unica regola, e quindi risulta particolarmente semplice da implementare in modo automatico (infatti, esso è alla base della programmazione logica e di molti dimostratori automatici).
Inoltre, esso è molto efficiente quando lo si applica su (insiemi di) formule che hanno una forma particolare. A partire dal metodo di risoluzione per la logica del primo ordine, ristretto su specifici insiemi di formule, si definisce il modello computazionale su cui è basato il linguaggio di programmazione Prolog (1972), utilizzato soprattutto nell’ambito dell’intelligenza artificiale e della manipolazione simbolica.
Il “prezzo da pagare” per la semplicità del metodo di risoluzione è il fatto che si possano considerare solo le formule in forma normale congiuntiva. Ciò non è un limite per quanto riguarda l’espressività semantica (perchè, come dimostrato in precedenza, per ogni formula della logica proposizionale classica ne esiste una equivalente in CNF), ma risulta “scomodo” dal punto di vista della lettura delle formule: il significato di una formula trasformata in CNF tende a essere meno chiaro rispetto a quello della formula originale.
Definizione: Una clausola è una disgiunzione di letterali.
Per comodità, una clausola può essere rappresentata come un insieme di letterali:
$$ C=l_1\lor...\lor l_m\implies \cal C=\{l_1,...,l_m\} $$
Questa rappresentazione è “corretta” perchè:
Ad esempio, le seguenti formule sono logicamente equivalenti,
$$ (X\lor Y)\lor \neg Z\equiv (\neg Z\lor Y)\lor X\equiv \neg Z\lor \neg Z\lor (Y\lor X) $$
e sono tutte rappresentate dall’insieme di letterali $\cal C=\{X, Y, \neg Z\}$.
Come già visto, le formule in forma normale congiuntiva sono quelle del tipo
$$ D=\bigwedge_{i=1}^n\Big(\bigvee_{j=1}^{m_i}l_{i,j}\Big) $$
e ogni formula $H$ è equivalente a una formula $D$ in CNF.
Si osserva che ciascuna $C_i$ è una clausola. Allora, siccome anche la congiunzione è commutativa, associativa e idempotente, una CNF può essere rappresentata come un insieme contenente le clausole che compaiono nella congiunzione: