Automatic Theorem Proving
Time and place: Thursday 10:00 - 11:30, 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: February 23, 1999
[
Up
] [
RISC-Linz
] [
University
] [
Search
]
