Logica matematica/Calcolo delle proposizioni/La risoluzione
Forma normale a clausole
modificaIntroduciamo 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).
Forma normale negativa
Una formula del calcolo proposizionale è detta in forma normale negativa sse il segno di negazione compare solo davanti agli atomi.
Clausola
Una clausola del calcolo proposizionale è una disgiunzione di letterali .
Sussunzione di clausole
Una clausola è sussunta da una clausola sse ogni letterale in occorre in .
Si noti che, se è un modello per una clausola , lo è anche per tutte le clausole da essa sussunte.
Forma clausale
Una formula del calcolo proposizionale è 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 , dove le sono clausole.
Poiché la disgiunzione è commutativa, una clausola generica può essere scritta come segue:
dove gli e sono atomi. Se , si ha la clausola vuota e si scrive , oppure . Nel seguito, una clausola verrà indicata anche come l'insieme dei suoi letterali, cioè mediante .
Se , cioè se una clausola ha la forma:
si dice che è una clausola definita.
Trasformazione in clausole
modificaOra, introduciamo un algoritmo per convertire le formule del calcolo proposizionale, in modo che assumano una forma a clausole (cioè congiunzione di disgiunzioni di letterali).