[isabelle] New paper: Linear Quantifier Elimination
I would like to announce the new paper
Linear Quantifier Elimination
This paper presents verified quantifier elimination procedures for dense
linear orders (DLO), for real and for integer linear arithmetic. The DLO
procedures are new. All procedures are defined and verified in the
theorem prover Isabelle/HOL, are executable and can be applied to HOL
formulae themselves (by reflection).
This paper documents the NNF-based methods in the AFP-article
Quantifier Elimination for Linear Arithmetic
that I announced recently.
This archive was generated by a fusion of
Pipermail (Mailman edition) and