Appunti del corso: Intelligenza Artificiale II Dimostrazione automatica di Teoremi Prof. Maurizio...

transcript

Appunti del corso: Intelligenza Artificiale II

Dimostrazione automatica di Teoremi

Prof. Maurizio MartelliDISI

Università di Genova

Calcolo dei predicati• linguaggio per esprimere concetti e loro relazioni e che permette di

inferire proposizioni da altre considerate vere.

SINTASSI (si prescinde dal significato)

• Alfabeto (a,b,...,A,B,...,(,),..., ⊆,≤,...,←,∃,...)• Simboli:

- Costanti di oggetti: C (a,b,casa, 23, ...)di funzione: F (+,-, padre, ...) con aritàdi predicato: P (<,=,pari,...) con arità

- Variabili: V (X,Y,...)

• Termini:

i) una variabile X ∈ V è un termine

ii) una costante c ∈ C è un termine

iii) l’applicazione (f(t1,...,tn)) di un simbolo di funzione n-ario f ∈ F

ad n termini t1,...,tn è un termine

iv) non esistono altri termini

termine ground - senza variabili(oggetti dell'Universo del discorso)

Es.: padre(padre(giovanni))

Calcolo dei predicati

• Atomi: {p(t1,..,tn) |p ∈ P, t1,..,tn termini}

Es.: fattoriale (3,6)uomo(paolo)maggiore(X,3)maggiore(più(X,1),Y)ama(giovanni,maria)ama(padre(giovanni),giovanni)ama(padre(padre(giovanni)),giovanni)maggiore(più(più(1,giovanni),Y),padre(3))

• Formule Ben Formate (fbf):- Atomi

- frasi logiche: se F, F1, F2 sono fbf

- negazione ~F

- congiunzione F1∧ F2 - disgiunzione F1∨F2

- implicazione F1← F2 - equivalenza F1↔ F2

- frasi quantificate: se Fè una fbf e X ∈ V

- universalmente (∀X.F) - esistenzialmente (∃X.F)

- non esistono altre fbf

• Il linguaggio del prim’ordine definito da un alfabeto è l’insieme di tutte le fbf

costruite con i simboli dell’alfabeto

• Occorrenza di variabile vincolata:

i) se compare all’interno di un quantificatore

ii) se compare nello scope di un quantificatore per quella variabile

• Una variabile è libera in una fbf se almeno una sua occorrenza è non

vincolata

• Una formula è chiusa se non contiene variabili libere

• Se f è una formula aperta,

∃(f) e ∀(f) denotano le chiusure esistenziale e universale di f

• importanza dell' ordine dei quantificatori.

• Ordine: primo, secondo, ... omega

LINGUAGGI DEL PRIM’ORDINE: SINTASSI, ESEMPI

• un esempio filosofico

(∀X)(uomo(X) → mortale(X)) ∧ uomo(socrate) → mortale(socrate)

• due degli assiomi di base dei numeri naturali

(interpretare

• f e g come funzioni successore e predecessore

• la costante 0 come zero

• il predicato u come uguaglianza )

(∀X)(∃Y)(u(Y,f(X)) ∧ (∀Z)(u(Z,f(X)) → u(Y,Z)))

(∀X)( ~u(X,0) → ((∃Y)(u(Y,g(X)) ∧ (∀Z)(u(Z,g(X)) → u(Y,Z)))))

• nella formula (∀X)p(X,Y), tutte le occorrenze di X sono vincolate, mentre Y è

libera

• Y è libera anche nella formula : (∀X)p(X,Y) ∧ (∀Y)q(Y)

Calcolo dei predicatiSEMANTICA (relazione tra frasi e concetti)

Dare una interpretazione alle espressioni sintatticamente corrette. Definire se

certe espressioni sono vere o false in base al significato che si dà ai

componenti l'espressione.

•Interpretazione (I):

-Dominio D

-funzione da C a D

-funzione da F a (Dn→D)

-funzione da P a (Dn→ {T,F})

•interpretazione intesa, altre int.

•assegnamento di variabili (U):

-funzione da V a D

•assegnamento di termini: (T)

combinazione di I ed U

• soddisfacimento ( ⊨I ): ⊨I F[U]

vale se F è vera per I e U, cioè interpretata nel dominio D di I.

- ⊨ Ip(t1,..,tn)[U] iff pI(I(t1),..,I(tn)) = T

- ⊨ I ~F[U] iff ⊨I F[U] non è vera

- ⊨ I F1 ^ F2[U] iff ⊨I F1[U] e ⊨I F2[U]

- ⊨ I F1 v F2[U] iff ⊨I F1[U] o ⊨I F2[U]

- ⊨ I F1 ← F2[U] iff ⊨I F1[U] o non ⊨I F2[U]

- ⊨ I F1↔ F2[U] iff ⊨I F1 ← F2[U] e ⊨I F2 ← F1[U]

- ⊨ I (∀X.F)[U] iff per ogni d ∈ D ⊨I F[V]

con V identica ad U tranne che V(X)=d.

- ⊨ I (∃X.F)[U] iff per qualche d ∈D ⊨I F[V]

con V identica ad U tranne che V(X)=d.

• ⊨ I una interpretazione I che soddisfa F per tutti i possibili assegnamenti di

variabile si dice un MODELLO di F: ⊨ I F

LINGUAGGI DEL PRIM’ORDINE: SEMANTICA, ESEMPI

f = (∀X) p(X) → q(f(X),a)un’interpretazione ID = {1,2}[a] = 1[f(1)] = 2 [f(2)] = 1[p(1)] = F [p(2)] = T[q(1,1)] = T [q(1,2)] = T[q(2,1)] = F [q(2,2)] = Tla valutazione di f in I è T (I è un modello di f),

se X=1,

p(1) → q(f(1),a) =

p(1) → q(2,1) =

F → F = T se X=2,

p(2) → q(f(2),a) =

p(2) → q(1,1) =

T → T = T

LINGUAGGI DEL PRIM’ORDINE: SEMANTICA, ESEMPI

f = (∀X) (∃Y) p(X) Λ q(X,Y)

un’interpretazione I

D = {1,2}

[a] = 1

[f(1)] = 2 [f(2)] = 1

[p(1)] = F [p(2)] = T

[q(1,1)] = T [q(1,2)] = T

[q(2,1)] = F [q(2,2)] = T

la valutazione di f in I è F (I non è un modello di f),

se X=1,

se Y=1,

p(1) ^ q(1,1) = F

se Y=2,

p(1) ^ q(1,2) = F

• una interpretazione I che soddisfa tutte le formule di un insieme T (teoria)

per tutti i possibili assegnamenti di variabile si dice un MODELLO di T: ⊨I T

