The goal of automated reasoning is to develop methods and tools to perform logical inferences in an algorithmic way. It is used to automatically (or semi-automatically) prove theorems, verify programs, solve problems, etc. In this course we focus on automated reasoning in first-order classical logic. We discuss one of the most popular and well-studied deduction methods (resolution) and rewriting-based reasoning techniques that deal with equalities.

• Resolution theorem proving.
• Rewriting-based deduction.

.

• Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, United Kingdom, 1998.
• John Alan Robinson, Andrei Voronkov. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001.
• The TPTP Problem Library for Automated Theorem Proving. http://tptp.org/.
• Andrei Voronkov. Automated Reasoning (in First Order Logic). Course at 3rd International School on Rewriting, ISR 2008. Slides.
• Uwe Waldmann. Automated Reasoning. Course at MPI. Suggested readings.

Temur Kutsia

---

---