# Logica matematica/Calcolo delle proposizioni/La risoluzione

Logica matematica
Copertina Tutti i moduli · Sviluppo
* InsiemiLogica matematica/Insiemi
* Sistemi formaliLogica matematica/Sistemi formali
* Calcolo delle proposizioniLogica matematica/Calcolo delle proposizioni
** Il sistema di Frege-HilbertLogica matematica/Calcolo delle proposizioni/Sistema di Hilbert
** La deduzione naturaleLogica matematica/Calcolo delle proposizioni/La deduzione naturale
** Il calcolo dei sequenti
** I tableaux semanticiLogica matematica/Calcolo delle proposizioni/I tableaux semantici
** La risoluzioneLogica matematica/Calcolo delle proposizioni/La risoluzione
** Esercizi su tavole di veritàLogica matematica/Calcolo delle proposizioni/Esercizi su tavole di verità
* Calcolo dei predicatiLogica matematica/Calcolo dei predicati
* Teoria dei modelliLogica matematica/Teoria dei modelli
* Computabilità
* IncompletezzaLogica matematica/Incompletezza
** Teoremi di incompletezza di GödelLogica matematica/Incompletezza/Teoremi di incompletezza di Gödel
* Intermezzo: EuclideLogica matematica/Intermezzo Euclide
* Intermezzo: i paradossiLogica matematica/Intermezzo paradossi
* Risorse internetLogica matematica/Risorse internet
Modifica il sommario

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