Logica matematica/Calcolo delle proposizioni/La risoluzione

Indice del libro


Forma normale a clausole

modifica

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

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