zbMATH — the first resource for mathematics

History and prospects for first-order automated deduction. (English) Zbl 1465.03055
Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 3-28 (2015).
Summary: On the fiftieth anniversary of the appearance of J. A. Robinson’s resolution paper [J. Assoc. Comput. Mach. 12, 23–41 (1965; Zbl 0139.12303)], 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.
For the entire collection see [Zbl 1316.68011].

03B35 Mechanization of proofs and logical operations
03-03 History of mathematical logic and foundations
68-03 History of computer science
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.