185.216
AK der Theoretischen Informatik 5, VU, 2.0 Std. (SS 2004)

Lehrveranstaltungsleiter: Alexander Leitsch

Thema: Automatische Modellbildung

Inhalt:

Automatische Beweiser sind grundsätzlich Semi-entscheidungsverfahren, welche Beweise zu gültigen Aussagen der Prädikatenlogik generieren. Auf Grund der Unentscheidbarkeit der Prädikatenlogik gibt es dagegen kein Verfahren welches für alle ungültigen Formeln automatisch Gegenbeispiele generiert. Für gewisse Klassen von Problemen lassen sich jedoch die Gültigkeit algorithmisch entscheiden und Gegenbeispiele erzeugen. Wir behandeln diese Fragestellung im Rahmen des Resolutionskalküls; hier besteht das Problem darin, für erfüllbare Klauselmengen Modelle zu konstruieren (unerfüllbare Klauselmengen repräsentieren gültige Sätze). Insbesonders untersuchen wir 1. die Hyperresolution und die Erzeugung von Atomrepräsentationen (ARM) von Herbrandmodellen, sowie 2. constrained clause logic, den Kalkül RAMC und die Erzeugung von constrained atomic representations (CARM) von Herbrand Modellen. Die erzeugten Modelle sind in der Regel unendlich was symbolische Darstellungen (im Gegensatz zu Modelltafeln) schon im Prinzip notwendig macht. Abschliessend werden Methoden zur algorithmischen Klauselevaluation über Repräsentationen (ARM und CARM) von Herbrand Modellen angegeben.

Literatur: R. Caferra, A. Leitsch, N. Peltier, Automated Model Building, Kluwer Verlag (erscheint 2004).

Zeit:

im Block zu den folgenden Terminen:
Dienstag, 20.4.2004, 14 - 18,
Dienstag, 27.4.2004, 14 - 18,
Dienstag, 4.5.2004, 14 - 18,
Dienstag, 11.5.2004, 14 - 18,
Dienstag, 18.5.2004, 14 - 18,
Dienstag, 25.5.2004, 14 - 18.

Ort:

ab 27.4.2004 Seminarraum 184/2, Favoritenstrasse 9, Stiege I, 3. Stock, blaue Zone.
Achtung: am 20.4.2004 im Zimmer HC 03 01, Institut für Computersprachen, Favoritenstrasse 9, Stiege II, 3. Stock, violette Zone.

Voraussetzungen:

Gute Kenntnisse der Prädikatenlogik und Grundkenntnisse des Automatischen Beweisens.

Bei Fragen wenden Sie sich bitte direkt an den Vortragenden.


Navigation: