Automated Reasoning: Past Story and New Trends

Abstract

We overview the development of first-order automated reasoning systems starting from their early years. Based on the analysis of current and potential applications of such systems, we also try to predict new trends in first-order automated reasoning. Our presentation will be centered around two main motives: efficiency and usefulness for existing and future potential applications. This paper expresses the views of the author on past, present, and future of theorem proving in first-order logic gained during ten years of working on the development, implementation, and applications of the theorem prover Vampire, see [Riazanov and Voronkov, 2002a]. It reflects our recent experience with applications of Vampire in verification, proof assistants, theorem proving, and semantic Web, as well as the analysis of future potential applications. 1 Theorem Proving in First-Order Logic The idea of automatic theorem proving has a long history both in mathematics and computer science. For a long time, it was believed by many that hard theorems in mathematics can be proved in a completely automatic way, using the ability of computers to perform fast combinatorial calculations. The very first experiments in automated theorem proving have shown that the purely combinatorial methods of proving firstorder theorems are too week even for proving theorems regarded as relatively easy by mathematicians. Provability in first-order logic is a very hard combinatorial problem. First-order logic is undecidable, which means that there is no terminating procedure checking provability of formulas. There are decidable classes of first-order formulas but formulas of these classes do not often arise in applications. Due to undecidability, very short formulas may turn out to be extremely complex, while very long ones rather easy. Sometimes first-order provers find proofs consisting of several thousand steps in a few seconds, but sometimes it takes hours to find a ten-step proof. The theory of first-order reasoning is centered around the completeness theorems while in practice completeness is often not an issue due to the intrinsic * Partially supported by a grant from EPSRC.