LOGICA MATEMATICA - docenti.unicam.itdocenti.unicam.it/tmp/4976.pdf · Sonia L’Innocente...

83
Sonia L’Innocente LOGICA MATEMATICA Sonia L’Innocente Corso di Laurea Informatica e Tecnologie/Informatica Industriale Argomento 1. Logica proposizionale a.a. 2014-2015 Sonia L’Innocente (Camerino) 1 / 83

Transcript of LOGICA MATEMATICA - docenti.unicam.itdocenti.unicam.it/tmp/4976.pdf · Sonia L’Innocente...

Sonia L’Innocente

LOGICA MATEMATICA

Sonia L’Innocente

Corso di Laurea

Informatica e Tecnologie/Informatica Industriale

Argomento 1.

Logica proposizionale

a.a. 2014-2015

Sonia L’Innocente (Camerino) 1 / 83

Sonia L’Innocente

Introduzione

Outline

1 Introduzione

2 Semantica e valutazioni

3 Cenni di sintassi

4 Connettivi, forme normali

5 Il problema della soddisfacibilità

6 Forme normali e clausole

7 Il Teorema di decomposizione

8 Il Teorema di risoluzione

Sonia L’Innocente (Camerino) 2 / 83

Sonia L’Innocente

Introduzione

Tentativo di definizioneLogica (matematica) = studio del pensiero (matematico)

I grandi della logica:Una lista sommaria di nomi e motivazioni

Aristotele (il sillogismo)Leibniz (calculus ratiocinator)Boole (l’algebra del pensiero, i fondamenti algebrici della logica)Frege (i fondamenti logici della matematica)Hilbert (il metodo assiomatico e il Programma)Godel (i teoremi di incompletezza, i limiti della conoscenzamatematica)Tarski (che cos’è la verità)Turing (l’avvento dell’informatica, l’intelligenza artificiale)

Sonia L’Innocente (Camerino) 3 / 83

Sonia L’Innocente

Introduzione

Cerchiamo di capire la struttura di affermazioni arbitrarie e di afferrarele regole che ne assicurano o ne escludono la verità. Una premessa èdoverosa, per mettere in guardia dalle differenze sottili che taloraseparano• il rigore della logica matematica,

• le convenzioni della lingua comune.

Il primo aiuta a studiare le seconde, ma spesso segue strade proprie.

Sonia L’Innocente (Camerino) 4 / 83

Sonia L’Innocente

Introduzione

Qualche esempio delle ambiguità che distinguono il linguaggiocomune e quello rigoroso della matematica.

• In geometria piana le due affermazioni “q, q’ sono quadrati e “q è unquadrato e q’ è un quadrato paiono perfettamente equivalenti: l’una el’altra sono vere se e solo se, appunto, sia q che q’ sono quadrati.

• Le due affermazioni “Carlo e Camilla sono sposati, “Carlo è sposatoe Camilla è sposata si prestano a interpretazioni diverse, perch nellinguaggio comune la prima equivale a dire che Carlo e Camilla sonosposati tra loro, la seconda a sostenere che ciascuno dei due sposato,ma eventualmente per conto proprio.

Sonia L’Innocente (Camerino) 5 / 83

Sonia L’Innocente

Introduzione

Consideriamo la seguente definizione:

un numero naturale n si dice primo se e solo se n > 1 e, se a è unnaturale ed a divide n, allora a = 1 o a = n.

Analizzando la struttura di questa definizione, si riconosconoproposizioni fondamentali

n > 1, a è un naturale, a divide n, a = 1, a = n

separate da connettivi

. . . e . . . , se . . . allora . . ., . . . o . . .

Se si indicano con p0, p1, p2, p3, p4 le proposizioni fondamentali sopraelencate, e con ∧,→, ∨ i connettivi, la precedente definizione apparecosì strutturata:

p0 ∧ ((p1 ∧ p2)→ (p3 ∨ p4)).

Sonia L’Innocente (Camerino) 6 / 83

Sonia L’Innocente

Introduzione

La Logica ProposizionaleLa logica proposizionale si propone un’analisi generale della ossaturadelle proposizioni matematiche sulle basi sopra accennate.Introduciamo questa logica. Cominciamo col definirne le formule.

Definizione.Alfabeto della logica proposizionale è l’insieme dei seguenti elementi:

variabili proposizionali p0, p1, . . ., pn, . . . per n naturale;

connettivi ¬ (non), ∧ (e), ∨ (o),→ (se ... allora),↔ (se e solo se);

parentesi ( , ) .

Sonia L’Innocente (Camerino) 7 / 83

Sonia L’Innocente

Introduzione

Gli elementi dell’alfabeto si dicono simboli della logica proposizionale.Si definisce invece parola una sequenza finita di simboli dell’alfabeto.Ad esempio, p0( )¬∧ è una parola (in verità un po’ disordinata).

Definizione.L’insieme F delle formule della logica proposizionale è il minimoinsieme di parole dell’alfabeto

• contenente ogni variabile proposizionale pn (per n naturale);

• tale che, se α e β sono in F , allora anche ¬α, α ∧ β, α ∨ β, α→ β,α↔ β sono in F .

Sonia L’Innocente (Camerino) 8 / 83

Sonia L’Innocente

Introduzione

Esempio.

p0 ∧ ((p1 ∧ p2)→ (p3 ∨ p4))

è una formula. Le parentesi (, ) sono usate nel modo ovvio per evitarepericoli di confusione ed ordinare le formule più elaborate. Così anche

(p0 ∧ p1) ∧ (p2 → (p3 ∨ p4))

è una formula, ma è diversa dalla precedente, come le parentesiappunto testimoniano. In realtà potremmo definire rigorosamente ilruolo delle parentesi, ma preferiamo qui affidarci al puro buon senso.

Sonia L’Innocente (Camerino) 9 / 83

Sonia L’Innocente

Introduzione

È comunque intuitivamente accettabile che, se α, β e γ ∈ F , le formule

α ∧ (β ∧ γ), (α ∧ β) ∧ γ,

come ancheα ∨ (β ∨ γ), (α ∨ β) ∨ γ,

si possano identificare. Scriveremo allora liberamente α∧ β ∧ γ oppureα ∨ β ∨ γ. Se poi α0, . . . , αn ∈ F , le abbreviazioni∧

i≤n

αi ,∨i≤n

αi

hanno l’ovvio significato

α0 ∧ . . . ∧ αn, α0 ∨ . . . ∨ αn.

Sonia L’Innocente (Camerino) 10 / 83

Sonia L’Innocente

Semantica e valutazioni

Outline

1 Introduzione

2 Semantica e valutazioni

3 Cenni di sintassi

4 Connettivi, forme normali

