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: May 03 2024 at 12:27 UTC