• F è conseguenza logica di una teoria T :

T ⊨I F

iff ogni modello di T è anche modello di F

• T è soddisfacibile

iff T ha almeno un modello

• T è insoddisfacibile (inconsistente)

iff T non ha alcun modello

• F è valida ⊨ F

iff F è soddisfatta per ogni I e per ogni U (ogni interpretazione è

un modello)

• teoria assiomatica

- assiomi logici (logicamente validi)

- assiomi non logici (conoscenza specifica)

- regole di inferenza (permettono di ricavare nuove fbf da insiemi di fbf)

Es: Modus Ponens: A B← A

• dimostrazione :

sequenza finita di fbf (f1,..,fn), ciascuna delle quali è un assiomi o è

derivata dalle precedenti mediante una regola di inferenza.

• teorema: ultima formula di una dimostrazione

• se T è un insieme di formule (assiomi non logici) T ⊢ A indica che A è un

teorema per la teoria T.

• ⊢ A indica che A è un teorema (formula logicamente valida)

Equivalenza tra sintassi e semantica

• Correttezza:

i teoremi di una teoria sono veri in tutti i modelli della teoria

• Completezza:

le fbf che sono vere in tutti i modelli della teoria (seguono logicamente dagli

assiomi) sono teoremi della teoria.

• il calcolo dei predicati del prim'ordine è corretto e completo (nel caso di

assenza di assiomi non logici, i teoremi coincidono con le formule valide)

Stile dichiarativo della PL _______________________________

• orientato ad utenti non programmatori

• grande potere espressivo

• programma come insieme di formule (assiomi)

• computazione come costruzione di una dimostrazione di una formula (goal)

del prim'ordine

sintassi semantica

dim. di --correttezza-> conseguenza

teoremi <-- copletezza-- logica

• limitazione nel tipo di formule (clausole Horn) e utilizzazione di particolare

tecniche per la dimostrazione di teoremi (unificazione e risoluzione)

Conseguenze logiche e insoddisfacibilità

• Teorema di deduzione

T |= F G iff T {F} |= G

• Teorema: Sia S un insieme di formule (chiuse), f una formula (chiusa), di un linguaggio del prim'ordine L

f è una conseguenza logica di Siff

l'insieme S {~f} è insoddisfacibile

Sia I un modello di S, I è anche un modello di f e quindi non di ~f. Quindi non esiste interpretazione che sia modello di S e di ~f.

Sia I una interpretazione che sia modello di S ma non di ~f. I è anche

modello di f. Quindi f è conseguenza logica di S

Forme NormaliH=G iff i valori di verità coincidono per ogni interpretazione

Leggi di Equivalenza

1. HG = (HG)(GH)2. HG = H(G)3. HG = GH HG = GH4. (HP)G = H(PG) (HP)G = H(PG)5. (HP)G = (HG)(PG) (HP)G = (HG)(PG)6. Hf = H Ht = H7. Ht = t Hf = f8. HH = t HH = f9. (H) = H10. (HP) = HP11. (HP) = HP

Forme Normali• Principio di rimpiazzamento: In una formula si può

rimpiazzare una sua parte con una formula equivalente ed il valore di verità non cambia.

• Letterale: atomo o negazione di atomo• Forma normale congiuntiva:

F1F2Fn con Fi = L1 L2 Lm

• Forma normale disgiuntiva:

F1F2Fn con Fi = L1 L2 Lm

• Procedura di trasformazione:– (1) e (2)– (9), (10) e (11)– (5)– + semplificazioni

Forme Normali

• Forma normale prenessa (prenex):

(Q1x1)(Q2x2Qnxn) (M)

– (Qixi) è xi oxi.

– M è una formula senza quantificatori

– (Q1x1)(Q2x2Qnxn) è il prefisso

– M è la matrice (spesso in f.n. congiuntiva o disgiuntiva)

Forme Normali• Leggi di Equivalenza

1a) (Qx)F[x]G = (Qx)(F[x]G)

1b) (Qx)F[x]G = (Qx)(F[x]G)

2a) ~((x)F[x]) = (x)(~F[x])2b) ~((x)F[x]) = (x)(~F[x])3a) (x)F[x]x)G[x] = (x)(F[x]G[x])

3b) x)F[x]x)G[x] =x)(F[xG[x])

4a) (Q1x)F[x](Q2x)G[x] = (Q1x)(Q2y)(F[x]G[y])

4b) (Q1x)F[x](Q2x)G[x] = (Q1x)(Q2y)(F[x]G[y])

• Procedura di trasformazione:– (1) e (2)– (9) (10) (11) (2a,2b)– ridenominazione variabili, (1a,1b)(3a,3b)(4a,4b)– (5) + semplificazioni

Forma standard di SkolemSia F = (Q1x1)(Q2x2Qnxn) (M)

– Prendiamo (Qrxr) del tipo xr) e

– si esaminino i (Qixi) con i<r.

a) se non vi è nessun quantificatore universale

i<r. Qi= sostituiamo ogni occorrenza di xr in M con una costante c (diversa da tutte le altre in M) e togliamo (Qrxr).

b) altrimenti, consideriamo s1,s2sm :i≤m. si<r e Qsi= Sostituiamo ogni occorrenza di xr in M con un nuovo simbolo di funzione f (diverso da tutti gli altri in M) applicato ad xs1,xs2xsm

(f(xs1,xs2xsm)) e togliamo (Qrxr).

Clausole

• disgiunzione di atomi o negazioni di atomi, in cui le variabili sono implicitamente quantificate universalmente

A1 A2 AnB1B2~Bm

• La clausola vuota [] corrisponde a F• è equivalente a

(A1 A2 An) (B1 B2 Bm)che si scrive (conclusione premesse)

A1,A2 AnB1,B2,Bm

• insieme di clausole: congiunzione di clausole.

Teorema di Skolemizzazione• una teoria del prim'ordine si può ridurre in forma a

clausole con semplici trasformazioni sintattiche: T diventa T' vale la seguente proprietà:

T è insoddisfacibile iff lo è T'• Teorema:

Sia S un insieme di clausole che rappresenta una forma standard di Skolem di una formula F

F è insoddisfacibile iff S è insoddisfacibile

• si può anche rappresentare la conoscenza direttamente in forma a clausole

• è comunque una forma particolarmente conveniente per il compito di dimostrare automaticamente teoremi

Trasformazione in forma a Clausole

1. x.y. (P(x)Q(x,y)) R(x)(eliminazione del connettivo )

2. x. y. (P(x)Q(x,y)) R(x)(riduzione della portata della negazione)

3. x. y. (P(x) Q(x,y)) R(x)(distribuzione del connettivo )

