Skip Navigation LSS Home | CECS Home | ANU Home | Search ANU | HORUS | Staff Home

Printer friendly

Program Outline

Week 1

Week2

Fundamentals of Metalogic Metatheory of classical first-order logic, including completeness theorem Basics of proof theory Model theory Introduction to Modal and Temporal Logic Kripke models, Hilbert calculi, Frame correspondences Tableaux-based decisions procedures Propositional linear-time temporal logic Overview of Automated Reasoning Automated propositional theorem proving Automated first-order theorem proving Reasoning with arithmetic constraints by quantifier elimination Computability and Incompleteness Computability, recursive functions and Turing machines Diagonalisation Peano Arithmetic and Goedel numbering Undecidability of first-order logic Incompleteness of Peano Arithmetic

Logic and Complexity Turing machines (again) Basic complexity classes NP and PSPACE Relating complexity and logic Programming in Higher-Order Logic Simply typed lambda calculus Higher-order intuitionistic logic Higher-order unification Goal-directed proof search Modules and abstraction in higher-order logic programming lambda-Prolog Programming examples Answer Set Programming: The KRR* solving paradigm Answer set programming Knowledge representation and reasoning Boolean constraint solving Logic programming Reasoning in Discrete Event Systems Discrete event systems in artificial intelligence Solution methods for DES problems Non-Classical Logic TBA