Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL

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.

• Type: Conference
• Year: 2008
• Where: AISC
• Authors: Amine Chaieb
• Keywords: AISC 2008, Artificial Intelligence, Axiomatic Type Classes, Procedure Generalizes Ferrante, Quantifier Elimination Procedure