Automated Reasoning
Course at TFCS 2019, Winter School on Theoretical Foundations of Computer Science
February 4–9, 2019. Tbilisi, Georgia.

Summary Slides Literature Lecturer

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.


Literature, used materials

Temur Kutsia
Research Institute for Symbolic Computation
Johannes Kepler University Linz

Back to the teaching page