Verifying and reflecting quantifier elimination for Presburger arithmetic

被引：15

作者：

Chaieb, A ^{[1
]}

Nipkow, T ^{[1
]}

机构：

[1] Tech Univ Munich, Inst Informat, D-8000 Munich, Germany

来源：

LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS | 2005年 / 3835卷

关键词：

D O I：

10.1007/11591191_26

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present an implementation and verification in higherorder 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.

引用

页码：367 / 380

页数：14

共 18 条

[1] [Anonymous], CRC053 SRI CAMBR
[2] Dependent types ensure partial correctness of theorem provers
Appel, AW
Felty, AP
[J]. JOURNAL OF FUNCTIONAL PROGRAMMING, 2004, 14 : 3 - 19
[3] Berghofer S, 2000, LECT NOTES COMPUT SC, V1869, P38
[4] Berghofer S., 2002, LNCS, V2277, P24
[5] CHAIEB A, 2003, GENERIC PROOF SYNTHE
[6] Cooper D. C., 1972, Machine intelligence 7, P91
[7] CREGUT P, 2004, 15 JOURN FRANC LANG
[8] FISCHER, 1974, SIAMAMS COMPL COMP P
[9] GREGOIRE B, 2002, INT C FUNCT PROGR 20, P235
[10] GREGOIRE B, 2005, LNCS

← 1 2 →