Automated Theorem Proving 1

First lecture: Wed, 12.Oct.2005, 8:30 - 10:00, T112.

This course presents and compares the basic methods for Automated Reasoning: the resolution method and the main methods for proving in natural style. The topics of the lecture are: syntax and semantics of logical formulae, normalization of formulae, the Herbrand Theorem, the proof method by resolution, the sequent calculus and its use in automated reasoning, basic methods for reasoning with equality. Some concrete implementations will be also presented, including the implementation in Theorema of natural style proving, as well as some applications of automated reasoning in Mathematics and Computer Science.

The main part of the lecture will be dedicated to the syntax, semantics and resolution proving in propositional and first-order predicate logic and will be based on the textbook:

Chin-Liang Chang, R. Char-Tung Lee

Symbolic logic and mechanical theorem proving.