History and Prospects for First-Order Automated Deduction

被引：17
作者：
Plaisted, David A. [1 ]
机构：
[1] Univ N Carolina, Dept Comp Sci, Chapel Hill, NC 27599 USA
来源：
AUTOMATED DEDUCTION - CADE-25 | 2015年 / 9195卷
关键词：
First-order logic; Resolution; Theorem proving; Instance-based methods; Model-based reasoning; Goal-sensitivity; Search space sizes; Term rewriting; Complexity; THEOREM PROVER;
D O I：
10.1007/978-3-319-21401-6_1
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
On the fiftieth anniversary of the appearance of Robinson's resolution paper [57], it is appropriate to consider the history and status of theorem proving, as well as its possible future directions. Here we discuss the history of first-order theorem proving both before and after 1965, with some personal reflections. We then generalize model-based reasoning to first-order provers, and discuss what it means for a prover to be goal sensitive. We also present a way to analyze asymptotically the size of the search space of a first-order prover in terms of the size of a minimal unsatisfiable set of ground instances of a set of first-order clauses.
引用
收藏
页码：3 / 28
页数：26
相关论文
共 68 条
  • [1] THEOREM-PROVING VIA GENERAL MATINGS
    ANDREWS, PB
    [J]. JOURNAL OF THE ACM, 1981, 28 (02) : 193 - 214
  • [2] [Anonymous], 1963, COMPUT THOUGHT
  • [3] [Anonymous], 1997, EFFICIENCY THEOREM P
  • [4] Bachmair L., 1989, Rewriting Techniques and Applications. 3rd International Conference, RTA-89. Proceedings, P15
  • [5] BALLANTYNE A, 1982, MACH INTELL, V10, P3
  • [6] The model evolution calculus as a first-order DPLL method
    Baumgartner, Peter
    Tinelli, Cesare
    [J]. ARTIFICIAL INTELLIGENCE, 2008, 172 (4-5) : 591 - 632
  • [7] Instance Based Methods-A Brief Overview
    Baumgartner, Peter
    Thorstensen, Evgenij
    [J]. KUNSTLICHE INTELLIGENZ, 2010, 24 (01): : 35 - 42
  • [8] Bibel W., 1982, AUTOMATED THEOREM PR
  • [9] Billon J., 1996, Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Springer-Verlag, P110
  • [10] Bledsoe W. W., 1984, CONT MATH
1234567