**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:

- Theorema demo (gzipped directory with Mathematica notebooks).
- demo propositional logic (Mathematica notebook).

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**:- Normal forms. Logical consequence. ATP-I-2009-10-28.pdf.

**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**:- First order predicate logic ATP-I-2009-11-25.pdf.

**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