5 Il problema della soddisfacibilità

6 Forme normali e clausole

7 Il Teorema di decomposizione

8 Il Teorema di risoluzione

Sonia L’Innocente (Camerino) 11 / 83

Sonia L’Innocente

Semantica e valutazioni

Le valutazioni della logica proposizionale.Definizione. Valutazione è una applicazione v dell’insieme{pn : n ∈ N} di tutte le variabili proposizionali in {0, 1}.

Una valutazione v è, allora, parlando alla buona, un modo di intendereogni variabile proposizionale pn come vera o falsa, nel senso che

• v(pn) = 1 significa che pn è vera per v ,

• v(pn) = 0 significa che pn è falsa per v .

Sonia L’Innocente (Camerino) 12 / 83

Sonia L’Innocente

Semantica e valutazioni

Ogni valutazione v si può estendere ad una applicazione vdell’insieme F di tutte le formule in {0, 1} nel modo seguente (cheesprime rigorosamente ragionevoli intuizioni del senso comune):anzitutto, per ogni n naturale,

v(pn) = v(pn);

se poi α e β sono formule,

v(¬α) è 1 se v(α) = 0 e 0 altrimenti;

v(α ∧ β) è 1 se v(α) = v(β) = 1 e 0 altrimenti;

v(α ∨ β) è 1 se v(α) oppure v(β) è 1, e 0 altrimenti;

v(α→ β) è 1 se v(α) = 0 o v(β) = 1, 0 altrimenti;

v(α↔ β) è 1 se v(α) = v(β), 0 altrimenti;

Sonia L’Innocente (Camerino) 13 / 83

Sonia L’Innocente

Semantica e valutazioni

La definizione di v(α→ β) può forse creare qualche perplessità,perché è difficile accettare che, quando si pensa che α sia falsa, alloraα→ β sia supposta vera indipendentemente da β. Suggeriamo però leseguenti implicazioni, che sono vere, ed hanno premesse false econclusioni l’una falsa e l’altra vera:

se 2 + 2 = 5, allora 3 + 2 = 6,

se 2 + 2 = 5, allora 2 + 2 > 3.Nel seguito indicheremo v ancora con v per semplificare la notazione.

Sonia L’Innocente (Camerino) 14 / 83

Sonia L’Innocente

Semantica e valutazioni

Definizione.

Siano α ∈ F , v una valutazione. Si dice che v soddisfa α (v |= α) sev(α) = 1.In particolare, se α e β appartengono a F , allora si ha:v |= ¬α se e solo se v 6|= α,v |= α ∧ β se e solo se v |= α e v |= β,v |= α ∨ β se e solo se v |= α o v |= β,

Sonia L’Innocente (Camerino) 15 / 83

Sonia L’Innocente

Semantica e valutazioni

v |= α→ β se e solo se v 6|= α o v |= β,v |= α↔ β se e solo se v |= α esattamente quando v |= β.Se S è un insieme di formule e v è una valutazione, diciamo che vsoddisfa S (v |= S) se v |= σ per ogni σ ∈ S.

Sonia L’Innocente (Camerino) 16 / 83

Sonia L’Innocente

Semantica e valutazioni

Teorema di coincidenzaSiano α una formula di F , n un naturale tale che le variabiliproposizionali occorrenti in α sono tra p0, . . . , pn. Siano poi v0 e v1due valutazioni tali che v0(pi) = v1(pi) per ogni i ≤ n. Allora v0 |= α see solo se v1 |= α.

Sonia L’Innocente (Camerino) 17 / 83

Sonia L’Innocente

Semantica e valutazioni

Dimostrazione.

Si procede per induzione sulla costruzione della formula α.Se α è una variabile proposizionale, deve essere α = pi per qualchei ≤ n; ma allora v0 |= pi se e solo se v1 |= pi per ipotesi.Se α è ¬β per qualche β ∈ F soddisfacente la tesi, allora v0 |= α se esolo se v0 6|= β e dunque se e solo se v1 6|= β, cioè se e solo se v1 |= α.

Se α è β ∧ γ dove β, γ ∈ F soddisfano la tesi, allora v0 |= α se e solose v0 |= β e v0 |= γ, dunque se e solo se v1 |= β e v1 |= γ, cioè se esolo se v1 |= α.Gli altri casi α = β ∨ γ, α = β → γ, α = β ↔ γ si trattano in modoanalogo. a

Sonia L’Innocente (Camerino) 18 / 83

Sonia L’Innocente

Semantica e valutazioni

Definizione.

Una formula α si dice soddisfacibile se e solo se esiste unavalutazione v tale che v |= α.Enunciamo anche il problema principale che intendiamo studiarenell’ambito della logica proposizionale.Problema della soddisfacibilità (per la logica proposizionale).Determinare un algoritmo per decidere, per ogni formula α, se α èsoddisfacibile o no.

Sonia L’Innocente (Camerino) 19 / 83

Sonia L’Innocente

Semantica e valutazioni

Definizione.

Una formula α si dice valida (o tautologia) se e solo se, per ognivalutazione v , v |= α.Allora una formula α è valida se e solo se ¬α non è soddisfacibile.Definizione. Un insieme S di formule si dice soddisfacibile se e solose esiste una valutazione v tale che v |= S (cioè, per ogni formula σ diS, v |= σ).Si vede facilmente che, se S è un insieme finito di formule, allora S èsoddisfacibile se e solo se

∧σ∈S σ è soddisfacibile. In particolare

l’insieme vuoto è soddisfacibile, anzi è soddisfatto da ogni valutazione.

Sonia L’Innocente (Camerino) 20 / 83

Sonia L’Innocente

Semantica e valutazioni

Equivalenza logicaDefinizione. Due formule α e β si dicono logicamente equivalenti se esolo se, per ogni valutazione v , v |= α esattamente quando v |= β.In altre parole, α e β sono logicamente equivalenti se e solo se α↔ βè una tautologia. Osserviamo poi che la relazione di equivalenzalogica è (a conferma del nome) una relazione di equivalenzanell’insieme di tutte le formule.

Sonia L’Innocente (Camerino) 21 / 83

Sonia L’Innocente

Semantica e valutazioni

Conseguenza logicaDefinizione. Siano S un insieme di formule, α una formula. Si diceche α è conseguenza di S (S |= α) se e solo se, per ogni valutazionev , quando v |= S, allora v |= α.Per S e α come sopra, S |= α se e solo se S ∪ {¬α} non èsoddisfacibile.Se S è finito, S |= α se e solo se la formula

∧σ∈S σ ∧ ¬α non è

soddisfacibile.Notiamo poi che una formula α è valida se e solo se ∅ |= α.

Sonia L’Innocente (Camerino) 22 / 83

