Appunti del corso: Intelligenza Artificiale II Dimostrazione automatica di Teoremi Prof. Maurizio Martelli DISI 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 - implicazione F1← F2 - disgiunzione F1∨F2 - equivalenza F1↔ F2 - frasi quantificate: se Fè una fbf e X ∈ V - universalmente (∀X.F) - non esistono altre fbf - esistenzialmente (∃X.F) 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 predicati SEMANTICA (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 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 è 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 (∀X) (∃Y) p(X) Λ q(X,Y) f = 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 dim. di semantica --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 S iff 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 Normali H=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 = GH 4. (HP)G = H(PG) (HP)G = H(PG) 5. (HP)G = (HG)(PG) (HP)G = (HG)(PG) 6. Hf = H Ht = H 7. Ht = t Hf = f 8. H~H = t H~H = f 9. ~(~H) = H 10. ~(HP) = ~H~P 11. ~(HP) = ~H~P 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)(Q2x2(Qnxn) (M) – (Qixi) è xi o xi. – M è una formula senza quantificatori – (Q1x1)(Q2x2(Qnxn) è 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[x]G[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 Skolem Sia F = (Q1x1)(Q2x2(Qnxn) (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 An~B1~ B2 ~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 Lemma sia 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' Skolemizzazione Teorema 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,…,m Sm= C Per il lemma precedente, Sk è inconsistente iff Sk-1 è inconsistente, quindi C è inconsistente iff S è inconsistente Skolemizzazione Sia C l’insieme di clausole risultante dalla skolemizzazione dell’insieme di fbf S se S è consistente, C non è necessariamente equivalente a S Esempio • 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 L f è 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 HERBRAND Universo 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 stessa iii) ad ogni funzione n-aria f di L è assegnata la n funzione da (UL) 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 modello D = {0,1} a=0 p(0) = t p(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-INTERPRETAZIONI E 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ò essere rappresentato da un albero (l’albero semantico), i cui archi sono etichettati da assegnamenti di valori 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 SEMANTICI Sia BS = {A1, A2,…,An,…} la Base di Herbrand della teoria S un corrispondente albero semantico binario: A1 A2 ~A1 ~A2 A2 ~A2 se l’Universo e la Base di Herbrand sono infiniti (se esiste almeno un simbolo di funzione), l’albero semantico è un albero binario infinito 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’ordine p(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 clausole c1: 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) C1 ~P(f(a),a) P(f(a),a) C3 P(f(a),f(a)) C3 ~P(f(a),f(a)) 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 un insieme 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 verifica a) algoritmo per generare sistematicamente le istanze ground delle 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 PUTMAN Regola della tautologia Cancellare le clausole che sono tautologie Regola del singolo letterale – S={{L},{...,L,...},{...,~L,...},...} – S'={ – se S'={} S è soddisfacibile, altrimenti prosegui con – S"={ {...,~L,...},...} {..., ,...},...} Regola del letterale puro Se 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 fallimento S* contiene [] IL PRINCIPIO DI RISOLUZIONE NEL CALCOLO PROPOSIZIONALE • estensione della regola del letterale unico di Davis&Putnam • siano c1 e c2 due clausole qualunque c1 = a11 a21 … an1 c2 = a12 a22 … am2 tali che i letterali ai1 e aj2 sono complementari il risolvente di c1 e c2 è la clausola a11 … ai-11 ai+11 … an1a12… aj-12 aj+12 … an2 disgiunzione delle clausole ottenute eliminando i letterali complementari • esempi • il risolvente, se esiste, di due clausole unitarie è la clausola vuota [] c1 = p r c2 = ~p q c1,2 =r q c1 = ~p q r c2 = ~q s c1,2 = ~p r s c1 = ~p q c2 = ~p r c1,2 non esiste 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 Prova siano c1 = a c1', c2 = ~a c2' e c = c1' c2', con c1' e c2' disgiunzioni di letterali sia I un modello di c1 e c2 in I è falso a oppure ~a supponiamo sia falso a c1' 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 proposizionale ogni 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 Jè un insieme finito della forma {v1 t1,…, vn tn} vi è una variabile ti è un termine diverso da vi le variabili vi, i=1,…,n sono tra loro distinte • una sostituzione è una funzione da variabili a termini la sostituzione vuota è denotata da e una sostituzione è ground se tutti i ti, i=1,…,n sono ground • siano J= {v1 t1,…, vn tn} una sostituzione ed E una espressione (termine, atomo, insieme di termini, etc.) • l’applicazione di J 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 EJ) è una istanza di E • la sostituzione J è grounding per l'espressione E se EJ è una istanza ground di E SOSTITUZIONI • siano J = {X1 t1,…, Xn tn} e l= {Y1 u1,…, Ym um} due sostituzioni • la composizione di Je l(denotata da J l) è la sostituzione così definita i) costruiamo l’insieme {X1 t1l,…, Xn tnl, Y1 u1,…, Ym um} ii) eliminiamo dall’insieme gli elementi Xi tiltali che til = 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 (J l) m = J (l m) SOSTITUZIONI: ESEMPIO J = {X f(Y), Y Z} l= {X a, Y b, Z Y} Costruzione di J l 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 l J 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.) {E ,…, E } 1 k • una sostituzione J è un unificatore per {E1,…, Ek} iff E1J= E2J = …= EkJ • un insieme {E1,…, Ek} è unificabile iff esiste una sostituzione J tale che J è un unificatore per {E1,…, Ek} • l’insieme {p(a,Y), p(X,f(b))} è unificabile dato che la sostituzione J= {X a, Y f(b)} è un unificatore per l’insieme • un unificatore J per l’insieme {E1,…, Ek} è l’unificatore più generale (most general unifier, mgu) iff per ogni unificatore l dell’insieme {E1,…, Ek} esiste una sostituzione m tale che l = J m • 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 = e t1,1 = a t2,1 = Z – µ1 = e {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 s, la clausola [L1 … Ln]sviene detta fattore unitario di c • c = p(X) p(f(Y)) q(X) i primi due letterali sono unificabili con mgu p(f(Y)) q(f(Y)) è un fattore unitario di c {X f(Y)} • 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 q tale che [Li]q= [~L'j]q la clausola (risolvente binario di c1 e c2) [L1Li-1Li+1LnL'1L'j-1L'j+1L'k]q è 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)) s = {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 [] oppure da 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 sola radice, 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 M M 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 = A11 V…V A1n e c2 = A21 V…V A2m non hanno variabili comuni (eventualmente si ridenomina) • c' = [ A11t V…V A1i-1t V A1i+1t V…V A1nt V A21t V…V A2j-1t V A2j+1t V…V A2mt]g = [ A11 V…V A1i-1 V A1i+1 V…V A1n V A21 V…V A2j-1 V A2j+1 V…V A2m] t g, dove c'1 = c1t, c'2 = c2 t, g è l’mgu di A1it e ~A2jt, cioè [A1it]g = ~[A2jt]g • A1i e ~A2j sono unificabili, in quanto t gè un loro unificatore • esiste un loro unificatore più generale s tale che t g=s m per una opportuna sostituzione m • esiste un risolvente di c1 e c2 rispetto ai letterali A1i e A2j c = [ A11 V…V A1i-1 V A1i+1 V…V A1n V A21 V…V A2j-1 V A2j+1 V…V A2m]s • c' = [ A11 V…V A1i-1 V A1i+1 V…V A1n V A21 V…V A2j-1 V A2j+1 V…V A2m] s m= cm 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: C2: C3: P(a,a) ~P(X,Y) P(f(X),f(Y)) ~P(f(a),X) P(a,a) ~P(a,a) C1 ~P(f(a),a) P(f(a),a) C3 P(f(a),f(a)) C3 ~P(f(a),f(a)) 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) C4 ~P(a,a) C1 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 provare W. 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)) ~ e(X) V v(X) V f(g(X)) s(a) e(a) ~ p(a,Y) V s(Y) ~ s(X) V ~ v(X) ~ s(X) V ~ f(X) (2) (3) (4) (5) (6) (7) la dimostrazione per risoluzione (8) (9) (10) (11) (12) (13) (14) (15) ~ v(a) da (3) e (6) v(a) V f(g(a)) da (2) e (4) f(g(a)) da (8) e (9) v(a) V p(a,g(a)) da (1) e (4) p(a,g(a)) da (8) e (11) s(g(a)) da (5) e (12) ~ f(g(a)) da (7) e (13) [] da (10) e (14) notare che si sono usate tutte le clausole e che si sono generati solo 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 sD Cs) 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). Esempio S= { ~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 • teorema Se 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 • 0 • B C1 • • B 0 1 C • 2. . . C n-1 • Cn• • B n-1 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 qp • La formula da dimostrare ~p ~q ~p q ~p q • q • p • • p q • p ~q • ~p ~q • Risoluzione lineare ~q • • • q UN ESEMPIO • Input resolution ~p q • q • • p q • p ~q p • • ~p ~q ~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 (q0 q1): – 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]qi = [A]qi Gi+1 = [A1Aj-1B1 B2 BnAj+1 Am]qi Esempio di derivazione SLD G • G1 • G • 2. . . G n-1 • • C q 1 1 • C q 2 2 • C n q n Gn • . . . • una refutazione è una sequenza di goal che termina con il goal vuoto. • una derivazione finita che non termina con la clausola vuota è detta fallita.