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.
CITATION STYLE
Plaisted, D. A. (2015). History and prospects for first-order automated deduction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9195, pp. 3–28). Springer Verlag. https://doi.org/10.1007/978-3-319-21401-6_1
Mendeley helps you to discover research relevant for your work.