4. x. y. (P(x) R(x)) (Q(x,y) R(x)) (Eliminazione del quantificatore esistenziale, introduzione di funzioni di Skolem)5. x. (P(x) R(x)) (Q(x,f(x)) R(x)) (eliminazione del quantificatore universale)6. (P(x) R(x)) (Q(x,f(x)) R(x))

(eliminazione del connettivo )

Insieme di clausole:{P(x) R(x), Q(x,f(x)) R(x)}

Skolemizzazione

Lemmasia S una formula in forma prenessa

(Q1 X1)…(Qn Xn) M(X1,…,Xn),

con Qr primo quantificatore esistenziale,

ed S1 la formula

( X1)…( Xr-1) (Qr+1 Xr+1)… (Qn Xn)

M(X1,…,Xr-1,f(X1,…,Xr1),Xr+1,…,Xn)

S è inconsistente iff S1 è inconsistente

Skolemizzazione Prova

i) supponiamo S inconsistente e S1 consistente, esiste I tale che S1 è vera in I: per tutti gli X1,…,Xr-1 esiste almeno un elemento, f(X1,…,Xr-1), tale che è vera in I (Qr+1Xr+1)…(QnXn) M(X1,…,Xr-1,f(X1,…,Xr-1),Xr+1,…,Xn)

quindi S sarebbe vera in I

ii) supponiamo S1 inconsistente e S consistente, esiste I (su D) tale che S è vera in I

per tutti gli X1,…,Xr-1 esiste almeno un elemento Xr tale che è vera in I (Qr+1 Xr+1)… (Qn Xn) M(X1,…,Xr-1,Xr,Xr+1,…,Xn) Sia I‘ l’interpretazione ottenuta estendendo I con una funzione f, tale

che, per tutti gli X1,…,Xr-1 in D, f(X1,…,Xr-1) = Xr per tutti gli X1,…,Xr-1 (Qr+1 Xr+1)… (Qn Xn) M(X1,…,Xr-1,f(X1,…,Xr-1),Xr+1,…,Xn) è vera in I', cioè S1 sarebbe vera in I'

SkolemizzazioneTeorema

Sia C l’insieme di clausole risultante dalla skolemizzazione dell’insieme di fbf S.

S è inconsistente iff C è inconsistente.Prova

S può essere un’unica formula in forma prenessa.Si assuma che in S esistano m quantificatori esistenziali e si consideri la sequenza di formule

S0 = S

Skè ottenuto da Sk-1, sostituendo il primo quantificatore

esistenziale in Sk-1 con una funzione di Skolem gk, k=1,…,mSm= C

Per il lemma precedente, Sk è inconsistente iff Sk-1 è inconsistente, quindi C è inconsistente iff S è inconsistente

SkolemizzazioneSia C l’insieme di clausole risultante dallaskolemizzazione dell’insieme di fbf S se S è consistente, C non è necessariamente

equivalente a SEsempio• S = { (X) p(X) }• C = { p(a) }• un’interpretazione I

D = {1,2}[a] = 1[p(1)] = F [p(2)] = T

• I è un modello di S e non di C

LA METODOLOGIA DI PROVA 1. W è conseguenza logica di T iff

siano S un insieme di formule e f una formula di un linguaggio del prim’ordine Lf è una conseguenza logica di S iff l’insieme S {~f } è

insoddisfacibile

2. {T ~W} è insoddisfacibile iff

sia C l’insieme di clausole risultante dalla skolemizzazione dell’insieme

di fbf S S è inconsistente iff C è inconsistente

3. T', insieme di clausole ottenuto skolemizzando {T ~W} è insoddisfacibile iff

un insieme di clausole C è insoddisfacibile iff non ha modelli di Herbrand

4. T' non ha modelli di Herbrand

basta considerare le interpretazioni su un particolare dominio, l’Universo di Herbrand

UNIVERSO E BASE DI HERBRAND Sia L un linguaggio del prim’ordine, il cui insieme di costanti non sia vuoto (se è vuoto, lo consideriamo formato da una costante arbitraria a)

• L’Universo di Herbrand di L (UL) è l’insieme di tutti i termini ground di L• Un termine (atomo) ground è un termine (atomo)

che non contiene variabili• Un’istanza ground di una clausola C in L è una

clausola ottenuta da C sostituendo le variabili con termini di UL

• La Base di Herbrand di L (BL) è l’insieme di tutti gli atomi ground di L, cioè di tutte le formule ottenute applicando i predicati di L agli elementi di UL

UNIVERSO E BASE DI HERBRANDUniverso di Herbrand per un insieme di clausole S:• H0 = {c0,…,cn} ci costanti in S (sempre almeno una)

• Hi+1 = Hi {f(t1,…,tn)| f è un simbolo di funzione n-ario e i tjHi }

• HU = Hi

• Base di Herbrand per un insieme di clausole S:

– B = {p(t1,…,tn)| p è un simbolo di predicato n-ario e i ti HU }

• Esempio: il linguaggio L della teoria del prim’ordine

1. p(0,X,X)2. ~p(X,Y,Z) V p(s(X),Y,s(Z))

UL = {0,s(0),s(s(0)),…}

BL = {p(0,0,0), p(s(0),0,0),p(s(0),s(0),0),…}

INTERPRETAZIONI DI HERBRAND (H-interpretazione) per L è

un’interpretazione tale che:

i) il suo dominio è UL

ii) ad ogni costante a di L è assegnata la costante

stessaiii) ad ogni funzione n-aria f di L è assegnata la

funzione da (UL)n a UL, che assegna il

termine f(t1,…,tn) alla n-upla di termini t1,…,tn

iv) ad ogni predicato n-ario p in L è assegnato un insieme di n-uple di termini di UL

INTERPRETAZIONI E MODELLI

DI HERBRAND

• ogni H-interpretazione per L è determinata in modo univoco da un sottoinsieme qualunque (anche vuoto) di BL, che definisce l’insieme degli atomi ground che sono veri

• sia A un insieme di formule chiuse del linguaggio del prim’ordine L

un modello di Herbrand (H-modello) di A è una qualunque H-interpretazione I tale che tutte

le formule in A sono vere in I

• abusi di notazione: Universo, Base, Interpretazioni, Modelli di Herbrand indiciati dall’insieme di formule (programma) invece che dal relativo linguaggio del prim’ordine

INTERPRETAZIONI DI HERBRAND: UN

ESEMPIO l’insieme di clausole A

1. p(0,X,X)2. ~p(X,Y,Z) V p(s(X),Y,s(Z))

UA = {0,s(0),s(s(0)),…}

