Lehrveranstaltungsleiter: Alexander Leitsch
Diese Lehrveranstaltung ist ein Wahlfach in den Magisterstudien Computational Intelligence und Intelligente Systeme.
This course also belongs to the foundation module Foundations
of the international Master Programme in Computational Logic.
Time and Place:
Thursday, 16:00 - 20:00
dates: April 15, April 22, April 29, May 6, May 20, May 27
Seminar Room von Neumann, Favoritenstrasse 9, ground floor
begin: April 15, 2010.
CONTENT:
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.
A.Leitsch