Benutzer: Gast  Login
Originaltitel:
Automatic Proofs and Refutations for Higher-Order Logic 
Übersetzter Titel:
Automatische Beweise und Gegenbeispiele für die höherstufige Logik 
Jahr:
2012 
Dokumenttyp:
Dissertation 
Institution:
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. 
Mündliche Prüfung:
28.06.2012 
Dateigröße:
1613269 bytes 
Seiten:
183 
Letzte Änderung:
31.08.2012