BA = {p(0,0,0), p(s(0),0,0),p(s(0),s(0),0),…}

IA1= {p(0,0,0), p(0,s(0),s(0)),p(s(0),0,s(0)),

p(0,s(s(0)),s(s(0))),…}

IA2= {p(0,0,s(0)), p(0,s(0),s(0)),p(s(0),0,s(0)),

p(0,s(s(0)),s(s(0))),…}

IA2 non è certamente un H-modello di A

CLAUSOLE E INTERPRETAZIONI DI

HERBRAND Teorema: Ogni insieme consistente di clausole S ha un H-

modello

sia I un modello di S e definiamo la H-interpretazione (corrispondente)

I' = { p(t1,…,tn) BS | p(t1,…,tn) è vera in I }

è evidente che anche I' è un modello di S

[attenzione al caso di assenza di costanti]

Corollario

Un insieme di clausole S è insoddisfacibile iff non possiede modelli di Herbrand

il teorema ed il corollario non valgono per insiemi di formule chiuse arbitrarie

UNA TEORIA CONSISTENTE SENZA H-MODELLI 1. p(a) 2. ~( X) p(X)

la teoria è consistente, come dimostrato dal modelloD = {0,1}a = 0p(0) = tp(1) = f

l’Universo di Herbrand {a}

la base di Herbrand {p(a)}

le H-interpretazioni {} {p(a)}

nessuna H-interpretazione è un modello!

il problema è legato alle quantificazioni esistenziali:c’è ( X)~p(X)

nell’assioma 2; nella versione skolemizzata introdurrebbe una nuova costante (di Skolem)

CLAUSOLE E H-INTERPRETAZIONI: PROPRIETA'

• una H-interpretazione è un sottinsieme della base e si può pensare di reppresentarla come l'insieme di tutti i letterali ground veri

I = {p(a), ~p(f(a)), p(f(f(a))), ....}

• una istanza ground c' di una clausola c è soddisfatta in una

H-interpretazione I iff c' I ≠

• una clausola c è soddisfatta in una H-interpretazione I iff

ogni istanza ground lo è.

• una clausola c è falsificata in una H-interpretazione I iff

c'è almeno una istanza ground che lo è.

• un insieme di clausole S è insoddisfacibile iff per ogni H-interpretazione I, c'è almeno una istanza ground di qualche c in S che non è soddisfatta da I.

CLAUSOLE, H-INTERPRETAZIONIE PROGRAMMAZIONE LOGICA

la maggior parte della teoria della programmazione logica ha a che fare solo con clausole

è sufficiente restringersi alle H-interpretazioni

alcune parti della teoria (completamento per trattare la negazione) richiedono l’uso di fbf non clausali

è necessario considerare interpretazioni arbitrarie

ALBERI SEMANTICI l’insieme di tutte le H-interpretazioni può essererappresentato da un albero (l’albero semantico), i cui archi sono etichettati da assegnamenti divalori di verità agli atomi della Base di Herbrand tali che:– per ogni nodo N vi è un numero finito di archi che

partono da N (L1, …,Ln). Sia Qi la congiunzione di

tutti i letterali che etichettano Li. Q1 …Qn è una

formula proposizionalmente valida.– per ogni nodo N, sia I(N) = insieme dei letterali

che etichettano gli archi del cammino dalla radice a N. I(N) non contiene coppie complementari (A, ~A).

ALBERI SEMANTICISia BS = {A1, A2,…,An,…} la Base di Herbrand della teoria S

un corrispondente albero semantico binario:

se l’Universo e la Base di Herbrand sono infiniti (se esiste almeno un

simbolo di funzione), l’albero semantico è un albero binario infinito

A1 ~A1

A2~A2 A2 ~A2

ALBERI SEMANTICI• Ogni cammino sull’albero semantico è

una H-interpretazione:l’insieme degli atomi positivi del cammino

• Ad ogni nodo N è associata la H-interpretazione (parziale) I(N).

• Un albero semantico è completo se per ogni foglia N, I(N) contiene A o ~A per ogni A in BS.

NODI DI FALLIMENTO

• un nodo n dell’albero semantico è un nodo di fallimento per l’insieme di clausole S,se esiste almeno una clausola c di S tale che– c’ (un’istanza ground di c) è falsa

nell’H-interpretazione In

– tutte le clausole di S (tutte le loro istanze ground) non sono false in tutte le H-

interpretazioni Im con m antenato di n, cioè

nessun nodo m antenato di n è un nodo di

fallimento.

ALBERI SEMANTICI CHIUSI

• un albero semantico è chiuso, se ogni suo cammino contiene un nodo di fallimento.

• può essere rappresentato da un albero binario finito, le cui foglie sono i nodi di fallimento.

• un nodo n dell’albero semantico è un nodo inferenza per l’insieme di clausole S, se tutti i suoi immediati successori sono nodi fallimento.

TEOREMA DI HERBRAND (versione 1) Un insieme di clausole S è insoddisfacibile

iff per ogni albero semantico completo c'è un corrispondente albero semantico finito e chiuso.

Prova• si assuma S insoddisfacibile, sia T il suo albero

semantico,sia r un cammino di T– poiché S è insoddisfacibile, Ir deve rendere falsa

un’istanza ground c' di una clausola c in S – essendo c' una disgiunzione finita di atomi ground, deve

esistere un nodo di fallimento ad una distanza finita dalla radice di T

– essendo questo vero per ogni ramo, T è chiuso

• si assuma T chiuso– ogni cammino contiene un nodo di fallimento– ogni H-interpretazione rende falso S– S è insoddisfacibile

TEOREMA DI HERBRAND: UN ESEMPIO

• la teoria del prim’ordinep(a,a)(X)(Y) p(X,Y) p(f(X),f(Y))

• la formula “da provare” (X) p(f(a),X)

• la sua negazione (X)~p(f(a),X)

• l’insieme di clausolec1: p(a,a)c2: ~p(X,Y)p(f(X),f(Y))c3: ~p(f(a),X)

• l’Universo di Herbrand: {a,f(a),f(f(a)),…}

• la Base di Herbrand: {p(a,a), p(f(a),a), p(f(a),f(a)), p(a,f(a)),…}

c1: p(a,a)c2: ~p(X,Y)p(f(X),f(Y))c3: ~p(f(a),X)

l’albero semantico è chiuso (i nodi di fallimento sono etichettati con la clausola che “fallisce” in

quel nodo)P(a,a) ~P(a,a)

P(f(a),a)~P(f(a),a)

~P(f(a),f(a))P(f(a),f(a))

• la costruzione dell’albero semantico e la determinazione dei nodi di fallimento costituisce una procedura che permette di semidecidere se una formula è conseguenza logica di un insieme di assiomi

