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).

Definizione

Forma normale negativa

Una formula del calcolo proposizionale ${\mathcal {L}}$ è detta in forma normale negativa sse il segno di negazione compare solo davanti agli atomi.

Clausola

Una clausola del calcolo proposizionale ${\mathcal {L}}$ è una disgiunzione di letterali $L_{1}\lor ...\lor L_{n}$.

Sussunzione di clausole

Una clausola $C_{2}$ è sussunta da una clausola $C_{1}$ sse ogni letterale in $C_{1}$ occorre in $C_{2}$.

Si noti che, se ${\mathcal {M}}$ è un modello per una clausola $C$, lo è anche per tutte le clausole da essa sussunte.

Forma clausale

Una formula del calcolo proposizionale ${\mathcal {L}}$ è detta in forma normale congiuntiva o in forma clausale, oppure si dice che essa è un insieme di clausole, sse è in forma normale negativa e inoltre ha la forma $C_{1}\land ...\land C_{n}$, dove le $C_{i}$ sono clausole.

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

$A_{1}\lor ...\lor A_{n}\lor \neg B_{1}\lor ...\lor \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 $\Box$. 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}\lor \neg B_{1}\lor ...\lor \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).