## Automated Theorem Proving B: Advanced Proving Methods |

- Time and place: Thursday 10:15 - 11:45, HT 177F, First lecture on March 9.
- Text Book:
**Symbolic Logic and Mechanical Theorem Proving**(Academic Press, Boston, 1973) by Chin-Liang**Chang**and Richard Char-Tung**Lee** - Additional material will be provided during the lectures and on this home page.
- Prerequisites: In principle, students coming to this lecture should
have taken
*Automatic Theorem Proving A*. However, I will also accept other students provided they already have sufficient knowledge or that they are willing to study part A from the textbook. - Some material will be provided as Mathematica notebooks, which can be visualised using MathReader (free software).
- Some lectures from previous years may help you to get an idea about the contents of the course.

- Lecture 1: Mar 9:
- Motivation: the importance of automated reasoning for the design of complex systems, in particular for program verification and synthesis.
- Overview of the course:
- refinements of the resolution method,
- methods for natural style proving,
- combining automated reasoning and algebraic computations.

- Summary of the logical basis: propositional logic, predicate logic.
- Summary of the resolution method.

- Mar 16: No lecture.
- Lecture 2: Mar 23:
- Summary of natural style proving.
- Refining the resolution method.

- Lecture 3: Mar 30:
- Example of natural style proving zip file.

- Lecture 4: Apr 6:
- Examples showing the parallelism between resolution and natural style proving.
- Refining the resolution method: PI resolution.
- Example from natural style proving where a similar refinement is applied zip file.

- Apr 13: No lecture.
- Apr 20: No lecture.
- Lecture 5: Apr 27: Robert Vajda: The use of Cilindrical Algebraic Decomposition for proofs in Elementary Analysis.
- May 4: No lecture.
- Lecture 6: May 11.
- ...
- Last Lecture: June 29.
Linear resolution: Cornelius Nevrinceanu zip file.

Maintained by: Tudor Jebelean