Gedächtnisprotokoll zur Diplomprüfung Deduktions- und
Inferenzsysteme (1695)
Kurs:
Deduktions- und Inferenzsysteme (1695)
Datum:
2.3.1998
Prüfer:
Prof. Dr. Beierle
Note:
1,3
Was sind Syntax und Semantik der Prädikatenlogik 1. Stufe?
Signatur, Terme, Formeln, Interpretation.
Wie ist eine logische Folgerung definiert?
(siehe Kurs).
Wann ist eine Formel allgemeingültig?
(siehe Kurs).
Wie beweist man dies?
Hier war verlangt: Durch Unerfüllbarkeit der negierten Formel.
Wie lautet der Satz von Herbrand für Klauselmengen?
(siehe Kurs).
Welche Arten von Kalkülen gibt es?
positive, negative, deduktive, Testkalküle.
Was ist die Idee des Gentzen-Kalküls?
Angelehnt an Schlußfolgerungen von Mathematikern; man erzeugt
Annahmen, von denen man sich wieder freimachen muß
Welche Regeln sind besonders kritisch?
Existenz-Einführung und Schnittregel, da man den wegzuschneidenden
Ausdruck geschickt wählen muß.
Wie funktioniert Resolution?
Resolvieren zweier Atome, die einmal negiert und einmal nicht-negiert
vorliegen
Müssen diese Atome gleich sein?
Nein => Unifikation
Welchen Unifikator verwendet man?
mgu
Wie lautet ein Algorithmus zur Unifikation?
Siehe Kurs: Robinson-Unifikation
Ist dieser mgu eindeutig?
Ja, bis auf Variablenumbenennung
Wie sieht es bei der E-Unifikation aus, ist dort der mgu eindeutig?
nein
Was verwendet man stattdessen?
Lösungsbasis
Was versteht man unter dem Hierarchieproblem?
Einordnen eines Problems in eine von vier Klassen.
Beschreiben Sie die Klassen.
Unitär, finitär, infinitär, Typ 0 (siehe Kurs).
Was ist die Idee der Theorieresolution?
Auch semantische Widersprüche können resolviert werden.
Wie ist ein Klauselgraph aufgebaut?
(siehe Kurs).
Wie funktioniert Resolution auf einem Klauselgraphen?
Auf den R-Kanten.
Wie kann man den Suchraum beeinflussen?
Durch Reduktionsregeln.
Nennen Sie eine.
(Im Kurs werden vier beschrieben).
Wofür kann man einen Klauselgraphen noch verwenden?
Theorieresolution.
Welches Problem stellt sich bei der Behandlung der Gleichheit?
Explosion des Suchraums.
Welche Lösungsmöglichkeiten gibt es in Bezug auf die Resolution?
Ich nannte Paramodulation, aber erwartet war wohl Termersetzung.
Wie arbeitet die Termersetzung?
Gleichungen werden nur in einer Richtung angewendet.
Kann man jedes Gleichungssystem so verwenden?
Nein, Umwandeln in ein Regelsystem.
Welche Eigenschaften eines Regelsystems sind wünschenswert?
Konfluenz und Terminierung.
Was bedeutet Konfluenz?
(siehe Kurs)
Wie kann man Terminierung überprüfen?
Durch Erzeugen einer wohlfundierten Ordnungsrelation, so daß
die Regeln des TRS eine Teilmenge dieser Ordnungsrelation
sind. Oder mit RPO.
Wie kann man Konfluenz überprüfen?
Mit kritischen Paaren etc. (siehe Kurs).
Welches Ergebnis kann der Knuth-Bendix-Algorithmus liefern?
Erfolg, Mißerfolg, Nicht-Beendung.
Was ist eine Hornklausel?
(siehe Kurs).
Wie funktioniert die SLD-Resolution?
(siehe Kurs).
Was ist ein SLD-Baum?
(siehe Kurs).
Hat die Auswahlfunktion Einfluß auf die Vollständigkeit des Baumes?
Nein.
Wie ist starke Vollständigkeit eines SLD-Baumes definiert?
Alles in allem fand ich mich bei der Prüfung ein wenig gehetzt, es schien,
als wären meine langen Antworten teilweise unerwünscht.
Auch verhielt sich Prof. Beierle sehr passiv beim Zuhören; ich
erhielt sehr wenig Feedback zu dem, was ich gerade sagte.