User: Guest  Login
Original title:
Proving Theorems of Higher-Order Logic with SMT Solvers 
Translated title:
Beweisen von Theoremen in höherstufiger Logik mit SMT-Lösern 
Year:
2012 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Nipkow, Tobias (Prof., Ph.D.); Rybalchenko, Andrey (Prof. Dr.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Controlled terms:
Automatisches Beweisverfahren; Isabelle Programm; HOL 
TUM classification:
DAT 706d 
Abstract:
Following the demand for increased proof automation in the interactive theorem prover Isabelle, this thesis describes how SMT solvers improve on the state of the art. Our main contributions are a sound translation from Isabelle's higher-order logic to the first-order logic of SMT solvers, and efficient checking of proofs found by the SMT solver Z3. Based on a large evaluation, we find that many theorems can now be proved automatically and almost instantaneously for which time-consuming user inge...    »
 
Translated abstract:
Der Nachfrage nach erhöhter Beweisautomatisierung für den interaktiven Theorembeweiser Isabelle folgend zeigt diese Arbeit, wie SMT-Löser den Stand der Technik verbessern können. Unsere Hauptbeiträge sind eine korrekte Übersetzung von Isabelles höherstufiger Logik in die erststufige Logik von SMT-Lösern sowie die effiziente Rekonstruktion von Beweisen des SMT-Lösers Z3. Mittels einer umfangreichen Evaluierung belegen wir, dass viele Theoreme nun automatisch und nahezu sofort bewiesen werden könn...    »
 
Oral examination:
11.05.2012 
File size:
611676 bytes 
Pages:
128 
Last change:
17.11.2017