Login
- Original title:
- 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. - WWW:
- https://mediatum.ub.tum.de/?id=676608
- Date of submission:
- 30.04.2008
- Oral examination:
- 09.10.2008
- Pages:
- 155
- Urn (citeable URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20081018-676608-1-8
- Last change:
- 22.03.2011
BibTeX