Sonia L’Innocente

Semantica e valutazioni

Segue dalle precedenti osservazioni che, se si dispone di un algoritmoper il problema della soddisfacibilità, si possono agevolmente costruirealgoritmi per decidere:

1. per ogni formula α, se α è valida o no;

2. per ogni insieme finito S di formule, se S è soddisfacibile o no;

3. per ogni coppia di formule α e β, se α e β sono logicamenteequivalenti o no;

4. per ogni insieme finito di formule S e per ogni formula α, se α è o noconseguenza di S.

Sonia L’Innocente (Camerino) 23 / 83

Sonia L’Innocente

Semantica e valutazioni

Osservazioni(i) Siano α, β e γ formule. Sono logicamente equivalenti

α e ¬¬α,

¬(α ∧ β) e ¬α ∨ ¬β,

¬(α ∨ β) e ¬α ∧ ¬β,

α↔ β e (α→ β) ∧ (β → α),

α→ β e ¬α ∨ β,

α ∧ (β ∨ γ) e (α ∧ β) ∨ (α ∧ γ),

α ∨ (β ∧ γ) e (α ∨ β) ∧ (α ∨ γ).

Sonia L’Innocente (Camerino) 24 / 83

Sonia L’Innocente

Semantica e valutazioni

Osservazioni(ii) Siano α, β, α′, β′ formule tali che α è logicamente equivalente adα′, e β è logicamente equivalente a β′. Allora anche le seguentiformule sono logicamente equivalenti:

¬α e ¬α′,

α ∧ β e α′ ∧ β′,

α ∨ β e α′ ∨ β′,

α→ β e α′ → β′,

α↔ β e α′ ↔ β′.

Sonia L’Innocente (Camerino) 25 / 83

Sonia L’Innocente

Semantica e valutazioni

Abbiamo prima definito i concetti di insieme soddisfacibile S diformule, e per conseguenza di un insieme S di formule.Abbiamo anche osservato che, se si dispone di un algoritmo per ilproblema della soddisfacibilità per le formule, è agevole dedurne altri,uno per controllare la soddisfacibilità di un insieme S di formule, eduno per controllare le conseguenze di S, purché S sia finito.L’ipotesi di finitezza di S è, del resto, assolutamente ovvia nel contestodi ricerca di algoritmi da applicare nella pratica.Vogliamo però dimostrare che, in un certo senso, il caso in cui S èinfinito si può ridurre al caso finito.Vale il seguente teorema.

Sonia L’Innocente (Camerino) 26 / 83

Sonia L’Innocente

Semantica e valutazioni

Teorema di CompattezzaSia S un insieme infinito di formule. Allora S è soddisfacibile se e solose ogni sottoinsieme finito di S è soddisfacibile.

In particolare si ha:

Corollario.Se S è un insieme infinito di formule e α è una formula, allora α èconseguenza di S se e solo se esiste un sottoinsieme finito S0 di Stale che α è conseguenza di S0.

Sonia L’Innocente (Camerino) 27 / 83

Sonia L’Innocente

Semantica e valutazioni

Dimostrazione del corollario.Sappiamo che S |= α se e solo se S ∪ {¬α} non è soddisfacibile. Sevale il Teorema di compattezza, questo equivale ad affermare cheesiste un sottoinsieme finito S1 di S ∪ {¬α} che non è soddisfacibile, enon c’è perdita di generalità nel supporre ¬α ∈ S1, cioèS1 = S0 ∪ {¬α} per qualche sottoinsieme finito S0 di S (infatti, se siaggiungono nuove formule, come ¬α, ad un insieme giàinsoddisfacibile, si ottiene un insieme ancora insoddisfacibile).Possiamo allora dire che S |= α se e solo se esiste un sottoinsiemefinito S0 di S tale che S0 ∪ {¬α} non è soddisfacibile, cioè tale cheS0 |= α. a

Sonia L’Innocente (Camerino) 28 / 83

Sonia L’Innocente

Cenni di sintassi

Outline

1 Introduzione

2 Semantica e valutazioni

3 Cenni di sintassi

4 Connettivi, forme normali

5 Il problema della soddisfacibilità

6 Forme normali e clausole

7 Il Teorema di decomposizione

8 Il Teorema di risoluzione

Sonia L’Innocente (Camerino) 29 / 83

Sonia L’Innocente

Cenni di sintassi

Teorema di completezza

Definizione: α dimostrabileDato

• un insieme di assiomi (ovvero di formule di F di evidentesensatezza);

• un insieme di regole di deduzione (ovvero di funzioni che a certesequenze ordinate di formule associano nuove formule, ad esempio(α, α→ β) 7−→ β)

si dice che, per ogni formula α e per ogni insieme S di formule, α èdimostrabile da S ,

S ` α

se e solo se esiste una sequenza finita α0, . . . , αn di formule tali cheαn = α e, per ogni i < n, αi è un assioma o appartiene a S o si ottieneda formule precedenti tramite le regole di deduzione.

Sonia L’Innocente (Camerino) 30 / 83

Sonia L’Innocente

Cenni di sintassi

Teorema di completezza

È possibile definire in modo opportuno

• un insieme di assiomi;

• un insieme di regole di deduzione;

in modo tale che, ∀α e ∀ insieme S di formule,

S |= α se e solo se S ` α

Sonia L’Innocente (Camerino) 31 / 83

Sonia L’Innocente

Cenni di sintassi

Questo risultato prende il nome di Teorema di completezza. Il suosignificato è chiaro. Sappiamo infatti che, se α è una formula e S è uninsieme di formule, α è conseguenza di S se e solo se ognivalutazione che crede a S crede anche ad α. Il Teorema dicompletezza ci dice che, per una opportuna scelta di assiomi e regoledi deduzione, questo equivale, per ogni S e α, alla possibilità didimostrare (nel senso sopra descritto) α da S.

Sonia L’Innocente (Camerino) 32 / 83

Sonia L’Innocente

Connettivi, forme normali

Outline

1 Introduzione

2 Semantica e valutazioni

3 Cenni di sintassi

4 Connettivi, forme normali

5 Il problema della soddisfacibilità

6 Forme normali e clausole

7 Il Teorema di decomposizione

8 Il Teorema di risoluzione

Sonia L’Innocente (Camerino) 33 / 83

Sonia L’Innocente

Connettivi, forme normali

Intendiamo affrontare in questo paragrafo il problema di dare unadefinizione rigorosa di connettivo.

Intuitivamente, connettivo (ad esempio ∧) è una costruzione che, apartire da certe formule (α, β nel nostro caso), definisce una nuovaformula (α ∧ β, appunto).

