ATP 1

Automated Theorem Proving 1

Winter Semester 2009

First lecture on Wed 14 Oct 8:30 - 10:00 HT 177F

The course is an introduction to automated reasoning for students in Computer Science and Mathematics: atp.pdf. Useful reading:

This material is copyrighted and is available only for the students of this lecture and only for the purpose of study related to it.

For viewing the Mathematica notebooks one may use the Mathematica Player (free of charge),

Users of Mathematica can download the Theorema system in order to try out the examples.

A version of propositional logic used for the verification of the propositional prover of Theorema propositional.pdf.

A case study in using level saturation in natural style proving: Case-Study-Irrationality.nb, proof version 0, proof version 1, proof version 2.

Lectures

• Oct. 14: Lecture 1:
• The role of Automatic Reasoning in contemporary technology.
• Demo of the Theorema system.

• Oct. 21: Lecture 2:
• Propositional Logic: syntax and semantics.
• Equivalences, proving by rewriting, normal forms.

• Oct. 28: Lecture 3:

• Nov. 4: Lecture 4:
• The resolution principle.

• Nov. 11: Lecture 5:
• The resolution principle.

• Nov. 18: Lecture 6:
• The DPLL method for SAT solving.

• Nov. 25: Lecture 7:

• Dec. 2: Lecture 8:
• First order predicate logic: overview and examples.
• Top down truth evaluation using modified assignments.

• Dec. 9: Lecture 9:
• Semantical based notions in predicate logic: validity, equivalence, etc.
• Interesting equivalences and proofs by rewriting.
• Normal forms: prenex, Skolem, CNF, standard.

• Jan 13: Lecture 10:
• Herbrand Universe and Herbrand interpretations.
• The Herbrand Theorem.

• Jan 20: Lecture 11:
• Overview of the material.
• Substitutions, unification, resolution.

• Jan 26, 17:00 - 18:30: Consultations

• Jan 27: Examination

T. Jebelean