• il metodo è semantico

• alla ricerca di procedure (“sintattiche”?) più efficienti

TEOREMA DI HERBRAND (versione 2) Un insieme di clausole S è

insoddisfacibile se e solo se esiste uninsieme finito insoddisfacibile S' di istanze ground di clausole di S

Sulla versione 2 del teorema sono basati i primi metodi per la verifica automatica di insoddisfacibilità:(Gilmore[1960], Davis&Putnam [1960],

Metodi di verificaa)algoritmo per generare sistematicamente le istanze

grounddelle clausole (la procedura di Herbrand):al passo i-esimo si istanziano le clausole sostituendo le variabili con termini di HUk tale che k ≤ i

b) algoritmo per verificarne l’insoddisfacibilità:

un qualunque algoritmo per il calcolo proposizionale

• non fattibile, perché il numero di clausole generate cresce in modo esponenziale

• il principio di risoluzione di Robinson [1965]– un metodo sintattico, basato sulla versione 1 del T. di

Herbrand– evita la generazione di insiemi di istanze ground

DAVIS E PUTMANRegola della tautologia

Cancellare le clausole che sono tautologie

Regola del singolo letterale– S={{L},{...,L,...},{...,~L,...},...}

– S'={ {...,~L,...},...}

– se S'={} S è soddisfacibile, altrimenti prosegui con

– S"={ {..., ,...},...}

Regola del letterale puroSe un letterale L non compare mai come ~L è puro, si può

ottenere un

nuovo insieme di clausole eliminando tutte quelle che contengono L

Regola di divisione– S={{A1,L},...,{An,L},{B1,~L},...,{Bm,~L}, R}

– S1={{A1},...,{An},R}

– S2={{B1},...,{Bm}, R}• S è insoddisfacibile iff lo è S1S2

IL METODO DI RISOLUZIONE: SCHEMA • un insieme di clausole S è insoddisfacibile se

– contiene la clausola vuota [] (contraddizione!)oppure

– da S si può derivare la clausola vuota []

• il principio di risoluzione è una regola di inferenza

sia S' l’insieme ottenuto aggiungendo all’insieme di clausole S le clausole derivabili da S con il principio di risoluzione

se S è insoddisfacibile, anche S' è insoddisfacibile

l’albero semantico (chiuso) di S' è strettamente “più piccolo” di

quello di S

iterando l’applicazione del principio di risoluzione si ottiene un insieme di

clausole S* il cui albero semantico è costituito dalla sola radice

la radice è un nodo di fallimentoS* contiene []

IL PRINCIPIO DI RISOLUZIONE NEL CALCOLO PROPOSIZIONALE

• estensione della regola del letterale unico di Davis&Putnam

• siano c1 e c2 due clausole qualunquec1 = a1

1 a21 … an

c2 = a12 a2

2 … am2

tali che i letterali ai1 e aj

2 sono complementari

il risolvente di c1 e c2 è la clausola

a11 … ai-1

1 ai+11 … an

1a12… aj-1

2 aj+12 … an

disgiunzione delle clausole ottenute eliminando i letterali complementari

• esempi c1 = p r c2 = ~p q

c1,2 =r qc1 = ~p q r c2 = ~q s

c1,2 = ~p r sc1 = ~p q c2 = ~p r

c1,2 non esiste

• il risolvente, se esiste, di due clausole unitarie è la clausola vuota []

CORRETTEZZA DEL PRINCIPIO DI RISOLUZIONE

NEL CALCOLO PROPOSIZIONALE Teorema

Date due clausole c1 e c2, un risolvente c di c1 e c2 è conseguenza logica di c1 e c2

Provasiano c1 = a c1', c2 = ~a c2' e c = c1' c2',

con c1' e c2' disgiunzioni di letteralisia I un modello di c1 e c2

in I è falso a oppure ~a supponiamo sia falso ac1' non può essere vuoto e deve essere vero in I (altrimenti I non sarebbe un modello di c1)è vero in I anche c = c1' c2' analogamente, se ~a è falso, c1' (e quindi c) vero in I quindi, in ogni caso, c è vero in I

• come vedremo nel contesto dei linguaggi del prim’ordine, il principio di

risoluzione è una regola di inferenza completa per la dimostrazione dell’insoddisfacibilità di un insieme di clausole

• un insieme di clausole S è insoddisfacibile se e solo se la clausola vuota [] può essere ricavata da S, applicando il principio di risoluzione

PRINCIPIO DI RISOLUZIONE NEI

LINGUAGGI DEL PRIM’ORDINE c1 = p(X) q(X) c2 = ~p(f(Y)) r(Y)

• servono letterali complementari, che esistono se consideriamo opportune istanze di c1 e c2 – c1' = p(f(a)) q(f(a)) c2' = ~p(f(a)) r(a)

c1,2' = q(f(a)) r(a)– c1" = p(f(Y)) q(f(Y)) c2" = ~p(f(Y)) r(Y)

c1,2" = q(f(Y)) r(Y)

• c1,2" è più generale di c1,2', ed è anzi la più generale fra le clausole ottenibili da c1 e c2 mediante il procedimento

istanziazione + risoluzione proposizionaleogni altra clausola è una istanza di c1,2"c1,2" è il risolvente di c1 e c2

• deduzione di c da S: c1,...,cn tale che ogni ci è una clausola di S o un risolvente di clausole precedenti e cn = c

• refutazione: deduzione di [] da S

SOSTITUZIONI• una sostituzione è un insieme finito della forma

{v1 t1,…, vn tn}vi è una variabileti è un termine diverso da vi le variabili vi, i=1,…,n sono tra loro distinte

• una sostituzione è una funzione da variabili a terminila sostituzione vuota è denotata da una sostituzione è ground se tutti i ti, i=1,…,n sono ground

• siano = {v1 t1,…, vn tn} una sostituzione ed E una espressione (termine, atomo, insieme di termini, etc.)

• l’applicazione di ad E è l’espressione ottenuta da E sostituendo simultaneamente ogni occorrenza di vi, i=1,…,n con il termine ti

• il risultato dell’applicazione (denotato da E) è una istanza di E

• la sostituzione è grounding per l'espressione E se E è una istanza ground di E

SOSTITUZIONI • siano = {X1 t1,…, Xn tn} e = {Y1 u1,…, Ym um}

due sostituzioni

• la composizione di e (denotata da ) è la sostituzione così definitai) costruiamo l’insieme

{X1 t1,…, Xn tn, Y1 u1,…, Ym um}

ii) eliminiamo dall’insieme gli elementi Xi titali che ti = Xi

iii) eliminiamo dall’insieme gli elementi Yj uj tali che