Della nuova formula non è tanto importante la rappresentazione chese ne dà, quanto il significato che le si attribuisce, e dunque quando lasi ritiene vera, in relazione naturalmente ai valori di verità assegnatialle formule che la definiscono.

Vediamo il successivo esempio.

Sonia L’Innocente (Camerino) 34 / 83

Sonia L’Innocente

Connettivi, forme normali

Esempio∀v , si ha che: v(α ∧ β) = 1 se e solo se v(α) = v(β) = 1. In questosenso ∧ si identifica con la funzione

f : {0, 1}2 → {0, 1}

tale chef ((1, 1)) = 1,

f ((0, 0)) = f ((0, 1)) = f ((1, 0)) = 0

o, equivalentemente, tale che, per ogni x0, x1 ∈ {0, 1},f ((x0, x1)) = v(α ∧ β) dove α e β sono formule e v è una valutazionetale che v(α) = x0 e v(β) = x1.

Sonia L’Innocente (Camerino) 35 / 83

Sonia L’Innocente

Connettivi, forme normali

Queste considerazioni suggeriscono la seguente definizione.

ConnettivoDefinizione. Sia n un intero positivo. Connettivo n-ario è una funzionedi {0, 1}n in {0, 1}.

Sia α con variabili proposizionali tra p0, . . . , pn−1.

Allora α definisce il seguente connettivo n-ario f nα : per ogni scelta di

x0, . . . , xn−1 ∈ {0, 1},

f nα(x0, . . . , xn−1) = v(α)

dove v è una valutazione tale che v(pi) = xi ∀i < n

Sonia L’Innocente (Camerino) 36 / 83

Sonia L’Innocente

Connettivi, forme normali

Osservazioni.Siano α e β due formule con variabili proposizionali tra p0, . . . , pn−1.

1. f nα è la funzione non nulla se e solo se α è soddisfacibile.

Spiegazione

Sia infatti α soddisfacibile, e sia v tale che v(α) = 1. Allora

f nα(v(p0), . . . , v(pn−1)) = 1,

e f nα non è la funzione nulla.

Viceversa, assumiamo che esista x = (x0, . . . , xn−1) ∈ {0, 1}n taleche f n

α(x) = 1. Se v è una valutazione tale che v(pj) = xj per ognij < n, si ha v(α) = f n

α(x) = 1. Così v |= α.

Sonia L’Innocente (Camerino) 37 / 83

Sonia L’Innocente

Connettivi, forme normali

Osservazioni.2. f n

α = f nβ se e solo se α e β sono logicamente equivalenti.

Spiegazione

Supponiamo infatti α e β logicamente equivalenti. Allora, ∀v ,v(α) = v(β). Sia x ∈ {0, 1}n; ricordiamo che

f nα(x) = v(α), f n

β (x) = v(β)

dove v è tale che v(pj) = xj per ogni j < n; dunque f nα(x) = f n

β (x).Segue f n

α = f nβ .

Supponiamo adesso f nα = f n

β . Per ogni v , si ha

v(α) = f nα(v(p0), . . . , v(pn−1)), v(β) = f n

β (v(p0), . . . , v(pn−1)).

Allora v(α) = v(β). Dunque α e β sono logicamente equivalenti.

Sonia L’Innocente (Camerino) 38 / 83

Sonia L’Innocente

Connettivi, forme normali

Siamo ora in grado di dimostrare il seguente teorema.

Teorema.Siano n ∈ N− {0} e g un connettivo n-ario.

Allora esiste una formula α con variabili proposizionali tra p0, . . . , pn−1tale che f n

α = g. Inoltre α può essere scelta come una disgiunzione dicongiunzioni di variabili proposizionali o negazioni di variabiliproposizionali.

OsservazioneIl teorma mostra che ∀n ∈ N− {0}e per ogni connettivo n-ario g, ∃ unaformula α costruita con il solo uso di ¬, ∧ e ∨ (addiritturaα =

∨i≤k

∧j<n λi,j dove ciascun λi,j è pj o la sua negazione) tale che

g = f nα . In particolare i connettivi proposti ¬, ∧, ∨,→,↔ sono (più che)

sufficienti; anzi ¬, ∧ e ∨ bastano per generare tutti i possibili connettivi.

Sonia L’Innocente (Camerino) 39 / 83

Sonia L’Innocente

Connettivi, forme normali

Definizione.

Una formula α si dice

1. basica se e solo se α è una variabile proposizionale o la suanegazione;

2. in forma normale disgiuntiva se α è una disgiunzione dicongiunzioni di formule basiche:

α =∨

i≤k∧

j≤niλi,j

dove k e ciascun ni (i ≤ k ) sono interi positivi, mentre ciascun λi,j èuna formula basica (si scrive allora α ∈ DNF );

Sonia L’Innocente (Camerino) 40 / 83

Sonia L’Innocente

Connettivi, forme normali

3. in forma normale congiuntiva se α è una congiunzione didisgiunzioni di formule basiche:

α =∧i≤k

∨j≤ni

λi,j

dove k e ciascun ni (i ≤ k ) sono interi positivi, mentre ciascun λi,j èuna formula basica (si scrive allora α ∈ CNF ).

Un’altra conseguenza del precedente teorema è data dal seguentecorollario.

Corollario.Sia β una formula. Allora esistono una formula α ∈ DNF e una formulaγ ∈ CNF logicamente equivalenti a β.

Sonia L’Innocente (Camerino) 41 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

Outline

1 Introduzione

2 Semantica e valutazioni

3 Cenni di sintassi

4 Connettivi, forme normali

5 Il problema della soddisfacibilità

6 Forme normali e clausole

7 Il Teorema di decomposizione

8 Il Teorema di risoluzione

Sonia L’Innocente (Camerino) 42 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

È già stato introdotto il problema della soddisfacibilità nella logicaproposizionale, un metodo semplice è il seguente

Le Tavole di veritàData una formula α,

1. si enumerano le variabili proposizionali p0, . . . , pn−1 in α;

2. si enumerano tutte le possibili sequenze x0, . . . , xn−1 che unavalutazione v può associare a p0, . . . , pn−1,

3. per ogni sequenza, si calcola il corrispondente valore di v(α).

α è soddisfacibile se e solo se almeno una volta si ottiene v(α) = 1.

Sonia L’Innocente (Camerino) 43 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

Esempi

1. α è ¬p0 ∨ (p0 → p1). Allora α è soddisfacibile.

p0 p1 ¬p0 p0 → p1 α

1 1 0 1 11 0 0 0 00 1 1 1 10 0 1 1 1

In particolare, le valutazioni v per cui v(α) = 1 sono quelle tali chev(p0) = 0 o v(p1) = 1.

Sonia L’Innocente (Camerino) 44 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

