期刊
AUTOMATED DEDUCTION - CADE-25
卷 9195, 期 -, 页码 3-28出版社
SPRINGER-VERLAG BERLIN
DOI: 10.1007/978-3-319-21401-6_1
关键词
First-order logic; Resolution; Theorem proving; Instance-based methods; Model-based reasoning; Goal-sensitivity; Search space sizes; Term rewriting; Complexity
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据