P 
Q 
R = {P,Q, R}
Il considerare la forma clausale è un passo obbligato nel cammino che dalla logica matematica conduce alla programmazione logica. Infatti, sia il formalismo che la regola di inferenza che viene qui applicata (il Principio di Risoluzione) sono molto più simili ai convenzionali linguaggi di programmazione che il formalismo e le regole di inferenza della forma standard della logica matematica.
Es: P
Q R = {P,Q, R}
Sulla base di queste convenzioni, una formula del Calcolo proposizionale o dei predicati può essere rappresentata semplicemente da un insieme di clausole.
Teorema
Sia S un insieme di clausole che rappresenta una forma standard di una formula FF è inconsistente
S è inconsistente
La conversione da forma standard a forma clausale si ottiene in nove passi:
[X
Y] XY X e Y formule
Per procedere all'eliminazione si può portare il simbolo
di implicazione verso l'interno:
[XY
Z] [XY] [XZ]
[XYZ] [XZ] [YZ]
[XYZ] [XYZ]
[XYZ] [XYZ]
[X[YZ]] [XYZ]
[[XY]Z] [XZ] [YZ] X, Y, Z formule
X
(YZ) (XY) (XZ)
Y)
vengono sostituite dall'insieme di formule {X,Y}.
Si ottiene un insieme finito di formule ciascuna delle
quali è una disgiunzione di letterali.
APer molte delle applicazioni della logica è sufficiente restringere la forma clausale alle clausole di Horn (dal nome del logico Alfred Horn che fu il primo a studiarle nel 1951).B1, ..., Bn
La maggior parte dei formalismi per la programmazione di calcolatori somiglia molto più alle clausole di Horn che alla forma clausale normale. Tuttavia la forma clausale normale costituisce una estensione significativa dei più semplici modelli di risoluzione di problemi più popolari espressi con clausole di Horn.
BC)
è logicamente equivalente alle seguenti implicazioni:
ciascuna delle quali apporta differenti informazioni sullo "stato del mondo" che descrive; la clausola come semplice disgiunzione di letterali non può indicare quale delle informazioni si debba intendere. È necessario dunque reintrodurre l'implicazione e rappresentare la conoscenza riguardo un problema facendo uso di due separate categorie: fatti e regole.(
I fatti sono asserzioni espresse come implicazioni e rappresentano la conoscenza specifica riguardo un caso particolare.
La clausola:
diventa:A
(la freccia d'implicazione è scritta nella direzione opposta rispetto alla forma standard solo per focalizzare l'attenzione sulla conclusione della clausola).
Le regole sono quelle asserzioni in cui compare l'implicazione. Esse esprimono la conoscenza generale riguardo un particolare soggetto.
dove:B1,B2,...,Bm
B1,B2,...,Bm,A1,A2,...,An sono formule atomiche con n
0, m0
A1,A2,...,An sono condizioni congiunte della clausola;
B1,B2,...,Bm sono conclusioni alternative della clausola.
Una clausola del tipo:
è chiamata fatto.A
Una clausola del tipo:
è chiamata regola.A
Una clausola del tipo:
è chiamata obiettivo.
Donna(x),Uomo(x) Umano(x).Donna(x) Madre(x,y).Madre(x,y) . Madre(x,y).
B1,...,Bn
si dice "vera" in una interpretazione I se e solo se:
Per dimostrare l'inconsistenza di un insieme di clausole è sufficiente dimostrare che l'insieme implica logicamente la clausola vuota. Un insieme vuoto di clausole è consistente: tutte le clausole che gli appartengono sono vere in ogni interpretazione dal momento che non contengono clausole che possono essere false.
Questa interpretazione inclusiva della disgiunzione contrasta con l'interpretazione esclusiva in cui "A o B" s'interpreta che o A o B è vero, ma non entrambe.
Il senso esclusivo della disgiunzione può essere espresso dalla disgiunzione inclusiva e dalla negazione. Esempio: esprimere che ogni umano è o femmina o maschio, ma non entrambi, richiede 2 clausole:
Femmina(x), Maschio(x)
Dato un insieme di clausole che esprime tutte le assunzioni concernenti un dominio, per determinare il valore di verità di ogni clausola è necessario determinare cosa sia logicamente implicato dalle assunzioni
Madre(Era,Ares) . (Era è madre di Ares)
Padre(Zeus,Ares) . (Zeus è padre di Ares)
Donna(x) Madre (x,y). (x è donna se è madre di y)
Uomo(x) Padre(x,y). (x è uomo se è padre di y)
si controlla se (a) è implicata dalle assunzioni C.(a) Madre(Zeus,Ares)
La clausola (a) è implicata logicamente da C, infatti: se Zeus è madre di Ares, allora, per la (3) di C, Zeus è una donna; ma nelle assunzioni non compare alcuna clausola che neghi l'affermazione che Zeus sia una donna, dunque (a) è logicamente implicata da C, (a) è vera in rapporto alle assunzioni C.
Se all'insieme C aggiungiamo la clausola (5):
Uomo(x),Donna(x).
Madre(Zeus,Ares) . (a)
Donna(Zeus). ottenuta dalla(a) e dalla C-(3)
Uomo(Zeus). ottenuta dalla (2) e dalla C-(5)
(Zeus non è un uomo)
Uomo(Zeus). ottenuta dalla C-(2) e dalla C-(4)
(Zeus è un uomo)
(5),
(a) è falsa in rapporto alle assunzioni
C(5).
Inoltre si può dimostrare che la nozione di implicazione logica può essere definita mediante la nozione di inconsistenza. e viceversa.
La semantica si può ridurre quindi alla nozione di inconsistenza. L'inconsistenza può essere dimostrata:
Il Principio di Risoluzione, introdotto da Robinson nel 1965, è una regola d'inferenza applicabile a tutti gli insiemi di clausole, semplice ed estremamente potente, facile da analizzare e da implementare. Il Principio di Risoluzione si usa per verificare l'insoddisfacibilità di un insieme S di clausole. L'idea è quella di controllare se S contiene la clausola vuota (che corrisponde ad una contraddizione); in questo caso risulta insoddisfacibile. Se S non contiene la clausola vuota, si controlla se questa può essere derivata da S.
La clausola così costruita è detta risolvente di C1 e C2.
Esempio:
C1: P(x), ¬R(a)
C2: S(y), R(a)
C, Risolvente di C1 e C2: P(x), S(y).
Una deduzione della clausola vuota („) ottenuta da S viene detta refutazione (o dimostrazione) di S.
La deduzione può essere rappresentata da un albero di deduzione.
Dato un insieme di clausole S, le clausole sono le foglie e se due clausole corrispondenti risolvono, si ha una risolvente detta discendente immediata delle due clausole.
La radice di un grafo di refutazione con risoluzione è la clausola vuota.
Qx,¬Qf(x),¬Pf(z)Rz,¬Rw}
l'albero di deduzione è:
Px
Quando in un'espressione non compaiono variabili, questa si dice vuota.
Una sostituzione si dice chiusa quando in t1,...,tn non compaiono variabili.
Una sostituzione si dice vuota quando non contiene elementi e si
denota con
.
in)
in E con il termine ti.
Eq viene detta istanza di E.
={x1/t1,...,xn/tn} e
={y1/u1,...,ym/um}
due sostituzioni.
Una composizione di
e
è la sostituzione
ottenuta dall'insieme
{x1/t1,...,xn/tn
,y1/u1,...,ym/um}
cancellando
per i quali xi=ti;
e
si denota con
°.
E1 =
E2 =
... =
Ek
L'insieme {E1,...Ek} viene detto unificabile se per esso esiste un unificatore.
=
y°
e
E1 g =
E2 =
... =
Ek
Esempio: la sostituzione {x/A} è l'unificatore più generale per le espressioni P(A,yz) e P(x,y,z).
Se Cg è una clausola unitaria, viene detto fattore unitario di C.
(C1g-L1g) >> (C2g-L2g)
viene detta risolvente binario di C1 e C2. I letterali L1 e L2 vengono detti letterali su cui si è risolto.
La Risoluzione applicata a due clausole unitarie produce la clausola vuota.C1 con L1C1 C2 con ¬L2
Date due clausole C1 e C2, se c'è un letterale L1 in C1 e un letterale ¬L2 in C2 tali che C1 e C2 hanno un "unificatore più generale" y, allora possiamo inferire la clausola ottenuta applicando la "sostituzione" all'unione di C1 e C2 meno i letterali complementari.
I casi (1) e (2) sono relativi alla risoluzione per il Calcolo Proposizionale.C1 con L1
Date due clausole C1 e C2, se c'è un letterale L1 in un fattore C1' di C1 e un letterale ¬L2 in un fattore C2' di C2 tali che L1 e L2 hanno un unificatore più generale g, allora diciamo che due clausole C1 e C2 si risolvono.
C1 con L1
Il principio può essere usato per dimostrare la conseguenza logica di una formula a partire da un dato insieme di formule (cioè per dimostrare un teorema inteso come formula derivabile da altre). Per dimostrare che un insieme S di formule implica logicamente la formula s si nega s e la si aggiunge ad S per ottenere l'insieme S'. Si converte S' in forma clausale e si applica la risoluzione. Se viene prodotta la clausola vuota, S' è inconsistente e, per il teorema suddetto, S implica logicamente s (si ha dunque una refutazione). La capacità di dimostrare il sussistere o meno della conseguenza logica apre il campo alle diverse applicazioni che si hanno del principio.(A1,...,An)
dove P è il predicato "essere padre" e G è il predicato "essere genitore". La nostra domanda (cioè il teorema da dimostrare) è: " Paolo è genitore di Mario ?", cioè G(Paolo,Mario).P(Paolo,Mario) P(Marco,Giulia) ¬P(x,y),G(x,y)
Neghiamo questa formula (¬G(Paolo,Mario)) e l'aggiungiamo all'insieme di formule date:
1- P(Paolo,Mario)
2- P(Marco,Giulia)
3- ¬P(x,y),G(x,y)
4- ¬G(Paolo,Mario)
5- G(Paolo,Mario) 1.3
6- G(Marco,Giulia) 2.3
7- ¬P(Paolo,Mario) 3.4
8- { } 4.5
9- { } 1.7
La domanda "chi è il genitore di Mario?", è rappresentata dalla formula P(x,Mario). La risposta sarà un letterale, cioè un termine della forma:
dove le variabili v1,...,vn sono le variabili libere nella domanda.Risposta(v1,...,vn)
Per rispondere alla domanda si forma una disgiunzione di questa e del letterale di risposta e si converte tutto in forma clausale:
{¬P(x,Mario),Risposta(x)}
Il principio di risoluzione ha molte altre applicazioni tra cui le principali sono: dimostrazioni dei teoremi della matematica; verifica correttezza dei programmi per calcolatori.1- P(Paolo,Mario) 2- P(Marco,Giulia) 3- P(x,y),G(x,y) 4- ¬P(z,Mario),Risposta(z) 5- G(Paolo,Mario) 1.3 6- G(Marco,Giulia) 2.3 7- ¬P(z,Mario),Risposta(w) 3.4 8- Risposta(Paolo) 4.5 9- Risposta(Paolo) 1.7
La risoluzione non ha meccanismi per sostituire termini costanti riconosciuti come equivalenti (1=1) e di conseguenza è impossibile dimostrare alcuni risultati anche se sono logicamente implicati dalle premesse.
È possibile ovviare a questa limitazione in 3 modi:
Esempio:
la definizione di fattoriale:
Fact(0)=1
Fact(k)=K*Fact(k-1)
si riscrive come:
Fact(0)=1
(k-1)=j Fact(j)=m k*m=n Fact(k)=n
e fornire appropriati assiomi di sostituzione.x x = x x y x = y
Nel caso dell'esempio di fattoriale:
k=j
Esistono strategie di cancellazione per eliminare le clausole ridondanti, ma l'eliminazione non può essere considerata un rimedio "economico". Infatti si è sprecato tempo (e nel caso di un calcolatore memoria e altre risorse) per generare le clausole inutili, riconoscerle come tali ed eliminarle.
È dunque necessario disporre di procedure per la dimostrazione di teoremi che impediscano la produzione di un numero ridondante di clausole. Sono stati studiati diversi affinamenti della risoluzione (risoluzione semantica, risoluzione con blocco, ... Chang-Lee); qui prenderemo in esame quelli che vengono usati dal PROLOG, il linguaggio logico che costituisce l'obiettivo di questo lavoro.
Dal principio di risoluzione generale alla strategia usata nel PROLOG i successivi affinamenti della risoluzione sono i seguenti:
"
e il simbolo d'implicazione
"".
La risoluzione
diretta si suddivide ulteriormente in due tipi di procedimento e uno
di questi è quello usato nel PROLOG.
Un risolvente lineare è quello in cui almeno una delle due clausole genitrici è o nell'insieme di clausole iniziale o è un predecessore dell'altra.
Le ridondanze che si ottengono da un uso "incontrollato" della risoluzione sono dovute al fatto che si risolvono clausole intermedie con altre clausole intermedie. Il vantaggio che offre la risoluzione lineare è quello d'impedire inutili inferenze focalizzando la deduzione su un predecessore della clausola su cui si sta operando o su un elemento dell'insieme di clausole iniziale.
C0 | / B0
| /
C1 |/ / B1
| /
C2 |/ /
| /
Cn-1 |/ / Bn-1
| /
Cn |/
Purtroppo non è completa per la refutazione, cioè non garantisce sempre la derivazione della clausola vuota da un insieme inconsistente di clausole; ma, restringendo l'attenzione alle clausole di Horn, la completezza si recupera.
La clausola rimane una disgiunzione di letterali; l'unica differenza è che l'ordine dei letterali non è irrilevante, ma viene chiaramente specificato.
P(x) Q(y) R(z)
R(z) è il letterale maggiore della clausola.
,
la clausola ordinata ottenuta dalla sequenza
C
eliminando tutti i
letterali identici ad un letterale minore nella sequenza viene detta
fattore ordinato di C.
;
e se C è la clausola
ordinata ottenuta concatenando le sequenze C1 e C2, eliminando L1 e L2 e
cancellando tutti i letterali identici ad un letterale minore dalla
sequenza ottenuta, allora C viene detto risolvente binario ordinato di
C1 su C2. I letterali L1 ed L2 vengono detti letterali su cui si
risolve.
C0 | / B0
| /
C1 |/ / B1
| /
C2 |/ /
| /
Cn-1 |/ / Bn-1
| /
Cn |/
Esempio:
(a) {¬L1,...,¬Ln,C} oppure
(b) {C,¬L1,...,¬Ln}
Come si è detto, la formula che rappresenta la domanda è una congiunzione di letterali, dunque non è più una clausola propriamente detta (Definizione: Una clausola è una disgiunzione di zero o più letterali).
Una clausola "in avanti" è una clausola in cui il letterale positivo
viene alla fine (L1, ..., L2
C).
La risoluzione "in avanti" si comporta nel seguente modo:
dati:
P(x)
M(A)
P(x)
M(A)
P(A) 1.2
{ } 3.4
L1,...,Ln).
La risoluzione "all'indietro" si comporta nel seguente modo:
dati:
P(z) e
P(x)
La clausola negativa P(z) è risolta con la prima clausola per produrre una conclusione intermedia negativa M(z).1- P(x)
Le principali tecniche di ricerca su albero sono due:
Graficamente una ricerca in ampiezza si può rappresentare come:
Profondità 0 Profondità 1 Profondità 2 Profondità 3
o o o o
| | |
| | |
o o o
/ \ / \
/ \ / \
o o o o
| |
| |
Graficamente una ricerca in profondità si può rappresentare come:
Ramo 1 Ramo 2 Ramo 3 Ramo 4
1| 1| 1| 1|
2/ 2/ / \ / \
3| 3| | |8 | |8
4/ / \6 / \ |9 / \ |9
5| | |7 | |/10 | |/ \11
Una procedura inferenziale si dice completa se e solo se ogni proposizione logicamente implicata da un insieme di formule (o clausole) può essere derivata usando quella procedura.
Per esempio la tautologia (cioè la formula sempre vera) {P,¬P} è logicamente implicata da ogni insieme di formule, ma la risoluzione non produce questa clausola da un insieme vuoto di clausole. Inoltre non è in grado di trattare proposizioni che contengano le relazioni di equivalenza; problema questo cui è possibile ovviare utilizzando opportune strategie.
Tuttavia, per insiemi di clausole senza proposizioni che contengano le relazioni di equivalenza e non equivalenza, la procedura è completa per la refutazione; cioè, dato un insieme di proposizioni insoddisfacibile, garantisce la produzione della clausola vuota.
Per l'indecidibilità del Calcolo dei Predicati sappiamo che è impossibile prendere in considerazione tutti i possibili domini. È possibile però fissare un dominio particolare H tale che S sia inconsistente se e solo se è falso sotto tutte le interpretazioni in questo dominio.
Questo dominio viene detto Universo di Herbrand di S.
Per i=0,1,2,..., sia Hi+1 l'unione di Hi e dell'insieme di tutti i termini della forma fn(t1,...,tn) per tutte le funzioni ad n-posti presenti in S dove tj=1,...,n sono elementi dell'insieme Hi.
Ogni Hi viene detto insieme delle costanti di livello di i, e
H
viene detto Universo di Herbrand.
Esempio:
Sia S = {P(a) P(x) Pf(x)}.
H0 = {a}
H1 = {a,f(a)}
H = {a,f(a),f(f(a)),......}.
Il significato di questo insieme è che se mj è Aj, ad Aj viene assegnato il valore "vero", altrimenti otterrà il valore "falso".
Esempio:
S={P(x)L'universo di Herbrand H di S è:L'insieme delle forme atomiche di S è:H={a,f(a),f(f(a)),...}.A={P(a),Q(a),R(a),Pf(a),Qf(a),Rf(a),......}.Alcune H-interpretazioni per S sono:
I1={P(a),Q(a),R(a),Pf(a),Qf(a),Rf(a),......} I2={¬P(a),¬Q(a),¬R(a),¬Pf(a),¬Qf(a),......} I3={¬P(a),Q(a),¬R(a),¬Pf(a),Qf(a),Rf(a),......}.
Dim...
Dim...
Dimostrazione......
Un albero semantico per S è un albero T rivolto verso il basso in cui ad ogni ramo è legato un insieme finito di atomi o di negazioni di atomi appartenenti ad A in modo tale che:
Dato l'insieme S={P(x)Q(x)R(x)},
l'insieme A delle forme atomiche di S è:
A={P(a),Q(a),R(a)}.
L'albero seguente è un albero semantico per S:
N
/ \
/ \
/ \
P(a)/ \¬P(a)
/ \
/ \
N1 N2
/ \ / \
/ \ / \
/ \ / \
Q(a)/ \¬Q(a) Q(a)/ \¬Q(a)
/ \ / \
N3 N4 N5 N6
/\ /\ /\ /\
/ \ / \ / \ / \
R(a)/ \¬R(a) / \ R(a)/ \¬R(a) / \
/ \ R(a)/ \¬R(a)/ \ R(a)/ \¬R(a)
N7 N8 N9 N10 N13 N12 N13 N14
L'albero semantico dell'esempio precedente è completo.
Un albero semantico completo per S è infinito se è infinito l'insieme A delle forme atomiche dell'insieme S di clausole.
Un albero semantico completo per S corrisponde ad un esame esaustivo di tutte le possibili interpretazioni di S.
Se S è inconsistente, allora risulta non vero in tutte le interpretazioni dell'albero semantico. Si può dunque evitare di espandere un nodo Ni se I(Ni) rende falso S.
Nell'esempio precedente l'interpretazione
I(N1-3-7) = {P(a),Q(a),R(a)}
Ma l'interpretazione
I(N2-6-13) = {¬P(a),¬Q(a),R(a)}
non rende vero l'insieme S.
Gli insiemi I(N1-3-7) e I(N2-6-13) sono modelli dell'insieme S.
Un modello non soddisfa una clausola se esiste un esempio base della clausola, ottenuto dai termini dell'universo di Herbrand, che ha valore "falso" nella interpretazione specificata nel modello.
I(N2-6-13) non soddisfa S.
Nell'esempio, N12 è un nodo di fallimento.
Un albero semantico di un insieme inconsistente di clausole è chiuso ed ha un numero finito di nodi sopra i nodi di fallimento.
Dimostrazione...
(Versione II: Un insieme S di clausole è inconsistente se e solo se esiste un insieme finito inconsistente S' di istanze chiuse di clausole di S.)
Dimostrazione........
Dimostrazione...........