[isabelle] New paper: Linear Quantifier Elimination

I would like to announce the new paper

 Linear Quantifier Elimination
 Tobias Nipkow

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