2.

Sia α la formula (p0 → p1) ∧ (p1 → p0). Allora α è soddisfacibile.

p0 p1 p0 → p1 p1 → p0 α

1 1 1 1 11 0 0 1 00 1 1 0 00 0 1 1 1

La formula α è soddisfacibile perché esistono valutazioni che leassociano il valore 1. Tali valutazioni sono quelle v per cuiv(p0) = v(p1). In particolare α è logicamente equivalente a p0 ↔ p1.

Sonia L’Innocente (Camerino) 45 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

3.

Sia ora α la formula p0 ∨ (p1 ∧ ¬p2). Allora α è soddisfacibile, comemostra la seguente tabella.

p0 p1 p2 ¬p2 p1 ∧ ¬p2 α

1 1 1 0 0 11 1 0 1 1 11 0 1 0 0 11 0 0 1 0 10 1 1 0 0 00 1 0 1 1 10 0 1 0 0 00 0 0 1 0 0

La formula α è soddisfacibile perché esistono valutazioni che leassociano il valore 1.

Sonia L’Innocente (Camerino) 46 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

4.

Il metodo esposto si può applicare, più in generale, per stabilire lasoddisfacibilità di una formula quale ¬α ∨ (α→ β) con α e β in F , inriferimento, naturalmente, alle valutazioni di α e β. In questo caso si ha

α β ¬α α→ β ¬α ∨ (α→ β)

1 1 0 1 11 0 0 0 00 1 1 1 10 0 1 1 1

Perciò, per ogni valutazione v , si ha che v soddisfa ¬α ∨ (α→ β) se esolo se v non soddisfa α oppure v soddisfa β. L’esistenza di una talevalutazione, e quindi la soddisfacibilità di ¬α ∨ (α→ β), dipendeovviamente da α e β.

Sonia L’Innocente (Camerino) 47 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

5.

Per ogni formula α, α ∨ ¬α è valida.

α ¬α α ∨ ¬α

1 0 10 1 1

Dunque, per ogni valutazione v , v soddisfa α ∨ ¬α.

6. Per ogni formula α, α ∧ ¬α non è soddisfacibile.

α ¬α α ∧ ¬α

1 0 00 1 0

Dunque, per ogni valutazione v , v non soddisfa α ∧ ¬α.

Sonia L’Innocente (Camerino) 48 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

7.

Se α e β sono formule, allora α→ β e ¬α ∨ β sono logicamenteequivalenti.

α β α→ β ¬α ¬α ∨ β

1 1 1 0 11 0 0 0 00 1 1 1 10 0 1 1 1

Allora, per ogni valutazione v , v soddisfa α→ β se e solo se vsoddisfa ¬α ∨ β. Di conseguenza le due formule sono logicamenteequivalenti.

Sonia L’Innocente (Camerino) 49 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

8.

Se α e β sono formule, allora β è conseguenza di {α, α→ β}.

α β α→ β

1 1 11 0 00 1 10 0 1

In particolare, una valutazione v che soddisfa α e α→ β soddisfaanche β.

Sonia L’Innocente (Camerino) 50 / 83

Sonia L’Innocente

Il problema della soddisfacibilità

Metodo efficiente?Il metodo delle tavole di verità è dunque molto semplice. Ha però ungrave difetto: infatti, se α è una formula con n variabili proposizionalip0, . . . , pn−1, le possibili sequenze (v(p0), . . . , v(pn−1)), quando vvaria tra le valutazioni, esauriscono tutto {0, 1}n, e sono dunque 2n.

L’impostazione della tavola di verità di α richiede 2n passi; segue che ilmetodo richiede troppo tempo e troppo spazio quando n è grande.

Si pone il problema di ottenere algoritmi più pratici ed efficienti.

Sonia L’Innocente (Camerino) 51 / 83

Sonia L’Innocente

Forme normali e clausole

Outline

1 Introduzione

2 Semantica e valutazioni

3 Cenni di sintassi

4 Connettivi, forme normali

5 Il problema della soddisfacibilità

6 Forme normali e clausole

7 Il Teorema di decomposizione

8 Il Teorema di risoluzione

Sonia L’Innocente (Camerino) 52 / 83

Sonia L’Innocente

Forme normali e clausole

Nella ricerca di nuovi metodi più veloci per il problema dellasoddisfacibilità, possiamo allora cercare intanto un metodo effettivoper tradurre una arbitraria formula α in una formula in DNF o in CNFlogicamente equivalente ad α. Illustremo tale metodo.

Sonia L’Innocente (Camerino) 53 / 83

Sonia L’Innocente

Forme normali e clausole

Riduzione in DNF o in CNF.

Sia α una formula. Per ottenere una formula in DNF o in CNFlogicamente equivalente ad α si esegue il seguente programma.

(a) Eliminare↔ in α (basta ricordare che, se β e γ sono due formule,allora β ↔ γ è logicamente equivalente a (β → γ) ∧ (γ → β)).

(b) Eliminare→ (per ogni scelta di β e γ, β → γ è logicamenteequivalente a ¬β ∨ γ).

(c) Eliminare ogni connettivo ¬ che non riguardi direttamente variabiliproposizionali (ricordare che, per ogni scelta di β e γ, sonologicamente equivalenti ¬¬β e β, ¬(β ∧ γ) e ¬β ∨ ¬γ, ¬(β ∨ γ) e¬β ∧ ¬γ).

Sonia L’Innocente (Camerino) 54 / 83

Sonia L’Innocente

Forme normali e clausole

Sappiamo che valgono le proprietà distributive tanto di ∧ rispetto a ∨quanto di ∨ rispetto a ∧: infatti, per ogni scelta di β, γ e δ in F , sonologicamente equivalenti le formule β ∧ (γ ∨ δ) e (β ∧ γ) ∨ (β ∧ δ),β ∨ (γ ∧ δ) e (β ∨ γ) ∧ (β ∨ δ)).

Così un semplice trucco per ridurre, dopo il passo (c), la formula α inDNF è quello di sostituire in α ∨ e ∧ rispettivamente con + e ·, fare icalcoli come se α fosse un polinomio e, dopo aver ridotto il polinomioin forma normale (somma di prodotti di variabili proposizionali),mettere nuovamente ∨ e ∧ al posto di + e ·. Naturalmente, se sipreferisce CNF a DNF , il trucco è lo stesso; basta avere laprecauzione di sostituire stavolta ∧ con + e ∨ con ·. Sintetizzando,l’ultimo passo del programma di riduzione a DNF o CNF è:

(d) usare le proprietà distributive di ∧ (∨) rispetto a ∨ (∧).

Sonia L’Innocente (Camerino) 55 / 83

Sonia L’Innocente

