---
title: "Automated Reasoning: Past Story and New Trends"
authors:
  - "Andrei Voronkov"
doi: ""
url: "https://ijcai.org/proceedings/2003/281"
pdf: "https://ijcai.org/proceedings/2003/0281.pdf"
venue: "Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence"
year: 2003
pages: "1607-1611"
track: ""
keywords:
---

# Automated Reasoning: Past Story and New Trends

Andrei Voronkov

*Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence*, pages 1607-1611.

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