Benutzer: Gast  Login
Originaltitel:
Proving Theorems of Higher-Order Logic with SMT Solvers 
Übersetzter Titel:
Beweisen von Theoremen in höherstufiger Logik mit SMT-Lösern 
Jahr:
2012 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Rybalchenko, Andrey (Prof. Dr.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Schlagworte (SWD):
Automatisches Beweisverfahren; Isabelle Programm; HOL 
TU-Systematik:
DAT 706d 
Kurzfassung:
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...    »
 
Übersetzte Kurzfassung:
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...    »
 
Mündliche Prüfung:
11.05.2012 
Dateigröße:
611676 bytes 
Seiten:
128 
Letzte Änderung:
17.11.2017