Transcript
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
