In allgemeinen logische Formalismen wie Prädikatenlogik, Mengenlehre
oder Zahlentheorie sind die meisten Probleme unentscheidbar. Diese
Allgemeinheit wird in vielen Anwendungen gar nicht benötigt: Spezielle
Theorien wie Presburger Arithmetik, die Theorien der Listen und der Arrays
sind entscheidbar. Für computerunterstütztes Schließen in Anwendungen
ist es entscheidend, allgemeine deduktive Methoden (wie das
Resolutionsverfahren) mit Entscheidungsverfahren für spezielle
Theorien zu kombinieren. Dieses Vorgehen ermöglicht den Entwurf
entsprechender Systeme die in praktischen Anwendungen sinnvoll
eingesetzt werden können. Im Seminar sollen fundamentale Methoden zur
Konstruktion von Entscheidungsprozeduren für logische Theorien
vorgestellt werden.
Themen und Literatur
Unter Umständen können mehrere Vorträge zu einem Thema vergeben
werden. Weitere oder oft auch die angegebene Literatur zu
den Themen kann per
Google oder per CiteSeer/ recherchiert werden.
Abstract Congruence Closure
L. Bachmair and A. Tiwari.
Abstract congruence closure and specializations.
In D.A. McAllester, editor,
Proceedings of the 17th International Conference on Automated Deduction,
volume 1831 of LNAI, pages 64-78. Springer-Verlag, 2000.
G. Nelson and D.C. Oppen.
Fast decision procedures based on congruence closure.
Journal of the ACM, 27(2):356-364, 1980.
C.G. Fermüller,
A. Leitsch, U. Hustadt, and T. Tammet. Resolution decision procedures.
In A. Robinson and A. Voronkov, editors,
Handbook of Automated Reasoning, volume II, chapter 25, pages 1791-1849.
Elsevier Science Publishers, 2001.
W.H. Joyner Jr. Resolution. Strategies as Decision Procedures.
Journal of the ACM, 23(3):398-417, 1976.
J.E. Hopcroft and J.D. Ullmann.
Introduction to Automata Theory, Languages, and Computation,
chapter 2: Finite automata and regular expressions, pages 13-54.
Addison-Wesley, 1979.
H. Comon and C. Kirchner.
Presburger arithmetic and classical word automata.
In H. Comon, C. Marché and R. Treinen, editors,
Constraints in Computational Logic: Theory and Applications,
volume 2002 of LNCS,
chapter 2: Constraint solving on terms, section 8, pages 79-83.
Springer-Verlag, 1999.
E. Börger, E. Grädel, and Y. Gurevich.
The Classical Decision Problem,
chapter 6: Standard classes with the finite model property, pages 239-313.
Springer-Verlag, 1997.
Automatentheorie für Presburger Arithmetik.
Victor Rach
[ Ausarbeitung ]
Voraussetzungen
Vorlesung "Logik für Informatiker" oder "Deduktionssysteme".
Scheinerwerb
Vortrag ca. 45 Minuten inklusive 10 Minuten Diskussion.
Ausarbeitung im Umfang von ca.\ 10 Seiten. Die
Ausarbeitung muss 10 Tage vor Seminartermin fertig sein um
sie den anderen Seminarteilnehmern rechtzeitig zur Verfügung
zu stellen.
