Login
- Original title:
- Automatic Proofs and Refutations for Higher-Order Logic
- Translated title:
- Automatische Beweise und Gegenbeispiele für die höherstufige Logik
- Author:
- Blanchette, Jasmin Christian
- Year:
- 2012
- Document type:
- Dissertation
- Faculty/School:
- Fakultät für Informatik
- Advisor:
- Nipkow, Tobias (Prof., Ph.D.)
- Referee:
- Nipkow, Tobias (Prof., Ph.D.); Claessen, Koen (Prof., Ph.D.)
- Language:
- en
- Subject group:
- DAT Datenverarbeitung, Informatik
- Keywords:
- Theorem proving, model finding
- Translated keywords:
- Theorembeweisen, Modellsuche
- Controlled terms:
- Isabelle Programm; HOL; Gegenbeispiel; Generierung
- TUM classification:
- DAT 706d
- Abstract:
- This thesis describes work on two components of the interactive theorem prover Isabelle/HOL. The primary contribution is the development of Nitpick, a counterexample generator that builds on a first-order relational model finder. The second main contribution is the further development of the Sledgehammer proof tool. This tool heuristically selects facts relevant to the conjecture to prove and delegates the problem to first-order resolution provers and SMT solvers.
- Translated abstract:
- Diese Dissertation beschreibt die Arbeit an zwei Komponenten des interaktiven Theorembeweisers Isabelle/HOL. Der erste Beitrag ist die Entwicklung von Nitpick, einem Gegenbeispielgenerator, der auf einem erststufigen relationalen Modellfinder aufbaut. Der zweite Beitrag ist die Weiterentwicklung des Beweistools Sledgehammer. Dieses Tool wählt relevante Fakten aus und delegiert das Problem an erststufige Resolutionsbeweiser und SMT-Löser.
- WWW:
- https://mediatum.ub.tum.de/?id=1097834
- Date of submission:
- 02.03.2012
- Oral examination:
- 28.06.2012
- File size:
- 1613269 bytes
- Pages:
- 183
- Urn (citeable URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20120628-1097834-1-6
- Last change:
- 31.08.2012
BibTeX