MPII Home PageMPII Home PageMPII Home Page

Peter Baumgartner

Up to: Research Units Building 46.1 Programming Logics Group

People - Selected



Entscheidungsverfahren für Logische Theorien

Seminar Wintersemester 2004/2005, Universität Koblenz-Landau.

Durchführung als Blockseminar am 1. und 2. März 2005, für genaue Angaben siehe unten.

Organisation und Betreuung: Peter Baumgartner, MPI für Informatik, Saarbrücken
Email: baumgart@mpi-sb.mpg.de

Inhalt

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.
  • Vortrag: Sebastian Bochra, Ausarbeitung

Quantorenelimination


Geordnete Resolution

  • 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.
  • Vortrag: Kerstin Susewind, Ausarbeitung

Automatentheorie für Presburger Arithmetik

  • 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.
  • Vortrag: Victor Rach, Ausarbeitung

Endliche Modelle

  • 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.
  • Vortrag: Tobias Hebel, Ausarbeitung

Durchführung

Dienstag, 1. März, 14-17, Raum MA 120:
14:15 - 15:00
Endliche Modelle. Tobias Hebel [ Ausarbeitung ]
15:00 - 15:45
Geordnete Resolution. Kerstin Susewind [ Ausarbeitung ]
16:00 - 16:45
Die kongruente Hülle. Sebastian Bochra [ Ausarbeitung ]
Mittwoch, 2. März, 10-12, Raum MA 120:
10:15 - 11:00
Quantorenelimination. Stefanie Lück [ Ausarbeitung ]
11:00 - 11:45
Automatentheorie für Presburger Arithmetik. Victor Rach [ Ausarbeitung ]

Voraussetzungen

Vorlesung "Logik für Informatiker" oder "Deduktionssysteme".

Scheinerwerb


This web page is maintained by Peter Baumgartner <baumgart@mpi-sb.mpg.de>.
Last modified: Mon Jul 25 09:12:51 CEST 2005