[TU Dresden]

Theorem Proving with Equality

Technische Universität Dresden
Institut für Theoretische Informatik
Lehrstuhl für Automatentheorie

Dr. Barbara Morawska

Course Description

The aim of this lecture is to review the fundamental techniques in the automated theorem proving in the first order logic with equality predicate. We will study completeness of various inference systems starting with Resolution, Ordered Resolution, Paramodulation and Superposition, i.e. saturation-based theorem provers. The main method of proving completeness, which we will use and study, is model generation and reduction of minimal counterexamples.

Prerequisites: an acquaintance with the basics of propositional and first-order logic is expected. We will also refer to the notions from the Term Rewriting Systems.


The lectures take place in room E005 every Friday, 14:50 - 16:20.

Course Material

A script of the lecture is not available and students are strongly recommended to copy what is written on the blackboard. There will be tutorials every other Friday (strating on 19.10) following the lecture. We will discuss solutions for the exercises assigned during lectures.


Credits / Examinations

Computational logic students can earn 5 credits by attending this lecture. The lecture can be used in the module TCSL and PI.
In order to get the credits, CL students have to submit the assignments and pass an oral examination at the end of the term.


Barbara Morawska