Yj occorre in {X1,…, Xn}

• Alcune delle proprietà delle sostituzioni:

– la composizione di sostituzioni è associativa() = ( )

– la sostituzione vuota è identità sia sinistra che destra = =

SOSTITUZIONI: ESEMPIO = {X f(Y), Y Z} = {X a, Y b, Z Y}

Costruzione di

i) {X f(b), Y Y, X a, Y b, Z Y}

ii) {X f(b), X a, Y b, Z Y}

iii) {X f(b), Z Y}

Costruzione di

i) {X a, Y b, Z Z, X f(Y), Y Z}

ii) {X a, Y b, X f(Y), Y Z}

iii) {X a, Y b}

UNIFICAZIONE DI INSIEMI DI ESPRESSIONI

• sia dato un insieme di espressioni (termini, atomi, etc.) {E1,…, Ek}

• una sostituzione è un unificatore per {E1,…, Ek} iff E1= E2 = …= Ek

• un insieme {E1,…, Ek} è unificabile iff esiste una sostituzione tale che è un unificatore per {E1,…, Ek}

• l’insieme {p(a,Y), p(X,f(b))} è unificabile dato che la sostituzione = {X a, Y f(b)} è un unificatore per l’insieme

• un unificatore per l’insieme {E1,…, Ek} è l’unificatore più generale (most general unifier, mgu)

iff per ogni unificatore dell’insieme {E1,…, Ek} esiste una sostituzione tale che =

• esiste un algoritmo (algoritmo di unificazione), che, dato un insieme di espressioni E = {E1,…, Ek}, – rivela la sua non unificabilità, oppure – calcola un unificatore più generale per E

MGU DI DUE ESPRESSIONI: UN ALGORITMO NAïF

• inizia con t1 , t2 ed una sostituzione µ0 inizialmente vuota

• scandisci le due espressioni da sinistra a destra

se le due espressioni sono uguali, termina con successo e restituisci

la corrente sostituzione µk (mgu di {t1 , t2})

altrimenti, siano t1,i and t2,i le prime due sottoespressioni diverse

se nè t1,i nè t2,i sono una variabile, termina con fallimento altrimenti, supponiamo che t1,i sia la variable V se t2,i contiene V, termina con fallimento altrimenti,

applica la sostituzione {V t2,i} a t1 e t2

µi = µi-1 {V t2,i}riprendi la scansione delle espressioni dove era stata sospesa

• da notare che le sostituzioni cicliche causano fallimento (l’occur check è necessario!)

MGU DI DUE ESPRESSIONI: UN ESEMPIO • E = {p(a,X,f(g(Y))), p(Z,f(Z),f(U))}

– µ0 = t1,1 = a t2,1 = Z

– µ1 = {Z a} = {Z a}

E1 = {p(a,X,f(g(Y))), p(a,f(a),f(U))}

t1,2 = X t2,2 = f(a)

– µ2 = {Z a} {X f(a)} = {Z a, X f(a)}

E2 = {p(a,f(a),f(g(Y))), p(a,f(a),f(U))}

t1,3 = g(Y) t2,3 = U

– µ3 = {Z a, X f(a)} {U g(Y)} = {Z a, X f(a), U g(Y)} E3 = {p(a,f(a),f(g(Y)))}

– µ3 è un mgu per E

Teorema di Unificazione

Teorema

Se W è un insieme di espressioni finito, non vuoto ma unificabile, allora

l'algoritmo di unificazione terminerà sempre al passo del successo e l'ultima sostituzione finale è un m.g.u. per W; altrimenti termineràcon fallimento.

LINGUAGGI DEL PRIM’ORDINE • Se la clausola c = L1 … Ln contiene un insieme di letterali

unificabile, con unificatore più generale , la clausola

[L1 … Ln]viene detta fattore unitario di c

• c = p(X) p(f(Y)) q(X)i primi due letterali sono unificabili con mgu {X f(Y)}p(f(Y)) q(f(Y)) è un fattore unitario di c

• date due clausole senza variabili a comune (eventualmente ottenute per ridenominazione delle variabili)

c1 = L1Ln c2 = L'1 L'k

se esistono Li ed L'j (unificabili) con unificatore più generale tale che

[Li]= [~L'j] la clausola (risolvente binario di c1 e c2)

[L1Li-1Li+1LnL'1L'j-1L'j+1L'k]è conseguenza logica di c1 e c2

LINGUAGGI DEL PRIM’ORDINE • Li e L'j vengono detti i letterali su cui si è risolto

• un risolvente di c1 e c2 è un risolvente binario

di [un fattore unitario di] c1 e di

[un fattore unitario di] c2

• Es: da ab e bc deriva ac da ab e b,dc deriva a,dc da b,d e bc deriva c,d

• Es: c1= ~p(s(0),s(0),W) ~p(W,s(0),W1)

c2= ~p(X,Y,Z) p(s(X),Y,s(Z))

= {X 0, Y s(0), W s(Z) }

c1,2 = ~p(s(Z),s(0),W1) ~p(0,s(0),Z)

IL METODO DI RISOLUZIONE • un insieme di clausole S è insoddisfacibile se

contiene la clausola vuota [] oppureda S si può derivare la clausola vuota []

• sia S' l’insieme ottenuto aggiungendo all’insieme di clausole S tutti i fattori unitari di clausole di S ed i risolventi binari di coppie di clausole in S

se S è insoddisfacibile, anche S' è insoddisfacibile

• l’albero semantico (chiuso) di S' è strettamente “più piccolo” di quello di S

• iterando l’applicazione del principio di risoluzione (generazione di fattori e risolventi) si ottiene un insieme di clausole S* il cui albero semantico è costituito dalla solaradice, la radice è un nodo di fallimento, S* contiene []

IL PRINCIPIO DI RISOLUZIONE É UNA

REGOLA DI INFERENZA CORRETTA • teorema:

se c è una clausola e c' un suo fattore unitario, c' è conseguenza logica di c

• dimostriamo che ogni istanza è conseguenza logica

supponiamo che c' sia falsa in una interpretazione M che è un modello di c

un’istanza ground di c' deve essere falsa in M

un’istanza ground di c è falsa in MM non può essere un modello di c

IL PRINCIPIO DI RISOLUZIONE É UNA

REGOLA DI INFERENZA CORRETTA • teorema:

se c1 e c2 sono clausole e c è

un loro risolvente binario, c è conseguenza logica di c1 e c2

il risolvente può essere calcolato componendo due regole (l’istanziazione e la risoluzione proposizionale) che sono state dimostrate essere regole di inferenza corrette

TEOREMA DI CORRETTEZZA DEL METODO DI RISOLUZIONE

Se dall’insieme di clausole S è possibile derivare con il principio di risoluzione la clausola vuota [] , l’insieme S è

insoddisfacibile

dimostrazione• [] è uno dei risolventi generati a partire

dalle clausole di S • [] è conseguenza logica di S• tutti i modelli di S sono anche modelli di []• [] (la contraddizione) non ha alcun modello• anche S non ha alcun modello

LEMMA DI GENERALIZZAZIONE Siano c'1 e c'2 istanze di c1 e c2 sia c' un risolvente di c'1 e c'2 esiste

un risolvente c di c1 e c2 tale che c' è una istanza di c

dimostrazione• c1 = A1

1 V…V A1n e c2 = A2

1 V…V A2m non hanno variabili comuni

(eventualmente si ridenomina)• c' = [ A1

1 V…V A1i-1 V A1

i+1 V…V A1n V

A21 V…V A2

j-1 V A2j+1V…V A2

m] =[ A1

1 V…V A1i-1 V A1

i+1 V…V A1n V

A21 V…V A2

j-1 V A2j+1 V…V A2

m] ,dove c'1 = c1, c'2 = c2 ,

