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 条

[11] NON-RESOLUTION THEOREM PROVING
BLEDSOE, WW
[J]. ARTIFICIAL INTELLIGENCE, 1977, 9 (01) : 1 - 35
[12] Bonacina M.P., 2014, P 4 WORKSH PRACT ASP
[13] Bonacina M.P., 2015, LNCS, V9200
[14] Claessen K., 2005, DAGST SEM DED APPL
[15] A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY
DAVIS, M
PUTNAM, H
[J]. JOURNAL OF THE ACM, 1960, 7 (03) : 201 - 215
[16] A MACHINE PROGRAM FOR THEOREM-PROVING
DAVIS, M
LOGEMANN, G
LOVELAND, D
[J]. COMMUNICATIONS OF THE ACM, 1962, 5 (07) : 394 - 397
[17] Davis M., 1963, Proceedings of Symposia in Applied Math, V15, P15
[18] ORDERINGS FOR TERM-REWRITING SYSTEMS
DERSHOWITZ, N
[J]. THEORETICAL COMPUTER SCIENCE, 1982, 17 (03) : 279 - 301
[19] Upper bounds on the satisfiability threshold
Dubois, O
[J]. THEORETICAL COMPUTER SCIENCE, 2001, 265 (1-2) : 187 - 197
[20] Feldman J, 1963, COMPUT THOUGHT

← 1 2 3 4 5 6 7 →