Forme normali e clausole

Proseguiamo la ricerca di un algoritmo per il problema dellasoddisfacibilità. Sia α una formula in CNF , ad esempio:

α :∧i≤n

∨j≤mi

λi,j

con n, mi ∈ N e formule basiche λi,j .Cambiando notazione, possiamo scrivere α come un insieme (finito enon vuoto) di insiemi (finiti e non vuoti) di formule basiche ponendo:

α = {{λi,j : j ≤ mi} : i ≤ n}.

In generale, possiamo dare la seguente definizione.

Definizione. Clausola è un insieme finito di formule basiche.

Sonia L’Innocente (Camerino) 56 / 83

Sonia L’Innocente

Forme normali e clausole

Ogni formula in CNF definisce un insieme finito e non vuoto diclausole non vuote. Esistono altri insiemi finiti di clausole:

• l’insieme vuoto ∅;

• gli insiemi contenenti la clausola vuota.

Nel seguito porremo

� = clausola vuota

Sonia L’Innocente (Camerino) 57 / 83

Sonia L’Innocente

Forme normali e clausole

Ricordiamo che, se v è una valutazione e α è una formula di CNF ,rappresentata nella forma ∧

i≤n

∨j≤mi

λi,j ,

o anche come insieme finito e non vuoto di clausole non vuote

{{λi,j : j ≤ mi} : i ≤ n},

allora v soddisfa α (v |= α) se e solo se, per ogni i ≤ n, esiste j ≤ mitale che v(λi,j) = 1. Poniamo allora la seguente definizione.

Definizione. Siano v una valutazione, α un insieme finito di clausole.Si dice che v soddisfa α, e si scrive v |= α, se e solo se, per ognik ∈ α, esiste λ ∈ k tale che v(λ) = 1.

Sonia L’Innocente (Camerino) 58 / 83

Sonia L’Innocente

Forme normali e clausole

Inoltre:

• ogni valutazione v soddisfa ∅ (non esiste alcuna clausola in ∅);

• se α è un insieme finito di clausole e � ∈ α, allora nessunavalutazione v soddisfa α (infatti � è una clausola di α, ma non esistealcun formula basica λ in �).

Possiamo adesso dare la seguente definizione.

Definizione. Diciamo che un insieme finito di clausole α èsoddisfacibile se e solo se esiste una valutazione v che soddisfa α.

Se poi α e α′ sono due insiemi finiti di clausole, diciamo che α′ èconseguenza logica di α, e scriviamo α |= α′, se ogni valutazione vche soddisfa α soddisfa anche α′. Ad esempio, è facile osservare che,se α′ ⊆ α, allora α |= α′.

Finalmente definiamo due insiemi finiti di clausole α e α′ logicamenteequivalenti se sono soddisfatti dalle stesse valutazioni.

Sonia L’Innocente (Camerino) 59 / 83

Sonia L’Innocente

Forme normali e clausole

Lemma.Siano α un insieme finito di clausole, k ∈ α, λ una variabileproposizionale tale che tanto λ quanto ¬λ appartengono a k. Allora αe α− {k} sono logicamente equivalenti.

Dimostrazione.Se v |= α, si ha v |= α− {k} perché α− {k} ⊆ α. Supponiamo allorav |= α− {k}; siccome v(λ) = 1 o v(¬λ) = 1, esiste comunque µ ∈ ktale che v(µ) = 1. Dunque v |= α. a

Sonia L’Innocente (Camerino) 60 / 83

Sonia L’Innocente

Forme normali e clausole

Possiamo poi assumere che, per ogni clausola k in α e per ognivariabile proposizionale λ,

λ 6∈ k oppure ¬λ 6∈ k .

Infatti, se α contiene una clausola k tale che, per qualche formulabasica λ, tanto λ quanto ¬λ appartengono a k , allora α èsoddisfacibile se e solo se α− {k} è soddisfacibile.

Sonia L’Innocente (Camerino) 61 / 83

Sonia L’Innocente

Forme normali e clausole

Conviene allora introdurre, a proposito di α e della formula basica λ, laseguente notazione:

α0λ = {k ∈ α : λ 6∈ k , ¬λ 6∈ k},

α+λ = {k ∈ α : λ ∈ k},

α−λ = {k ∈ α : ¬λ ∈ k}

(allora α0λ, α+

λ , α−λ formano una partizione di α: sono a due a duedisgiunti e α0

λ ∪ α+λ ∪ α

−λ = α); poniamo anche:

Posλ(α) = α0λ ∪ {k − {λ} : k ∈ α+

λ },

Negλ(α) = α0λ ∪ {k − {¬λ} : k ∈ α−λ }

(naturalmente, quando λ = ¬µ è la negazione di una variabileproposizionale, si intende ¬λ = µ)

Sonia L’Innocente (Camerino) 62 / 83

Sonia L’Innocente

Forme normali e clausole

Esempio.

Siano

α = {{p0, ¬p1, p2}, {¬p0,¬p1, p2}, {p1, ¬p2}, {p0}}, λ = p0.

Alloraα0λ = {{p1,¬p2}},

α+λ = {{p0, ¬p1, p2}, {p0}},

α−λ = {{¬p0, ¬p1, p2}},

Posλ(α) = {{p1,¬p2}, {¬p1, p2}, �},

Negλ(α) = {{p1,¬p2}, {¬p1, p2}}.

Sonia L’Innocente (Camerino) 63 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Outline

1 Introduzione

2 Semantica e valutazioni

3 Cenni di sintassi

4 Connettivi, forme normali

5 Il problema della soddisfacibilità

6 Forme normali e clausole

7 Il Teorema di decomposizione

8 Il Teorema di risoluzione

Sonia L’Innocente (Camerino) 64 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Teorema (di decomposizione). Siano α un insieme finito di clausole,λ una variabile proposizionale. Allora α è soddisfacibile se e solo sePosλ(α) o Negλ(α) è soddisfacibile.

Sonia L’Innocente (Camerino) 65 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Osservazione

Sia α una formula in CNF con variabili proposizionali tra p0, . . . , pn−1.Sappiamo che α è soddisfacibile se e solo se Posλ(α) oppure Negλ(α)è soddisfacibile. Dunque, per controllare la soddisfacibilità di α, bastacontrollare quella di

Pospi (α), Negpi (α),

per qualche i < n; Pospi (α) e Negpi (α) hanno il vantaggio di avere unavariabile proposizionale in meno perché pi non occorre né in Pospi (α)né in Negpi (α); conviene anzi scegliere i < n tale che pi (o ¬pi ) ha ilmassimo numero di occorrenze in α.

