Vai al contenuto

Logica matematica/Calcolo delle proposizioni/La risoluzione

Wikibooks, manuali e libri di testo liberi.
Indice del libro


Forma normale a clausole

[modifica | modifica sorgente]

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 è 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

[modifica | modifica sorgente]

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