Technische Universität München, Fakultät für Informatik
Bereich: 2 SWS Vorlesung im Bereich Informatik III (Theoretische Informatik)
Termin: Do. 14.15-15.45, Beginn 24.10.02
Ort: Raum 00.09.055
Schein: durch Teilnahme an Semestralklausur oder mündliche Prüfung
Im Automatischen Beweisen geht es um das Problem der maschinellen Suche nach Beweisen der Gültigkeit von Formeln der Prädikatenlogik 1. Stufe. Der breite industrielle Einsatz automatischer Beweiser wird in den nächsten Jahren erwartet. Auf Grund der Unentscheidbarkeit der Prädikatenlogik 1. Stufe kann es aber keine Entscheidungsverfahren geben. In vielen Anwendungen automatischer Beweiser reicht aber diese Funktionalität nicht aus.
In dieser Vorlesung konzentrieren wir uns deshalb auf entscheidbare Teilsprachen der Prädikatenlogik, die für viele Anwendungen ausreichen. In der Vorlesung wird im Detail der aktuelle Forschungsstand der leistungsfähigsten Entscheidungsverfahren für wichtige Teilsprachen der Prädikatenlogik dargestellt. Die Bandbreite der betrachteten Teilsprachen reicht von der Aussagenlogik über die sog. Quantifizierte Boolsche Logik und die Modallogik zu Sprachen wie dem Guarded Fragment der Prädikatenlogik. Da Entscheidungsverfahren für die Aussagenlogik (sog. SAT-Solver) bereits in vielen Bereichen mit stark steigender Tendenz eingesetzt werden, wird dieses Thema einen Schwerpunkt der Vorlesung bilden. Weiterhin werden auch effiziente Implementationstechniken vorgestellt und diskutiert sowie die Performanz konkreter Solver an Hand von Beispielen demonstriert.
Improvements to Propositional Satisfiability Search Algorithms
Freeman, J.W., PhD thesis, The University of Pennsylvania, 1995.
The Search for Satisfaction
Ian Gent and Toby Wash, 1999.
Algorithms for the Satisfiability (SAT) Problem: A Survey
J. Gu, P. W. Purdom, J. Franco, and B. W. Wah, in
"Satisfiability Problem: Theory and Applications", DIMACS Series in Discrete
Mathematics and Theoretical Computer Science, American Mathematical
Society, 1997, pp. 19-152.
Ordered binary decision diagrams and the Davis-Putnam procedure.
Uribe, T.E. and M.E. Stickel,
Proceedings of the First International Conference on Constraints in
Computational Logics,
Munich, Germany, September 1994, 34-49.
First-Order Calculi and Proof Procedures for Automated Deduction .
R. Letz, Dissertation, TU Darmstadt, 1993
The Quest for Efficient Boolean Satisfiability Solvers.
Lintao Zhang, Sharad Malik:
Proceedings of the 14th Conference on Computer-Aided Verification,
Copenhagen 2002, 17-36
Liste wird noch vervollständigt
Material vom 24.10.02 bis 19.12.02 , Material vom 9.1.03 (QBF-Verfahren) , Material vom 16.1.03 (Datenlogik-Verfahren)
SATLIB - The Satisfiability Library
SAT: references on satisfiability