è l’mgu di A1i e ~A2

j, cioè [A1i] = ~[A2

j] • A1

i e ~A2j sono unificabili, in quanto è un loro unificatore

• esiste un loro unificatore più generale tale che per una opportuna sostituzione

• esiste un risolvente di c1 e c2 rispetto ai letterali A1i e A2

c = [ A11 V…V A1

i-1 V A1i+1 V…V A1

n V A2

1 V…V A2j-1 V A2

j+1 V…V A2m]

• c' = [ A11 V…V A1

i-1 V A1i+1 V…V A1

n V A2

1 V…V A2j-1 V A2

j+1 V…V A2m] = c

NODI DI INFERENZA • consideriamo l’albero semantico chiuso di

un insieme di clausole S insoddisfacibile,un nodo di inferenza è un nodo dell’albero semantico, tale che entrambe i suoi successori sono nodi di fallimento

• se le clausole che falliscono nei successori del nodo di inferenza n sono ck e cj,

possiamo inferire da ck e cj una nuova

clausola rkj (che è proprio un risolvente) tale che:

rkj fallisce nel nodo n o in un nodo

antenato di n

NODI DI INFERENZA: ESEMPIO • C1: P(a,a)• C2: ~P(X,Y) P(f(X),f(Y))• C3: ~P(f(a),X)

P(a,a) ~P(a,a)

P(f(a),a)~P(f(a),a)

~P(f(a),f(a))P(f(a),f(a))

NODI DI INFERENZA: ESEMPIO • le clausole che falliscono sotto il nodo

d’inferenza sono C2 e C3

• il risolvente di C2 e C3 è C4 = ~P(a,Y)

fallisce sopra il nodo di inferenza

• il nuovo albero semantico è infatti

P(a,a) ~P(a,a)

IL LEMMA SUI NODI DI INFERENZA Dalle clausole che falliscono nei successori di un nodo di inferenza n possiamo inferire una nuova clausola (che è proprio un risolvente) che fallisce in un nodo n’ sopra n.

Dimostrazione

• sia n un nodo di inferenza, siano n1 e n2 i nodi di fallimento suoi immediati successori, e sia mn+1 l’atomo assegnato a vero o a falso sotto il nodo n

• poiché n1 e n2 sono nodi di fallimento, mentre n non lo è, devono esistere due istanze ground c'1 e c'2 delle clausole c1 e c2 tali che c'1 e c'2 sono false in n1 e n2 rispettivamente e non sono falsificate da n

• c'1 e c'2 devono contenere ~mn+1 e mn+1 rispettivamente • il risolvente rispetto a questi due letterali

