User: Guest  Login
Original title:
Automated methods for formal proofs in simple arithmetics and algebra 
Translated title:
Automatische Methoden für formale Beweise in einfachen Arithmetiken und Algebren 
Year:
2008 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Avigad, Jeremy (Prof., Ph.D.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik; MAT Mathematik 
Keywords:
verification, theorem proving, decision procedures, logic 
Translated keywords:
Verifikation, Automatisches Beweisen, Entscheidungsprozedur, Logik, Theorembeweiser 
Abstract:
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 problems ov...    »
 
Translated abstract:
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 Beweisverf...    »
 
Oral examination:
11.04.2008 
Pages:
100 
Last change:
22.04.2008