Sonia L’Innocente (Camerino) 66 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Corollario 1 (regola della formula basica pura).Se α ∈ CNF (o, più in generale, α è un insieme finito di clausole), λ èuna formula basica e α−λ = ∅ (cioè ¬λ non occorre mai nelle clausoledi α), allora α è soddisfacibile se e solo se α0

λ è soddisfacibile.

Dimostrazione. Infatti, se α è soddisfacibile, anche α0λ ⊆ α è

soddisfacibile. Viceversa supponiamo α0λ soddisfacibile; siccome

α−λ = ∅, Negλ(α) = α0λ, e dunque Negλ(α) è soddisfacibile. Per il

Teorema di decomposizione, α è soddisfacibile. a

Sonia L’Innocente (Camerino) 67 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Corollario 2 (regola della clausola unitaria).Se α ∈ CNF e, per qualche formula basica λ, {λ} è una clausola di α,allora α è soddisfacibile se e solo se Negλ(α) è soddisfacibile.

Dimostrazione. Se {λ} ∈ α, allora {λ} ∈ α+λ e dunque � = {λ} − {λ}

appartiene a Posλ(α). Segue che Posλ(α) non è soddisfacibile. La tesiè allora un caso particolare del Teorema di decomposizione. a

Sonia L’Innocente (Camerino) 68 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Diamo adesso alcuni esempi di applicazione del Teorema didecomposizione e delle regole di Davis-Putnam.

Esempi

1. Sia dapprima

α = {{¬p0, ¬p1, p2}, {¬p0, ¬p1, p3}, {¬p4, ¬p5, p6},

{¬p6, ¬p3, p7}, {p0}, {p1}, {p4}, {p5}, {¬p7}}.

Allora α non è soddisfacibile. Infatti, con uso ripetuto della regola dellaclausola unitaria, possiamo vedere che α è soddisfacibile se e solo serisultano successivamente soddisfacibili i seguenti insiemi finiti diclausole:

Sonia L’Innocente (Camerino) 69 / 83

Sonia L’Innocente

Il Teorema di decomposizione

{{¬p1, p2}, {¬p1, p3}, {¬p4, ¬p5, p6}, {¬p6,¬p3, p7},

{p1}, {p4}, {p5}, {¬p7}},

e poi

{{p2}, {p3}, {¬p4, ¬p5, p6}, {¬p6, ¬p3, p7}, {p4}, {p5}, {¬p7}},

{{p2}, {¬p4, ¬p5, p6}, {¬p6, p7}, {p4}, {p5}, {¬p7}},

{{p2}, {¬p4, p6}, {¬p6, p7}, {p4}, {¬p7}},

{{p2}, {p6}, {¬p6, p7}, {¬p7}},

{{p2}, {p6}, {¬p6}},

{{p2}, �}

(si considerino nell’ordine le clausole unitarie {p0}, {p1}, {p3}, {p5},{p4}, {¬p7}, {p6}). L’ultimo insieme di clausole non è soddisfacibileperché contiene �.

Sonia L’Innocente (Camerino) 70 / 83

Sonia L’Innocente

Il Teorema di decomposizione

2.

Sia adesso

α = {{p0, p1, ¬p2, p3}, {¬p0, ¬p1, ¬p2, p3}, {¬p0, ¬p1, ¬p2}}.

Siccome α−¬p2= ∅, si può usare la regola della formula basica pura per

λ = ¬p2. Dato che α0¬p2

= ∅ è soddisfacibile, anche α lo è.

3. Finalmente consideriamo

α = {{p0, ¬p1}, {p0, p2}, {¬p0, ¬p1}, {¬p0, p3}, {p1, ¬p2}, {p1, ¬p3}}.

Applicando il Teorema di decomposizione per λ = p0, si ha che α èsoddisfacibile se e solo se uno dei seguenti insiemi è soddisfacibile:

Posp0(α) = {{¬p1}, {p2}, {p1, ¬p2}, {p1, ¬p3}},

Negp0(α) = {{¬p1}, {p3}, {p1, ¬p2}, {p1, ¬p3}}.

Sonia L’Innocente (Camerino) 71 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Consideriamo dapprima Posp0(α); con la regola della clausola unitariaapplicata a p2, si ottiene:

{{¬p1}, {p1}, {p1, ¬p3}},

da cui si passa, ancora con la regola della clausola unitaria, stavoltaapplicata a p1, a {�}, che è non soddisfacibile. Segue che Posp0(α)non è soddisfacibile. Allo stesso modo si vede che anche Negp0(α)non è soddisfacibile (basta ripetere i passaggi per Posp0(α) invertendoi ruoli di p2 e p3). Dunque neppure α lo è.

Sonia L’Innocente (Camerino) 72 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Algoritmo per il problema della soddisfacibilità suggerito dalTeorema di DecomposizioneData formula α in CNF , con variabili proposizionali tra p0, . . . , pn−1, èo no soddisfacibile: determinare prima

Posp0(α), Negp0(α)

(che hanno variabili proposizionali tra p1, . . . , pn−1), poi

Posp1(Posp0(α)), Negp1(Posp0(α))

ePosp1(Negp0(α)), Negp1(Negp0(α)),

(che hanno variabili proposizionali tra p2, . . . , pn−1), e così via. Sidetermina in questo modo un albero 2-adico con n livelli e, quindi, 2n

rami. Al termine di ciascun ramo si trova un insieme finito di clausolenon contenenti alcuna formula basica, dunque coincidenti con ∅oppure con {�}.

Sonia L’Innocente (Camerino) 73 / 83

Sonia L’Innocente

Il Teorema di decomposizione

Algoritmo per il problema della soddisfacibilità suggerito dalTeorema di DecomposizionePer il Teorema di decomposizione, α è soddisfacibile sse, ad ognilivello dell’albero, almeno un nodo è soddisfacibile. Ricordiamo che ∅ èsoddisfatto da ogni valutazione, mentre {�} non è soddisfacibile.

α è soddisfacibile se e solo se al termine di almeno un ramo si trova ∅.In particolare il metodo richiede, se α ha n variabili proposizionali, diesplorare 2n rami di un albero. Si presta perciò alle medesime critichedelle tavole di verità: è, in generale, troppo lento. Naturalmente, in casiparticolari (come quelli relativi agli esempi precedenti), l’uso delTeorema di decomposizione e delle regole di Davis-Putnam permetteun rapido controllo della soddisfacibilità della formula proposta.

Sonia L’Innocente (Camerino) 74 / 83

Sonia L’Innocente

Il Teorema di risoluzione

Outline

1 Introduzione

2 Semantica e valutazioni

3 Cenni di sintassi

4 Connettivi, forme normali

5 Il problema della soddisfacibilità

6 Forme normali e clausole

7 Il Teorema di decomposizione

