## Automatic Theorem Proving |

- Time and place: Friday 8:15 - 9:45, K 123A
- Text Book:
**Symbolic Logic and Mechanical Theorem Proving**(Academic Press, Boston, 1973)by Chin-Liang

**Chang**and Richard Char-Tung**Lee**Chapters 1-5 and part of Chapters 6-9.

- Contents:
- The Propositional Logic
- The First Order Logic
- Herbrand's Theorem
- The Resolution Principle
- Semantic Resolution and Lock Resolution
- Linear Resolution
- The Equality Relation
- Some Proof Procedures based on Herbrand's Theorem

- Homework: 5 sets of exercises will be assigned which amount to 20% of the final grade.
- Exam: There will be a final written exam (without books and notes), at the end of the semester.

Maintained by: Tudor Jebelean

Last Modification: March 7, 1997

[Up] [RISC-Linz] [University] [Search]