c' = (c'1 - ~mn+1 ) (c'2 - mn+1 ) fallisce in un nodo n’ sopra n poiché sia (c'1 - ~mn+1 ) che (c'2 - mn+1 ) sono falsificati da n (l’unico letterale che non falliva è stato tolto!)

• per il lemma di generalizzazione, esiste un risolvente c di c1 e c2, tale che c' è una istanza ground di c (anche c fallisce in n’)

TEOREMA DI COMPLETEZZA DEL

METODO DI RISOLUZIONE Se l’insieme di clausole S è insoddisfacibile, è possibile derivare da S in un numero finito di passi con il principio di risoluzione la clausola vuota []

Dimostrazione

• S è insoddisfacibile, quindi ha un albero semantico chiuso finito T• se T è formato da un solo nodo (la radice), S deve contenere [], perché

nessuna altra clausola può essere falsificata dalla radice • altrimenti, T ha almeno un nodo di inferenza (in caso contrario ogni

nodo avrebbe almeno un successore non di fallimento e si potrebbe trovare un cammino di T infinito, contro l’ipotesi di finitezza)

• per il lemma dei nodi di inferenza, esiste un risolvente c di clausole in S, che fallisce almeno in n

• sia T' l’albero semantico (chiuso) di S {c} il numero di nodi di T' è strettamente minore di quello di T

• il procedimento può essere iterato, finché, dopo un numero finito di passi (l’albero iniziale è finito!) si raggiunge la clausola vuota [] e si ottiene un albero semantico chiuso formato dalla sola radice

UN ESEMPIO la teoria

1. p(0,X,X)2. ~p(X,Y,Z) V p(s(X),Y,s(Z))

la formula da provareW. p(s(0),0,W)

la sua negazione (clausola)3. ~p(s(0),0,W)

la prova (mostrata sotto forma di albero di rifiuto)

UN ESEMPIO • le premesse (assiomi)

– i funzionari di dogana hanno perquisito tutti coloro che sono entrati in Italia,

ad eccezione dei VIP– alcuni spacciatori di droga sono entrati in Italia e sono stati perquisiti

solo da spacciatori di droga

– nessuno spacciatore era un VIP• la conclusione

– alcuni funzionari erano spacciatori

• e(X) rappresenta “X è entrato in Italia”; v(X) rappresenta “X era un VIP”; p(X,Y) rappresenta “Y ha perquisito X”; f(X) rappresenta “X era un funzionario di dogana”;s(X) rappresenta “X era uno spacciatore di droga”

• (X)(e(X) ~v(X)) (Y)(p(X,Y) f(Y))~ e(X) V v(X) V p(X,g(X)) ~ e(X) V v(X) V f(g(X))

(X)s(X) e(X) (Y)(p(X,Y) s(Y))s(a) e(a) ~ p(a,Y) V s(Y)

(X)(s(X) ~ v(X))~ s(X) V ~ v(X)

• (X)s(X) f(X) la cui negazione è~ s(X) V ~ f(X)

UN ESEMPIO (1) ~ e(X) V v(X) V p(X,g(X))(2) ~ e(X) V v(X) V f(g(X))(3) s(a)(4) e(a)(5) ~ p(a,Y) V s(Y) (6) ~ s(X) V ~ v(X)(7) ~ s(X) V ~ f(X)

la dimostrazione per risoluzione

(8) ~ v(a) da (3) e (6)(9) v(a) V f(g(a)) da (2) e (4)(10) f(g(a)) da (8) e (9)(11) v(a) V p(a,g(a)) da (1) e (4)(12) p(a,g(a)) da (8) e (11)(13) s(g(a)) da (5) e (12)(14) ~ f(g(a)) da (7) e (13)(15) [] da (10) e (14)

notare che si sono usate tutte le clausole e che si sono generatisolo alcuni dei risolventi

IL METODO DI RISOLUZIONE • il metodo di risoluzione è un potente metodo di dimostrazione

sintattico (basato su una sola regola di inferenza)

– non piace a coloro cui piacciono le prove• sono poco naturali e poco convincenti• inoltre richiede la skolemizzazione, che “fa perdere informazione”

– è molto più efficiente degli altri metodi basati sul teorema di Herbrand• l’astuzia principale sta nell’unificazione

– in molti casi produce comunque una tale esplosione nel numero di risolventi generati da risultare inutilizzabile

• anche perché vengono generate molte clausole irrilevanti e ridondanti

– da qui l’interesse per particolari strategie di applicazione del principio di risoluzione, che

• generino meno clausole• garantiscano la completezza

• risoluzione a livelli di saturazione(S0= S, S1= {risolventi a partire da S0}, ...)

• strategie di cancellazione (tautologie, clausole sussunte: C sussume D sse D C)

STRATEGIE DI RISOLUZIONE

Risoluzione semantica (1)

• interpretazione particolare per dividere le clausole in 2 insiemi

• ordinamento dei simboli di predicato per determinare una scelta sulla applicazione della risoluzione

Hyperisoluzione (positiva o negativa) (1a)

• interpretazione particolare tutta positiva o negativa

STRATEGIE DI RISOLUZIONE

Set of support strategy(1b)

• individuare ST tale che S-T è soddisfacibile e non scegliere mai di risolvere clausole in S-T.

Lock resolution(2)

• ogni letterale è indicizzato e si applica la risoluzione solo ai letterali con indice minore di ogni clausola (non si può mescolare con altre strategie).

EsempioS= { ~q ~ p r, r p, r q, ~r}S’= { ~q r, ~p r, ~q ~ p , p, q}S’’= {~q, ~p, r}S’’’= {[]}----I= {~q, ~p, ~r}

S1 = {~q ~ p r, ~r} {~q r, ~ p r}

S2 = {r p, r q} {p, q} {r}

----p>q>r: ~q r r []

STRATEGIE DI RISOLUZIONE • un esempio di strategia completa

– la AF-resolution (ancestry-filtered resolution), che costruisce alberi di rifiuto con la proprietà AF

– un albero di rifiuto è ancestry-filtered se ogni suo nodo è

• una clausola della teoria iniziale, oppure

• un risolvente con almeno una clausola genitrice nella teoria iniziale,

oppure• un risolvente di due clausole ci e cj, con ci antenato di cj

• teoremaSe una teoria è insoddisfacibile, possiede almeno un albero di rifiuto ancestry-filtered

• E’ simile alla strategia lineare, su cui si basa la programmazione logica

RISOLUZIONE LINEARE

• un’altra strategia completa

• dall’insieme S viene prelevata una clausola c0 (clausola iniziale)

• un albero di rifiuto lineare ha la seguente proprietà:– per i=1,…,n-1 ci+1 è un risolvente di ci

(clausola centrale) e bi (clausola laterale)

– ogni bi appartiene a S oppure è un cj per j<i

RISOLUZIONE LINEARE• •

RISOLUZIONE LINEARE

• teorema di completezza

se S è insoddisfacibile e S- c0 è

soddisfacibile, esiste un albero

di rifiuto lineare con clausola iniziale c0

RISOLUZIONE INPUT E UNIT • input resolution

– è un caso particolare della risoluzione lineare, in cui tutte le clausole laterali sono clausole di S

– non sono permessi risolventi fra risolventi– non è completa, ma assomiglia molto alla

SLD-resolution utilizzata nella programmazione logica

• unit resolution

– il risolvente è ottenuto da almeno una clausola unitaria (come la input non completa)

• SL ed SLD resolution

UN ESEMPIO • La teoria

~q p q p ~p q• La formula da dimostrare

• Risoluzione lineare

• •

p q~p q

UN ESEMPIO• Input resolution

• •

p q~p q

• • •

Clausole Horn• clausola con al più un letterale positivo

– clausole definite:• Regole

AB1 B2 Bm.• Fatti

A.– clausole negative: (goal)

B1 B2 Bm.

• clausole Horn sono un sottinsieme vero delle clausole: non tutte le formule del

calcolo dei predicati del prim'ordine sono esprimibili con esse.

• clausole definite esprimono 'conoscenza'

programma logico = insieme di cl. definite

• clausole negative:

– domanda X1Xn.B1 B2 Bm)

– negazione per applicare la refutazione

~X1Xn.B1 B2 Bm)

X1Xn.B1 ~B2 ~Bm)B1 B2 Bm.

Risoluzione SLD• risoluzione Lineare con funzione di Selezione per clausole

Definite.

• si parte da un insieme di clausole definite (il programma P) ed

un'unica clausola negativa (il goal G)

• ogni risolvente è sempre ottenuto da una clausola definita ed una

negativa, riottenendo così un'altra clausola negativa (il nuovo goal)

• si deve selezionare a quale letterale del goal applicare la risoluzione

(regola di sel. R).

• una derivazione SLD è una sequenza massimale (finita o no)

di goal (G0G1 di clausole di P (c0 c1) e di sostituzioni (0 1):

– G0 è il goal iniziale G

– ci non ha variabili a comune con G,ci,...,ci-1

– Gi+1 è ottenuto da Gi = A1 A2 Am e ci = AB1 B2 Bn

[Aj]i= [A]i

Gi+1 = [A1Aj-1B1 B2 BnAj+1 Am]i

Esempio di derivazione SLD

• una refutazione è una sequenza di goal che termina con il goal vuoto.

• una derivazione finita che non termina con la clausola vuota è detta fallita.

• •

C 22G1

Appunti del corso: Intelligenza Artificiale II Dimostrazione automatica di Teoremi Prof. Maurizio...

Documents