SAT-based Finite Model Generation for Higher-Order Logic
Translated title:
SAT-basierte Generierung endlicher Modelle für höherstufige Logik
Author:
Weber, Tjark
Year:
2008
Document type:
Dissertation
Faculty/School:
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.
Login
BibTeX