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