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!
-----------------------------------------------------------