8 Il Teorema di risoluzione

Sonia L’Innocente (Camerino) 75 / 83

Sonia L’Innocente

Il Teorema di risoluzione

Definizione.Siano k1, k2 due clausole, λ una variabile proposizionale tale cheλ ∈ k1 e ¬λ ∈ k2. Si dice risolvente di k1 e k2 rispetto a λ, e si indicacon resλ(k1, k2), la clausola (k1 − {λ}) ∪ (k2 − {¬λ}).

Esempio. Siano k1 = {p0, p1}, k2 = {¬p0, p2}, λ = p0. Allora

resλ(k1, k2) = {p1, p2}.

Si noti che, per ogni valutazione v , se v |= {k1, k2}, allora v(p1) = 1oppure v(p2) = 1, e dunque v |= {resλ(k1, k2)}.

Sonia L’Innocente (Camerino) 76 / 83

Sonia L’Innocente

Il Teorema di risoluzione

Lemma 1.Siano k1, k2 clausole, λ una variabile proposizionale tale che λ ∈ k1 e¬λ ∈ k2. Allora {k1, k2} |= {resλ(k1, k2)}.

Risolvente di una formulaSia α ∈ CNF (o, più in generale, sia α un insieme finito di clausole), esia λ una variabile proposizionale. Poniamo

RESλ(α) = α0λ ∪ {resλ(k1, k2} : k1 ∈ α+

λ , k2 ∈ α−λ }.

Sonia L’Innocente (Camerino) 77 / 83

Sonia L’Innocente

Il Teorema di risoluzione

Lemma 2.Siano α ∈ CNF (o comunque un insieme finito di clausole), λ unavariabile proposizionale. Allora α è soddisfacibile se e solo seRESλ(α) è soddisfacibile.

Dimostrazione. (=⇒) Proviamo che, addirittura, ogni valutazione v chesoddisfa α soddisfa anche RESλ(α). Sia k ∈ RESλ(α), cerchiamoµ ∈ k tale che v(µ) = 1. Se k ∈ α0

λ, allora k ∈ α, e la tesi è ovvia. Siaallora k = resλ(k1, k2) con k1 ∈ α+

λ e k2 ∈ α−λ . Allora {k1, k2} ⊆ α,dunque v |= {k1, k2}. Per il Lemma 1, v |= {k}, ovvero esiste µ ∈ ktale che v(µ) = 1.

Sonia L’Innocente (Camerino) 78 / 83

Sonia L’Innocente

Il Teorema di risoluzione

Dimostrazioen del Lemma 2 (seconda parte)

(⇐=) Per il Teorema di decomposizione, basta provare che, se v è unavalutazione che soddisfa RESλ(α), allora v soddisfa Posλ(α) oppureNegλ(α). Dunque supponiamo che v |= RESλ(α) ma v 6|= Posλ(α), edimostriamo che, in questo caso,v |= Negλ(α) = α0

λ ∪ {k2 − {¬λ} : k2 ∈ α−λ }. Chiaramente v |= α0λ

perché α0λ ⊆ α. Sia ora k2 ∈ α−λ ; sappiamo che esiste k ∈ Posλ(α) tale

che, per ogni µ ∈ k , v(µ) = 0, e, siccome v |= α0λ, deve essere

k = k1 − {λ} per un’opportuna clausola k1 ∈ α+λ . Per ipotesi

v |= {resλ(k1, k2)}, cioè esiste µ ∈ resλ(k1, k2) tale che v(µ) = 1; manon può essere µ ∈ k1 − {λ} = k , dunque µ ∈ k2 − {λ}. Inconclusione, v |= Negλ(α). a

Sonia L’Innocente (Camerino) 79 / 83

Sonia L’Innocente

Il Teorema di risoluzione

Il lemma 2 suggerisce già un algoritmo per controllare lasoddisfacibilità di una formula α ∈ CNF .

Se le variabili proposizionali di α sono tra p0, . . . , pn−1, si costruisconosuccessivamente

α0 = α

e, per ogni i con 0 < i < n,

αi+1 = RESpi (αi).

Allora, per ogni i < n, le variabili proposizionali nelle clausole di αisono tra pi , . . . , pn−1, e αi è soddisfacibile sse lo è α.

Le clausole di αn non contengono alcuna variabile proposizionale, edunque αn = ∅ oppure αn = {�}. Se αn = ∅, allora α è soddisfacibile,mentre, se αn = {�}, α non è soddisfacibile.

Sonia L’Innocente (Camerino) 80 / 83

Sonia L’Innocente

Il Teorema di risoluzione

Definizione.Sia α ∈ CNF . Si dice confutazione di α una sequenza finita k0, . . . , kmdi clausole tali che km = � e, per ogni i ≤ m, ki ∈ α o esistono j , h < ied una variabile proposizionale λ tali che λ ∈ kj , ¬λ ∈ kh eki = resλ(kj , kh).

Teorema di risoluzione.Sia α ∈ CNF. Allora α non è soddisfacibile sse esiste unaconfutazione di α.

Sonia L’Innocente (Camerino) 81 / 83

Sonia L’Innocente

Il Teorema di risoluzione

Esempio.

Siaα = {{¬p0, ¬p1, p2}, {¬p0, ¬p1, p3}, {¬p4, ¬p5, p6},{¬p6, ¬p3, p7}, {p0}, {p1}, {p4}, {p5}, {¬p7}}.

Abbiamo già provato, con l’uso delle regole di Davis-Putnam, che αnon è soddisfacibile. Ecco una confutazione di α:

k0 = {¬p0, ¬p1, p3} ∈ α,

k1 = {¬p6, ¬p3, p7} ∈ α,k2 = {¬p0, ¬p1, ¬p6, p7} = resp3(k0, k1),

k3 = {p0} ∈ α,k4 = {¬p1, ¬p6,p7} = resp0(k3, k2),

k5 = {p1} ∈ α,k6 = {¬p6, p7} = resp1(k5, k4),

Sonia L’Innocente (Camerino) 82 / 83

Sonia L’Innocente

Il Teorema di risoluzione

k7 = {¬p7} ∈ α,

k8 = {¬p6} = resp7(k6, k7),

k9 = {¬p4, ¬p5, p6} ∈ α,

k10 = {¬p4, ¬p5} = resp6(k9, k8},

k11 = {p4} ∈ α,

k12 = {¬p5} = resp4(k11, k10),

k13 = {p5} ∈ α,

k14 = � = resp5(k13, k12).

Si può comunque mostrare che anche il metodo ora descritto, perquanto più rapido dei precedenti in qualche caso particolare ha tuttavialo stesso difetto: è troppo lento.

Sonia L’Innocente (Camerino) 83 / 83