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 over rings, universal polynomial problems over the reals, quantifier elimination for parametric linear problems over ordered fields, Presburger arithmetic, mixed real-integer linear arithmetic, algebraically and real closed fields. Our work has been carried out in the Isabelle framework.     «

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...     »

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 Beweisverfahren im Detail. Die wichtigsten präsentierten Verfahren sind: a) Entscheidungsprozeduren für universelle und schwach existentielle Probleme in Ringen, b) Univerelle Probleme reeller Polynome, c) Quantoren-elimination für parametrische lineare Formeln über geordnete Körper, Presburger Arithmetik, die gemischte lineare Theorie der reelen und ganzen Zahlen, Algebraisch- und Reel-abgeschlossene Körper. Alle unsere Arbeiten basieren auf dem Isabelle Theorembeweiser.     «

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...     »