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