AIMA Notizen
Teil III
Kapitel 9: Inferenz in der Prädikatenlogik
Inhalt
- Reduktion der
Prädikatenlogik auf die Aussagenlogik
- Skolemisierung
(-> F1-Skript) entfernt die
Existenzquantoren, Inferenzäquivalenz
- Propositionalisierung
entfernt Allquantoren und ersetzt den
Ausdruck durch entsprechende Ausdrücke für alle
konstanten
Symbole
- geht (nur?) für
beschränkte Domänen
- jetzt kann
aussagenlogische Inferenz benutzt werden, allerdings
ist die KB beträchtlich gewachsen. sehr langsam
- semientscheidbar: nur
für positive Antworten ist
Terminierung sichergestellt (das gilt allerdings für die
gesamte
Prädikatenlogik)
- Inferenz, Unifizierung,
Lifting in der Prädikatenlogik
- generalisierter
Modus-Ponens für die Prädikatenlogik
- nur die Substitutionen
werden ausgeführt die auch
tatsächlich notwendig sind, nicht alle, wie bei der Reduktion
auf
die Aussagenlogik
- Unifizierung (->
F1-Skript) verdongelt die Variablen so,
dass zwei Ausdrücke gleich werden
- occur check ist
rechenintensiv und wird deswegen meist
(PROLOG) weggelassen
- Lifting beschreibt den
Vorgang etwas von der Aussagenlogik auf
die höhere Stufe der Prädikatenlogik zu heben
- Forward Chaining
(Vorwärtsverkettung, bottom-up)
- definite Klauseln: genau
ein positives Literal (also Fakten und
Regeln)
- die KB darf nur definite
Klauseln enthalten
- Verkettung der Regeln von
den Fakten aus bis die Anfrage
abgeleitet ist
- DATALOG
- Fixpunkt: ab hier sind
keine Inferenzen mehr möglich bis
neue Klauseln der KB hinzugefügt werden
- effizientes Forward
Chaining:
- most constrained
variable: der eingeschränkteste Teil
der Prämisse wird zuerst belegt und davon abhängig
die
anderen Teile der Prämisse gecheckt
- inkrementelles Forward
Chaining betrachtet bei jedem Schritt
nur Regeln, deren Prämissen Prädikate enthalten,
über
die im vorherigen Schritt etwas herausgefunden wurde
- irrelevante Fakten
können vermieden werden, indem ein
Magic Set rückwärts vom Ziel ausgehend gebildet wird
und nur
damit die Inferenz betrieben wird (hybrider Ansatz zwischen Forward-
und Backward)
- Backward Chaining
(Rückwärtsverkettung, top-down)
- PROLOG
- implizite
Substitutionsfunktion die sich direkt aus der
Belegung der Variablen ergibt
- Tiefensuche
- Reihenfolge der Klauseln
in der KB ist relevant
- unvollständig
- Resolution
- so wie schon bei der
aussagenlogischen Resolution, bloß
dass Substitution hinzukommt
- Resolution produziert
Beweise, aber meist keine
verständlichen Begründungen
- Resolution ist langsam und
komplex, nur positive Antwort ist
garantiert
- Resolutionsstrategien
- Einheitspräferenz
(unit preference): Resolutionsschritte
bei denen eine der Klauseln Einheitsklauseln (Fakten) sind werden
bevorzugt, da sie zu kleineren Resolventen führen
- insgesamt werden
kürzere Klauseln bei der Resolution
bevorzugt
- set of support: wird vor
der Resolution festgelegt. jeder
Schritt wird mit einer Klausel aus der Menge ausgeführt und
die
Resolvente wird der Menge hinzugefügt
- gängige
Methode: am Anfang steht in der Menge nur die
Negation der Anfrage
- theorem
provers
- vollständig
- meist zur
Unterstützung von Menschen (daher fällt die
Semientscheidbarkeit weniger ins Gewicht, da der Mensch gegebenenfalls
die Anfrage abbricht und eine andere formuliert)
letzte Änderung: 20.
Dezember 2004.
mail
AT timobaumann.de