Logic
VU 3 WS 2005/06 LVA 703600
Description
The lecture is an introduction to formal logic and the theory of automated deduction.There are no prerequisites, but the learning curve is less step, if you have already heard Logic in Computer Science (Algorithmische Mathematik 7).
Content
| Week 1: | Introduction & Background. |
| Week 2: | Introduction to Formal Proof |
| Week 3: | Propositional Logic: Syntax & Semantics |
| Week 4: | The Replacement Theorem, Uniform Notations |
| Week 5: | Semantic Tableaux (propositional case) |
| Week 6: | Resolution (propositional case) |
| Week 7: | First-Order Logic |
| Week 8: | The Model Existence Theorem |
| Week 9: | Applications of the Model Existence Theorem |
| Week 10: | First-Order Proof Procedure & Completeness |
| Week 11: | Implementing Tableaux and Resolution |
Literature
The lecture is based on the following book:Melvin Fitting, "First-Order Logic and Automated Theorem Proving"Currently the book seems to be out of print, to remedy this, we provide copies of the first 3 chapters at the secretaries offices of the AG Computational Logic.
Springer, 2nd ed., 1996, XVII, 348 p. 15 illus., Hardcover ISBN: 0-387-94593-8.