User: Guest  Login
Original title:
Automatic Proofs and Refutations for Higher-Order Logic 
Translated title:
Automatische Beweise und Gegenbeispiele für die höherstufige Logik 
Year:
2012 
Document type:
Dissertation 
Institution:
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. 
Oral examination:
28.06.2012 
File size:
1613269 bytes 
Pages:
183 
Last change:
31.08.2012