Linear quantifier elimination

被引：0
作者：
Nipkow, Tobias [1 ]
机构：
[1] Tech Univ Munich, Inst Informat, D-8000 Munich, Germany
来源：
AUTOMATED REASONING, PROCEEDINGS | 2008年 / 5195卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This paper presents verified quantifier elimination procedures for (tense 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).
引用
收藏
页码：18 / 33
页数：16
相关论文
共 19 条
  • [1] Ballarin C, 2006, LECT NOTES ARTIF INT, V4108, P31
  • [2] Boyer R. S., 1981, CORRECTNESS PROBLEM, P103
  • [3] Verifying and reflecting quantifier elimination for Presburger arithmetic
    Chaieb, A
    Nipkow, T
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 367 - 380
  • [4] Chaieb A, 2006, LECT NOTES ARTIF INT, V4130, P528
  • [5] Cooper D. C., 1972, Machine intelligence 7, P91
  • [6] Ferrante J., 1975, SIAM Journal on Computing, V4, P69, DOI 10.1137/0204006
  • [7] GONTHIER G, COMPUTER CHECKED PRO
  • [8] Haftmann F, 2007, LECT NOTES COMPUT SC, V4502, P160
  • [9] HARRISON J, INTRO LOGIC IN PRESS
  • [10] HARRISON J, 2001, LNCS, V2152, P159
12