Login
- Originaltitel:
- Automatic Proofs and Refutations for Higher-Order Logic
- Übersetzter Titel:
- Automatische Beweise und Gegenbeispiele für die höherstufige Logik
- Autor:
- Blanchette, Jasmin Christian
- Jahr:
- 2012
- Dokumenttyp:
- Dissertation
- Fakultät/School:
- Fakultät für Informatik
- Betreuer:
- Nipkow, Tobias (Prof., Ph.D.)
- Gutachter:
- Nipkow, Tobias (Prof., Ph.D.); Claessen, Koen (Prof., Ph.D.)
- Sprache:
- en
- Fachgebiet:
- DAT Datenverarbeitung, Informatik
- Stichworte:
- Theorem proving, model finding
- Übersetzte Stichworte:
- Theorembeweisen, Modellsuche
- Schlagworte (SWD):
- Isabelle Programm; HOL; Gegenbeispiel; Generierung
- TU-Systematik:
- DAT 706d
- Kurzfassung:
- 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.
- Übersetzte Kurzfassung:
- 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
- Eingereicht am:
- 02.03.2012
- Mündliche Prüfung:
- 28.06.2012
- Dateigröße:
- 1613269 bytes
- Seiten:
- 183
- Urn (Zitierfähige URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20120628-1097834-1-6
- Letzte Änderung:
- 31.08.2012
BibTeX