User: Guest  Login
Original title:
SAT-based Finite Model Generation for Higher-Order Logic 
Translated title:
SAT-basierte Generierung endlicher Modelle für höherstufige Logik 
Year:
2008 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Veith, Helmut (Prof. Dr.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Controlled terms:
Modellgenerierung Künstliche Intelligenz; Isabelle Programm 
TUM classification:
DAT 706d; MAT 030d; DAT 540d 
Abstract:
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. 
Translated abstract:
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. 
Oral examination:
09.10.2008 
Pages:
155 
Last change:
22.03.2011