Sciweavers

AISC
2008
Springer

Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL

13 years 5 months ago
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.
Amine Chaieb
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where AISC
Authors Amine Chaieb
Comments (0)