Reflecting Quantifier Elimination for Linear Arithmetic
Reflecting Quantifier Elimination for Linear Arithmetic
复制标题
线性算术的反射量词消除
DOI：
10.1007/978-1-4020-6324-4
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
T. Nipkow
本文形式化并验证了在定理证明器Isabelle/HOL中，稠密线性序和真实的及整数线性运算的量词消去过程。它是一种反射形式化，因为它可以应用于HOL公式本身。特别是，我们得到验证可执行的线性算术决策程序。各种理论的形式化是模块化的帮助下，区域设置，结构设施在伊莎贝尔。
This paper formalizes and verifies quantifier elimination procedures for dense linear orders and for real and integer linear arithmetic in the theorem prover Isabelle/HOL. It is a reflective formalization because it can be applied to HOL formulae themselves. In particular we obtain verified executable decision procedures for linear arithmetic. The formalization for the various theories is modularized with the help of locales, a structuring facility in Isabelle.