Benutzer: Gast  Login
Originaltitel:
SAT-based Finite Model Generation for Higher-Order Logic 
Übersetzter Titel:
SAT-basierte Generierung endlicher Modelle für höherstufige Logik 
Jahr:
2008 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Veith, Helmut (Prof. Dr.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Schlagworte (SWD):
Modellgenerierung Künstliche Intelligenz; Isabelle Programm 
TU-Systematik:
DAT 706d; MAT 030d; DAT 540d 
Kurzfassung:
This thesis presents two extensions to the theorem prover Isabelle/HOL, a logical framework based on higher-order logic.
The main contribution is a model generator for higher-order logic that proceeds by translating the input formula to propositional logic, so that a standard SAT solver can be employed for the actual model search. The translation is proved correct. The model generator has been integrated with the Isabelle system, extended to support some of the definitional mechanisms provided by Isabelle/HOL, and applied to various case studies.
Moreover, SAT solvers have been integrated with Isabelle in a proof-producing fashion: propositional tautologies can be proved by a SAT solver, and the resolution proof found by the solver is verified by Isabelle. An adequate representation of the problem allows to verify proofs with millions of resolution steps. 
Übersetzte Kurzfassung:
Diese Arbeit präsentiert zwei Erweiterungen des Theorembeweisers Isabelle/HOL, einem auf Logik höherer Stufe basierenden System.
Der Hauptbeitrag ist ein Modellgenerator für höherstufige Logik, der seine Eingabeformel in Aussagenlogik übersetzt, so dass ein herkömmlicher SAT-Solver für die eigentliche Modellsuche verwendet werden kann. Die Korrektheit der Übersetzung wird gezeigt. Der Modellgenerator ist in das Isabelle-System integriert worden, unterstützt verschiedene definitorische Mechanismen, wie sie in Isabelle/HOL zur Verfügung stehen, und ist auf mehrere Fallstudien angewandt worden.
Darüber hinaus sind SAT-Solver beweisgenerierend mit Isabelle integriert worden: Aussagenlogische Tautologien können von einem SAT-Solver bewiesen werden, und der von dem Solver gefundene Resolutionsbeweis wird von Isabelle verifiziert. Eine günstige Repräsentation des Problems erlaubt die Verifikation von Beweisen mit mehreren Millionen Resolutionsschritten. 
Mündliche Prüfung:
09.10.2008 
Seiten:
155 
Letzte Änderung:
22.03.2011