Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
复制标题
验证和反思Presburger算术的量词消除
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
Amine Chaieb;T. Nipkow
给出了Presburger算法中库珀量词消去的高阶逻辑实现和验证。反射，即ML中的直接执行，比LCF风格的实现速度提高了200倍，并且表现得与ML中手工编码的决策过程一样好。
We present an implementation and verification in higher-order logic of Cooper’s quantifier elimination for Presburger arithmetic. Reflection, i.e. the direct execution in ML, yields a speed-up of a factor of 200 over an LCF-style implementation and performs as well as a decision procedure hand-coded in ML.