Automated Reasoning: Past Story and New Trends

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, ...

• Type: Conference
• Year: 2003
• Where: IJCAI
• Authors: Andrei Voronkov
• Keywords: First-order Automated Reasoning, First-order Logic, IJCAI 2003, IJCAI 2007, Theorem Proving