Appunti del corso: Intelligenza Artificiale II Dimostrazione automatica di Teoremi Prof. Maurizio...
-
Upload
rinaldo-di-pietro -
Category
Documents
-
view
219 -
download
1
Transcript of Appunti del corso: Intelligenza Artificiale II Dimostrazione automatica di Teoremi Prof. Maurizio...
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
Calcolo dei predicati
• 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
Calcolo dei predicati
• 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
Calcolo dei predicati
• 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)
Calcolo dei predicati
• 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
B
• 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)
Calcolo dei predicati
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
Prova
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)),…}
TEOREMA DI HERBRAND: UN ESEMPIO
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))
C1
C3
C3 C2
TEOREMA DI HERBRAND: UN ESEMPIO
• 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
1
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
2
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.
PRINCIPIO DI RISOLUZIONE NEI
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
PRINCIPIO DI RISOLUZIONE NEI
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
j
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))
C1
C3
C3 C2
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)
C1C4
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• •
•
•
•
•
•
.
.
.
•
C B0
B1C1
C2
Bn-1
C
Cn-1
n
0
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
~p ~q
• Risoluzione lineare
•
•
•
•
• •
•
•
•
q
p
~q
~p ~q
p ~q
p q~p q
q
UN ESEMPIO• Input resolution
•
•
•
•
• •
•
•
•
q
p
~q
~p ~q
p ~q
p q~p q
~p ~q
~p
• • •
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.
• •
•
•
•
•
•
.
.
.
.
.
.
•
G
n
C1 1
C 22G1
G2
Cn
G
Gn-1
n