Benutzer: Gast  Login
Originaltitel:
Automated methods for formal proofs in simple arithmetics and algebra 
Übersetzter Titel:
Automatische Methoden für formale Beweise in einfachen Arithmetiken und Algebren 
Jahr:
2008 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Avigad, Jeremy (Prof., Ph.D.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik; MAT Mathematik 
Stichworte:
verification, theorem proving, decision procedures, logic 
Übersetzte Stichworte:
Verifikation, Automatisches Beweisen, Entscheidungsprozedur, Logik, Theorembeweiser 
Kurzfassung:
In an LCF-like theorem prover, any proof must be produced from a small set of inference rules. The development of automated proof methods in such systems is extremely important. In this thesis we study the following question: How should we integrate a proof procedure in an LCF-like theorem prover, both in general and in the special case of arithmetics? We investigate three integration paradigms and present several proof procedures. These include universal and weak existential prob...    »
 
Übersetzte Kurzfassung:
In einem LCF-ähnlichen Theorembeweiser, stammt jeder Beweis aus einer minimalen Menge von Inferenzregeln ab. Somit sind Verfahren zur Generierung solcher Beweise von enormer Wichtigkeit. Das Ziel dieser Abhandlung ist folgende Frage zu studieren: Wie soll, allgemein und im Spezialfall der Arithmetik, ein LCF-ähnlicher Theorembeweiser um eine Entscheidungsprozedur erweitert werden? Wir betrachten drei verschiedene Ansätze für eine solche Integration und präsentieren mehrere Be...    »
 
Mündliche Prüfung:
11.04.2008 
Seiten:
100 
Letzte Änderung:
22.04.2008