Schlußfolgern durch Theorembeweisen
Universität Bielefeld
fügt eine Frage-Formel in DATABASE ein und versucht, darauf passende Antworten zu deduzieren
query
INTERFACE
Idee: Eine Anfrage wird als zu beweisendes Theorem betrachtet.
8. Vorlesung: Unifikation; Vorwärts- und Rückwärtsverkettung, Goal Trees
Antwort
Anfrage
3 Logik und Inferenz
GATEKEEPER
(a) Direkter Beweis
– bei den Axiomen (d.h. hier: den assertierten Formeln) beginnen
– Schlußregeln anwenden, bis zu beweisendes Theorem dasteht
(b) Indirekter Beweis: durch Widerlegung des Gegenteils
– Nimm an, die Verneinung (das Negat) der Anfrage sei wahr
Methoden der Künstlichen Intelligenz
Ipke Wachsmuth
– Zeige, daß die Axiome und das Negat zusammen etwas als
wahr bezeichnen, das nicht stimmt
WS 2004/2005
– Folgere, daß das Negat nicht wahr sein kann, da ein
Widerspruch folgt
DATABASE
– Schließe, daß die Anfrage wahr sein muß, da ihr Negat nicht
wahr sein kann
8. Vorlesung
Einschub: Schlußfolgern in der Aussagenlogik
Ein Blick auf die deduktiven Schlußregeln der Aussagenlogik (AL)
Modus ponens
A→ B
A
B
¬
Modus tollens
AvB
A
B
A→ B
¬B
¬A
AvB
¬B
¬A
gegeben:
AvB
¬BvC
AvC
Methoden der Künstlichen Intelligenz
Es regnet ¬B
nicht
Schluß:
Ich trage die
Sonnenbrille
Beweis durch
Widerlegung
des Gegenteils
3
A
Ich trage die
Sonnenbrille
gegeben:
¬
Resolution ist eine allgemeinere
Schlußregel; sie beinhaltet zugleich
Modus ponens und Modus tollens.
2
Beispiel: Resolution in der Aussagenlogik
Gilt A v C ?
Resolutionsregel
8. Vorlesung
Klauseldarstellung
Methoden der Künstlichen Intelligenz
8. Vorlesung
AvB
ODER
A
¬
Es regnet
B
ODER
Ich nehme den
Schirm mit
ODER
Ich nehme den
Schirm mit
BvC
B
¬
¬
∅
A &¬C
C
C
Das Negat
der Anfrage
B
also gilt: A v C
Methoden der Künstlichen Intelligenz
4
Verallgemeinerter Modus Ponens
PL-Formeln mit Variablen: 2. Weg
(PL: Prädikatenlogik)
Statt (I) Modus Ponens betrachte folgende allgemeinere Regel:
• Unifikation: Sie ermöglicht Inferenzen mit Formeln der PL,
die gleiche Prädikate, aber verschiedene Argumente haben.
=> Verallgemeinerung (zunächst) des Modus ponens für PL
(Modus Ponens verallg.)
(III) Unifikations-Inferenz
Aus p' und (if p q ) inferiere q'
wobei p mit p' unifizieren muß
und die resultierende Substitution auf q angewandt wird,
wodurch man q' erhält.
(I) Modus Ponens erneut betrachtet:
Aus p und (if p q ) inferiere q
• Problem:
Was tun, wenn hier statt p eine Formel p' steht, welche
andere Argumente hat als in p ?
p
• Idee:
(if p q)
p'
p'
Methoden der Künstlichen Intelligenz
(if (inst ?x canary)(color ?x yellow))
(inst tweety canary)
(inst ?x canary)
(inst tweety canary)
unifizieren mit der Substitution: {x = tweety}
(inst x canary) und (inst tweety canary)
würden gleich bei der Substitution: {x = tweety}
8. Vorlesung
Beispiel
assert:
assert:
und durch Anwendung dieser Substitution auf (color ?x yellow)
ist (color tweety yellow) das Ergebnis.
q'
5
8. Vorlesung
Unifikation
Methoden der Künstlichen Intelligenz
Anderes Beispiel für Unifikation
•
Unifikation heißt hier:
Können Variablensubstitutionen gefunden werden, die die Ausdrücke
gleich machen (unifizieren)?
Substituiere Werte von Variablen so, daß zwei verschiedene Ausdrücke
gleich werden. (Werte können auch andere Variablen sein.)
p
(freund ?x,hans)
• Allgemein ist eine Substitution eine Menge von Variable-Wert-Paaren.
p'
(freund fritz,?y)
• Jedes solche Paar heißt Variablenbindung.
p und p' unterscheiden sich in den Argumenten des freund-Prädikats
Die Anwendung einer Substitution auf eine Formel heißt, jedes Vorkommen einer dadurch gebundenen Variablen durch ihren Wert zu ersetzen.
• Es können auch mehrere Ausdrücke (Formeln oder Terme) einer
gemeinsamen Substitution unterzogen werden!
Gegenbeispiel
(freund ?x,?x)
(freund fritz,hans)
Methoden der Künstlichen Intelligenz
(freund fritz,hans)
unifiziert mit der Variablensubstitution {x=fritz,y=hans}
• Entsprechende Variablen heißen durch die Substitution gebunden.
8. Vorlesung
6
?
unifiziert nicht (x kann nicht zwei Dinge zugleich sein)
7
8. Vorlesung
Methoden der Künstlichen Intelligenz
8
Verallgemeinerter Modus Ponens
Weitere Notationen und Begriffe
da capo
Benennung von Substitutionen durch griechische Buchstaben, z.B.:
Die Inferenzregel (III) ist ein Spezialfall der Resolutionsregel
in der Prädikatenlogik. Hauptgewinn:
θ
„theta“
Für p
Formel oder Term: notiere
in einem Mechanismus zusammengefaßt.
Beispiel:
• forward chaining für eine assertierte Formel p
θ
Substitution von
• verschiedene separate Inferenz-Mechanismen werden
durchzuführen, heißt dann:
pθ
deren Antezedenten p' mit der Assertion p
p:
(touching (side ?x) ?y)
θ =
pθ :
{ x = a, y = (surface ?z) }
(touching (side a) (surface ?z))
Subsumtion
unifizieren,
Man sagt, eine Formel p subsumiert (schließt ein) eine andere
Formel q , wenn es eine Substitution gibt mit p θ = q .
(auch:
"resolvieren").
Subsumption)
Beispiel: (not (divine ?x))
subsumiert
(not (divine fred))
8. Vorlesung
Methoden der Künstlichen Intelligenz
9
8. Vorlesung
q
Eine Substitution
schließe
θ
ist ein Unifikator für eine Menge
von Formeln oder Termen
folgt aus p
wenn
1)
10
"Vereinheitlicher"
(engl: unifier)
(IV) Subsumtions-Inferenz
q
= { x = fred }
Unifikator
Mit der Subsumtion erhält man eine einfache weitere Inferenzregel:
subsumiert
θ
mit
Methoden der Künstlichen Intelligenz
Subsumtionsinferenz, Varianten
Aus p
für das Resultat der
in p .
Begriff der
Finde Assertionen (if p' q )
(die mit der Assertion p
= { x = a, y = (surface ?z) }
p 1θ
= p 2θ
{ p 1, p 2, ..., p n }
=... = p nθ = P
(das heißt also, daß die p i durch die Substitution θ gleich werden).
Zwei Formeln, die sich gegenseitig subsumieren, heißen Varianten
(bedeuten das gleiche).
Beispiel:
2)
Beispiel:
(p ?x ?x) und (p ?y ?y) sind Varianten
(above ?z floor-19)
(if (above ?x ?y) (below ?y ?x))
p subsumiert q echt, wenn gilt:
θ
p subsumiert q , aber q subsumiert nicht p .
Beispiel:
8. Vorlesung
11
8. Vorlesung
haben als Unifikator:
={ x = table-21, y = floor-19, z = table-21 }
dann folgt (below floor-19 table-21)
(p ?x ?y) subsumiert echt (p ?x ?x)
Methoden der Künstlichen Intelligenz
und der Antezedent von
Methoden der Künstlichen Intelligenz
.
12
Übersicht Unifikation
Allgemeinster Unifikator
Ein Unifikator ist ein
Most General Unifier
(MGU)
MGU
(für eine Menge von Formeln oder
Termen), wenn das produzierte
P
nicht echt subsumiert wird
von dem P , das irgendein anderer Unifikator produziert.
Beispiel:
(dann folgt (below floor-19 table-21)
so, daß zwei Ausdrücke (Terme
(Terme oder Formeln) gleich macht.
oder Formeln) gleich werden.
(D.h. ein Unifikator ist eine spezielle
Eine Formel
)
Formel
und als
(ein MGU!!)
={ x = ?z, y = floor-19}
(dann folgt (below floor-19 ?z)
8. Vorlesung
Die Substitution
Der
Der
MGU
MGUist
ist
eindeutig
eindeutig
(bis
(bisauf
auf
Varianten)
Varianten)
Subsumtion:
1. Unifikator (s.o. - kein MGU!)
θ 1 ={ x = table-21, y = floor-19, z = table-21 }
θ2
das Substituieren von Variablen
haben als
(if (above ?x ?y) (below ?y ?x))
2. Unifikator
(Vor allen Dingen
bleiben Variablen
erhalten, was oft
wichtig ist.)
Unifikator:
und der Antezedent von
(above ?z floor-19)
Es ist günstig, einen
möglichst allgemeinen
Unifikator zu finden:
damit nur so viele
Spezialisierungen
erfolgen, wie eben
nötig sind.
Unifikation:
).
q
p
q
aus
p
13
Das
Dasist
ist
der
der
beste!
beste!
Allgemeinster Unifikator (MGU):
durch
Diejenige unifizierende Substitution, die
eine Variablensubstitution hervorgeht.
am wenigsten Spezialisierungen vornimmt.
(Formeln, die sich gegenseitig
Man kann zeigen: Für jede unifizierbare
subsumieren, heißen Varianten.)
Menge von Formeln existiert ein MGU!
MGUs sind gut
fürs chaining!
Methoden der Künstlichen Intelligenz
die zwei Ausdrücke
Substitution!)
subsumiert eine
, wenn
θ,
siehe
siehe z.B.
z.B. Lloyd:
Lloyd: Foundations
Foundations of
of Logic
Logic Programming
Programming
8. Vorlesung
Methoden der Künstlichen Intelligenz
14
Rückwärtsverkettung – Idee
Vorwärts- und Rückwärtsverkettung
Die meisten Inferenzen in einem deduktiven System werden
Forward Chaining
Aus
p'
inferiere
wobei
p
mit MGU
(if p q )
und
q'
zur Query Time vorgenommen.
(if p q )
• GATEKEEPER wird eine Implikation
sei assertiert.
p'
und
unifiziert
und
q'= q θ
wird
(if p q )
zwar
assertieren, aber nichts damit anstellen, bis eine Frage
q' gefragt wird (als goal)
q,q' haben MGU θ
p'= p θ als subgoal aufgeworfen.
Wenn nach
mit
θ
Backward Chaining
(query) der Form
(subgoal)
p'
q'
gestellt wird. Dann wird subquery
gestellt.
• Das Stellen von subgoals, sub-subgoals etc. wird durch
• Inferenz zur Assertion Time
• Inferenz zur Query Time
• "Die Assertion resolviert mit der Implikation."
• "Das goal resolviert mit der Implikation."
Goal Trees
(Zielbäume)
Ziel
backward chaining (Rückwärtsverkettung) bewerkstelligt.
• Der Basismechanismus des Backward Chaining bezieht sich
auf nichtkonjunktive goals: Verkettung von Implikationen
(rückwärts).
Rückwärtsverkettung: zielorientiertes Inferenzverfahren
(bei konjunktiven (sub-)goals in Verbindung mit Goal Tree-Suche)
Teilziele
• Als Suchstruktur bei konjunktiven goals von der Form
(if (and p1 p2 ) q)
8. Vorlesung
Methoden der Künstlichen Intelligenz
15
8. Vorlesung
werden Goal Trees eingesetzt.
Methoden der Künstlichen Intelligenz
16
Goal-Formeln kennzeichnen
Goal-Formeln skolemisieren
Für goals werden die Konventionen fürs Skolemisieren
Verwende (Show: formula ) zur Kennzeichnung von
umgedreht (entsprechend dem Verfahren bei not ):
goal-Formeln.
Logisch gesehen ist Show:
Antwort
Anfrage
INTERFACE
Hier am Beispiel
(Show: (color tweety yellow))
gleichbedeutend mit not
bzw. subgoal
(Show: (inst tweety canary))
(die entsprechenden Aus-
• Show: ist kein logischer Junktor!
(manchmal Pseudo-Junktor genannt)
• hängt aber zusammen mit dem
DATABASE
Junktor not
8. Vorlesung
(kommt später)
Wenn eine Anfrage
(query) an DATABASE
gestellt wird, muß die
entsprechende Formel
gekennzeichnet werden,
um sie von den "beliefs"
(assertierten Formeln)
unterscheiden zu
können.
Methoden der Künstlichen Intelligenz
17
(Show: (forall (y) (color y yellow)))
•
(not (color tweety yellow))
wird probeweise assertiert – als Annahme;
entspricht Show: einer
gemachte Assertion)
intuitiv: Wenn es für ein gewisses sk-8 gezeigt werden
kann, kann es für beliebige Instanzen gezeigt werden.
8. Vorlesung
Methoden der Künstlichen Intelligenz
18
mit forward und
backward chaining
als Spezialfällen:
Klauseldarstellung!
Schreibe
(if p q)
als (or (not p) q)
Chaining
Aus
und
inferiere
Forward
p'
(or (not p) q)
q'
Abschnitt 6.6
Backward
(not q')
(or q (not p))
(not p')
in Charniak/
Allgemein
not m'
Forward
m =(not p)
n = q
Backward
m = q
n =(not p)
siehe
Schon vorhandene "geglaubte" Assertionen:
(inst tweety canary)
(if (inst ?x canary)(color ?x yellow))
was gleichbedeutend ist mit:
(or (not(inst ?x canary))(color ?x yellow))
(or m n)
n'
McDermott
mit unifizierender Substitution analog zu (III)
Das negierte goal resolviert mit der Implikation zu
(not (inst tweety canary))
Methoden der Künstlichen Intelligenz
(Show: (color sk-8 yellow))
Annahme (probeweise
Weitere Details
(beide RegelAntezedenten
dürfen disjunktiv
sein)
WIDERSPRUCH! Also gilt das ursprüngliche goal.
8. Vorlesung
wird skolemisiert als
pragmatisch gesehen
Allgemeine Resolutionsregel
(Show: (color tweety yellow)) – goal – kann als Versuch verstanden
werden, (color tweety yellow) durch Widerspruch zu beweisen:
•
(Show: (color ?y yellow))
Weise skolemisiert)
Resolutionsregel – grobe Idee
•
wird skolemisiert als
drücke werden in gleicher
(bezogen auf früheres Beispiel)
GATEKEEPER
(Show: (exists (y) (color y yellow)))
19
8. Vorlesung
(V) Allgemeine Resolutionsregel
Aus (or n 1 (not m' )) und (or m n 2)
inferiere (or n 1' n 2 ')
Methoden der Künstlichen Intelligenz
20
Zentral: Antwortsubstitution
Theorembeweiser – Goal Tree
Beispiel: Assertiert seien
Allgemein:
(i)
Bei konjunktiven Goals sind Antworten für ein
(inst tweety canary)
Gegeben das goal (Show:q')
mit (if p q) in DATABASE
und q,q'haben MGU θ .
(ii) (if (inst ?x canary)(color ?x yellow))
Produziere subgoal (Show:pθ)
und falls das eine Antwort ψ hat,
ist θ U ψ eine Antwort auf das
resolviert mit (ii) zum subgoal
(Show: (inst ?y canary))
ursprüngliche goal.
„theta“
(Show: (color ?y yellow))
Dies unifiziert mit (i) zu
(inst tweety canary)
als goal
θ = {x = ?y}
Die beim backwardbackwardchaining vorgenommenen
Substitutionen liefern
eine spezifische Antwort!
8. Vorlesung
führt zu der Antwort "Ja, tweety ist gelb": {x = tweety}
Theorembeweiser
---> Goal Tree-Suche
Ziel
Die UND-Knoten eines Goal Trees enthalten
constraints: Randbedingungen an die
Teilziele
Lösungen für jede ihrer Komponenten.
•
Hier sind das die folgenden: Die Variablen-
Charniak & McDermott,
Kap. 6, 351-360; 378ff.
bindungen für gleich benannte Variablen in
den Teillösungen müssen identisch sein!
Antwortsubstitution
Methoden der Künstlichen Intelligenz
21
8. Vorlesung
Methoden der Künstlichen Intelligenz
(grossvater fritz ?u)
PROLOG: ""PROgramming
PROgramming in LOGic"
LOGic" (Basis: Hornformeln der PL)
Eine Definition von "Großvater":
Für alle x, für alle y, für alle z gilt:
x ist Großvater von y, wenn
x Vater von z ist und z Vater von y.
oder ganz formal:
∀x∀
∀y∀
∀z (grossvater x y)
← (vater x z)(vater z y)
In PROLOG gelten alle Variablen als implizit allquantifiziert (matchen mit beliebigen Termen);
Quantoren werden weggelassen:
(grossvater ?x ?y)1
← (vater ?x ?z)(vater ?z ?y)
(grossvater ?x ?y)2
← (vater ?x ?z)(mutter ?z ?y)
∀ x∀
∀y∀
∀z (grossvater x y)
← (vater x z)(mutter z y)
"klassische" Clocksin/Mellish–Syntax:
grossvater(X Y)
:− vater(X Z),vater(Z Y)
(vater fritz hans)
(vater fritz klara)
(mutter klara peter)
Show: Ist Fritz ein Großvater?
(grossvater fritz ?u)
>(grossvater fritz peter)
Methoden der Künstlichen Intelligenz
23
(grossvater ?x ?y)2
(grossvater ?x ?y)1
(vater ?x ?z)
Seien dazu nun noch folgende Fakten assertiert:
Die entsprechende Definition
"über die Mutter":
22
Goal-Tree-Suche in PROLOG
Ein PROLOG-Beispiel
8. Vorlesung
anderen Konjunkte sind.
("Deductive Retriever")
Leseempfehlung heute:
D.h. die Frage "Existiert etwas, das gelb ist?"
Konjunkt zu finden, die auch Antworten für die
Algorithmus:
Goal Trees
(Zielbäume)
ψ = {y = tweety}
und damit bestätigt sich das ursprüngliche goal zu
(color tweety yellow)
θ U ψ = {x = tweety}
„psi“
Bei konjunktiven (sub)goals
z.B. (if (and r1 r2) q)
(vater
fritz
hans)
(vater
fritz
klara)
(vater ?z ?y)
(vater
fritz
hans)
(vater
fritz
klara)
(vater ?x ?z)
(vater
fritz
hans)
(vater
fritz
klara)
(mutter ?z ?y)
(mutter
klara
peter)
redo:
(grossvater fritz ?u)
show:
(grossvater fritz ?u)
show:
(vater fritz ?z)
show:
(vater fritz ?z)
success: (vater fritz hans)
success: (vater fritz hans)
show:
(vater hans ?y)
show:
(mutter hans ?y)
redo:
(vater hans ?y)
fail:
(mutter hans ?y)
fail:
(vater hans ?y)
redo:
(vater fritz ?z)
redo:
(vater fritz ?z)
success: (vater fritz klara)
show:
(mutter klara ?y)
success: (vater fritz klara)
success: (mutter klara peter)
show:
(vater klara ?y)
redo:
(vater klara ?y)
success: (grossvater fritz peter)
fail:
(vater klara ?y)
8. Vorlesung
Methoden der Künstlichen Intelligenz
FRAGE:
Was sind
hier die
Constraints
an den
UNDKnoten?
ANTWORT:
Dass die
Variablenbindungen
gleich
benannter
Variablen in
den Teillösungen
auch
tatsächlich
gleich sind.
24
© Copyright 2024 ExpyDoc
