Theorem Proving and Equality
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 lecture takes place in room GRU 359: Friday 11:10-12:40.
The next lecture will take place in room GRU 359: Tuesday (10.01.2006) 11:10-12:40.
There is no exercise group, though some (voluntary) exercises are given in the lecture.
Some slides used in the lecture will be available here.
Computational logic students can earn 3 credits by attending this lecture. The lecture can be used in the module TCSL and IT. In order to get the credits, CL students have to pass a short oral examination at the end of the term.