After successful completion of the course, students are able to learn new ,methods in Automated Deduction and Proof Theory and to apply new techniques. Moreover, the students will gather new knowledge in the area of inductive inference
Inductive structures and schemata. Automated analysis of inductive proofs, schematic cut-elimination, refutation of formula schemata. Schematic CERES-method, Herbrand systems, schematic unification.
The methods applied in this course are of deductive nature. In particular, methods of mathematical logic are applied to problems in automated deduction.
Grading in this course is based on two talks to be given in the seminar and on participation.
Not necessary
Firm knowledge in Mathematical Logic, basics in Automated Deduction
