Logica matematica/Calcolo delle proposizioni/La risoluzione

Forma normale a clausole

Introduciamo la forma normale a clausole e un algoritmo per convertire le formule del calcolo proposizionale in formule equivalenti, espresse in forma normale a clausole. Questa ci servirà per introdurre il metodo di risoluzione. Ricordiamo che, nel calcolo proposizionale, i letterali sono simboli proposizionali (atomi) o simboli proposizionali negati (atomi negati).

Poiché la disgiunzione è commutativa, una clausola generica può essere scritta come segue:

$A_1\vee ...\vee A_n\vee \mathrm{\neg }{B}_1\vee ...\vee \mathrm{\neg }{B}_m$

dove gli $A_i$ e $B_j$ sono atomi. Se $n=m=0$, si ha la clausola vuota e si scrive $\{\}$, oppure $◻$. Nel seguito, una clausola verrà indicata anche come l'insieme dei suoi letterali, cioè mediante $\{L_1,...,L_p\}$.

Se $n=1$, cioè se una clausola ha la forma:

$A_1\vee \mathrm{\neg }{B}_1\vee ...\vee \mathrm{\neg }{B}_m$

si dice che è una clausola definita.

Trasformazione in clausole

Ora, introduciamo un algoritmo per convertire le formule del calcolo proposizionale, in modo che assumano una forma a clausole (cioè congiunzione di disgiunzioni di letterali).