Revised Syllabus for CS3AUR: Automated Reasoning 2002
=====================================================

Introduction
- What is Automated Reasoning?
- Examples for Applications
- History of Automated Reasoning

First-order Logic Review
- Syntax and Semantics of FOL
- Models
- Satisfiability, Validity and Consequence

Automated Deduction with KE
- KE Rules for FOL
- Improvements: Analytic PB and Beta Simplification
- Undecidability and the Gamma Rule
- Saturated Branches and Countermodels
- Smullyan's Uniform Notation
- Soundness and Completeness of KE

Unification
- Unifiers and MGUs
- Robinson's Unification Algorithm

Automated Deduction with Smullyan Tableaux
- Tableaux Rules for FOL
- Comparison with KE
- Free-variable Tableaux for FOL

Automated Deduction with Resolution
- Prenex Normal Form
- Skolemisation
- Binary Resolution with Factoring for FOL
- Horn Clauses
- SLD Resolution for Horn Clauses
- Foundations of Logic Programming

Reasoning with Temporal Constraints
- Allen's Interval Relations
- Temporal Constraint Networks
- Constraint Propagation

Knowledge Representation and Description Logics
- Logic-based Knowledge Representation
- Description Logic ALC: Syntax and Semantics
- TBoxes and ABoxes
- Common Reasoning Services of DL Systems
- Tableaux for ALC ABoxes
- Soundness, Completeness and Termination of ALC Tableaux
- Standard Translation

Implementing Automated Reasoning Systems
- Mini Projects

-----------------------------------------------------------

The Bigger Picture
==================

By following this course you will also find answers to
the following (somewhat more general) questions.

> Why is Automated Deduction so useful?

Because logic is such a powerful representation formalism.

> Why is Automated Deduction so difficult?

Because the complexity of problems can be very high. 
FOL is even undecidable.

> Why are there so many different reasoning methods around?

Because of the aforementioned  difficulties. Different 
methods perform differently on different problems. 

> Why do we have to formally prove properties like 
> soundness and completeness?

Because we have to make sure that our algorithms really 
compute what they have been designed for.

> What (non-mechanical) techniques are there to prove 
> mathematical theorems?

For example:
 - Proof by case analysis
 - Proof by contradiction 
 - Proof by contraposition
 - Proof by (structural) induction 
 - Constructive proofs

> Is that all?

No. There's much more out there!

-----------------------------------------------------------