This article presents detailed implementations of quantifier elimination for both integer and real linear arithmetic for theorem provers. The underlying algorithms are those by Cooper (for Z) and by Ferrante and Rackoff (for R). Both algorithms are realized in two entirely different ways: once in tactic style, i.e. by a proof-producing functional program, and once by reflection, i.e. by computations inside the logic rather than in the meta-language. Both formalizations are highly generic because they make only minimal assumptions w.r.t. the underlying logical system and theorem prover. An implementation in Isabelle/HOL shows that the reflective approach is between one and two orders of magnitude faster.

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

We use higher-order logic to verify a quantifier elimination procedure for linear arithmetic over ordered fields, where the coefficients of variables are multivariate polynomials over another set of variables, we call parameters. The procedure generalizes Ferrante and Rackoff's algorithm for the non-parametric case. The formalization is based on axiomatic type classes and automatically carries over to e.g.the rational, real and non-standard real numbers. It is executable, can be applied to HOL formulae by reflection and performs well on practical examples.

Proof reconstruction is a technique that combines an interactive theorem prover and an automatic one in a sound way, so that users benefit from the expressiveness of the first tool and the automation of the latter. We present an implementation of proof reconstruction for first-order logic and set-theoretical constructions between the interactive theorem prover Isabelle and the automatic SMT prover HarVey.

We report on some recent experiments with SML embedded into the Isabelle/Isar theory and proof language, such that the program text may again refer to formal logical entities via antiquotations. The meaning of our antiquotations within SML text observe the different logical environments at compile time, link time (of theory interpretations), and runtime (within proof procedures). As a general design principle we neither touch the logical foundations of Isabelle, nor the SML language implementation. Thus we achieve a modular composition of the programming language and the logic within the Isabelle/Isar framework. Our work should be understood as a continuation and elaboration of the original “LCF system approach”, which has introduced ML as a programming language for theorem proving in the first place.

We address some aspects of a system architecture for mathematical assistants that integrates calculations and deductions by common infrastructure within the Isabelle theorem proving environment. Here calculations may refer to arbitrary extra-logical mechanisms, operating on the syntactic structure of logical statements. Deductions are devoid of any computational content, but driven by procedures external to the logic, following to the traditional “LCF system approach”. The latter is extended towards explicit dependency on abstract theory contexts, with separate mechanisms to interpret both logical and extra-logical content uniformly. Thus we are able to implement proof methods that operate on abstract theories and a range of particular theory interpretations. Our approach is demonstrated in Isabelle/HOL by a proof-procedure for generic ring equalities via Gröbner Bases.

We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer arithmetics in higher-order logic based on a work by Weispfenning. To this end we provide two verified quantifier elimination procedures: for Presburger arithmitics and for linear real arithmetics.

Proof-producing program analysis augments the invariants inferred by an abstract interpreter with their correctness proofs. If these invariants are precise enough to guarantee safety, this method is an automatic verification tool. We present proof-synthesis algorithms for a simple flow chart language and domains Vars-> Values mapping variables to abstract values and discuss some benefits for proof carrying code systems. Our work has been carried out in Isabelle/HOL and incorporated within a verified proof carrying code system.

We integrate Ferrante and Rackoff's quantifier elimination procedure for linear real arithmetic in Isabelle/HOL in two manners: (a) tactic-style, i.e. for every problem instance a proof is generated by invoking a series of inference rules, and (b) reflection, where the whole algorithm is implemented and verified within Isabelle/HOL. We discuss the performance obtained for both integrations.

We present an implementation and verification in higher-order logic of Cooper's quantifier elimination for Presburger arithmetic. Reflection, i.e. the direct execution in ML, yields a speed-up of a factor of 200 over an LCF-style implementation and performs as well as a decision procedure hand-coded in ML.

Out of annotated programs proof carrying code systems construct and prove verification conditions that guarantee a given safety policy. The annotations may come from various program analyzers and must not be trusted as they need to be verified. A generic verification condition generat or can be utilized such that a combination of annotations is verified incrementally . New annotations may be verified by using previously verified ones as trusted facts. We show how results from a trusted type analyzer may be combined with untrusted interval analysis to automatically verify that bytecode programs do not overflow. All trusted components are formalized and verified in Isabelle/HOL.

We develop in complete detail an extension of Cooper's decision procedure for Presburger arithmetic that, in the positive case, returns a proof of the input formula. The algorithm is formulated as a functional program that makes only very minimal assumptions w.r.t. the underlying logical system and is therefore easily adaptable to specific theorem provers.