Email Gateway (Aug 18 2022 at 11:29): Email Gateway (Aug 18 2022 at 11:29):From: Tobias Nipkow <nipkow@in.tum.de>
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).
http://www.in.tum.de/~nipkow/pubs/lqe.html
This paper documents the NNF-based methods in the AFP-article
Quantifier Elimination for Linear Arithmetic
that I announced recently.
Enjoy,
Tobias
Last updated: Jan 04 2025 at 20:18 UTC