Lehrveranstaltungsleiter: Alexander Leitsch
Diese Lehrveranstaltung ist ein Wahlfach in den Magisterstudien Computational Intelligence und Intelligente Systeme.
This course also belongs to the modules Logical Foundations and Principles of Inference of the international Master Programme in Computational Logic.
Time and Place:
Thursday, 16:00 - 20:00
dates: May 5, May 12, May 19, May 26, June 9, June 16
Seminar Room Gödel, Favoritenstrasse 9, ground floor
begin: May 5, 2011.
Basic Principles of Automated Deduction
Automated Deduction, i.e. the automated construction of proofs for mathematical theorems, is a key discipline in Computational Logic and Artificial Intelligence; its applications range from mathematics (computer aided proof construction of nontrivial proofs) to logic (cut-elimination) and computer science (program verification). In this course we present the theoretical principles of automated deduction and show how to use automated theorem provers in practice. The presented topics are: transformation to normal form, unification, the resolution principle, semantic trees, completeness of the resolution principle, refinements, resolution as decision procedures, subsumption and paramodulation. In parallel to the theoretical program the students are invited to work with the theorem proving program Prover9 and to investigate practical problems of automated deduction.