Program outline
Week 1
Fundamentals of Metalogic- Metatheory of classical first-order logic, including completeness theorem
- Basics of proof theory
- Model theory
- Kripke models, Hilbert calculi, Frame correspondences
- Tableaux-based decisions procedures
- Propositional linear temporal logic
- Automated propositional theorem proving
- Automated first-order theorem proving
- Reasoning with arithmetic constraints by quantifier elimination
- Basics of EL, completeness, automation
- Unification and term rewriting
- Knuth-Bendix completion
- Discrete event systems in artificial intelligence
- Solution methods for DES problems
Week 2
Computability and Incompleteness- Computability, recursiveness, Turing machines
- Diagonalisation
- Peano Arithmetic and Goedel numbering
- Undecidability of first-order logic
- Incompleteness of Peano Arithmetic
- Simply typed lambda calculus
- Higher-order intuitionistic logic and unification
- Goal-directed proof search
- Modules and abstraction in higher-order LP
- lambda-Prolog
- Non-classical logics for natural language
- Lambda calculus, Curry-Howard correspondence
- Entailment in natural language systems
- Probability calculus and Bayesian networks
- Traditional methods of probabilistic inference
- Inference by logical encoding and compilation
- Substructural proof theory
- Model theory of some non-classical systems
- Topics in the philosophy of logic
