Course descriptions

Fundamentals of metalogic

Content: Completeness theorems, Model theory and proof theory.

Course description: This course provides an introduction to the metatheory of elementary logic. Following a "refresher" on the basics of notation and the use of classical logic as a representation language, we concentrate on the twin notions of models and proof. An axiomatic system of first order logic is introduced and proved complete for the standard semantics, and then we give a very brief overview of the basic concepts of proof theory and of formal set theory. The material in this course is presupposed by other courses in the Summer School, which is why it is presented first.

Pre-requisites: it is assumed that students are at least familiar with logical notation for connectives and quantifiers, and can manipulate truth tables, some kind of proof system or semantic tableaux or the like. Normally they will have done a first logic course at tertiary level. Some basic mathematical competence is also presupposed, to be comfortable with the notion of a formal language, follow proofs by induction, be familiar with standard set-theoretic notation and the like.

Lecturer: John Slaney is the founder and convenor of the Logic Summer school. He originated in England, ever so long ago, and discovered Australia in 1977. Undeterred by the fact that it had apparently been discovered before, he gradually moved here, joining the Automated Reasoning Project in 1988 on a three-year contract because he could not think of anywhere better to be a logician. He is still here and still can't. His research interests pretty much cover the waterfront, including non-classical logics, automated deduction and all sorts of logic-based AI. He was formerly the leader of the Logic and Computation group at the ANU, and of the NICTA program of the same name.

Introduction to modal logic

Content: Kripke models, Hilbert calculi, Frame correspondences, Tableaux-based decisions procedures and Propositional linear temporal logic

Course description: We cover the syntax, Kripke semantics, correspondence theory and tableaux-style proof theory of propositional modal and temporal logics. These logics have important applications in a diverse range of fields incuding Artificial Intelligence, Theoretical Computer Science and Hybrid Systems.

Pre-requisites: You should have a good grounding in classical propositional and first-order logic, including material covered in the "Fundamentals of Metalogic" course. Some very basic notions from graph theory would also be useful, but are not essential.

Lecturer: Rajeev Gore is currently a a Senior Fellow in the ANU, and leader of the Logic and Computation research group. He was an Australian Research Council Queen Elizabeth II Fellow at the ANU from 1997-2001, a Research Fellow at the ANU from 1994-1996, and a Research Associate at the University of Manchester from 1992-1993. He obtained his PhD in Modal Theorem Proving from the University of Cambridge in 1992.

Overview of automated reasoning

Content: Automated propositional theorem proving; automated first-order theorem proving; Interactive theorem proving

Course description: In many applications, we expect computers to reason logically. We might naively expect this to be what computers are good at, but in fact they find it extremely difficult. In this overview course, we look at various methods to automate logical reasoning, which are needed to support a variety of application domains.

Automated reasoning procedures are parametrized by the logic they are capable of reasoning with. We distinguish between propositional logic and first-order logic. Development and application of propositional logic procedures, also called SAT solvers, received considerable attention in the last ten years, e.g., for solving constraint satisfaction problems, applications in hardware design, verification, and planning and scheduling. Regarding automated deduction in first-order logic, we discuss applications, standard deductive procedures such as resolution, and basic concepts, such as unification. We also examine the dual problem of theorem proving, viz., generating models of a given theory, which has applications to finding counterexamples for non-theorems, and we provide an overview of some recent trends (instance-based methods, satisfiability modulo theories). Finally, we describe in some depth so-called quantifier elimination methods for theorem proving in decidable fragments of arithmetics over the reals and the integers.

Pre-requisites: Elementary logic, as provided by the "Fundamentals of Metalogic" course of this Summer School.

Lecturer: Peter Baumgartner is a Principal Researcher in Software Systems in the Canberra Laboratory of NICTA, where he was formerly the lab manager of the "Managing Complexity" theme. Previous employments were at the Max Planck Institute for Computer Science and the University of Koblenz, both in Germany. His research interest is automated deduction, particularly for first-order logic, and its applications. He holds a PhD and a Habilitation degree in Computer Science.

Equational Logic and Term Rewriting

Contents: Equational logic; Syntactic Unification; Term rewriting.

Course description: Equational logic has only one logical connective: the equals sign. This may seem rather basic, but in fact equational logic is interesting enough to underly an entire field of mathematics (universal algebra), and equational reasoning is undecidable in general. We will introduce the syntax and semantics of equational logic, and demonstrate the completeness of Birkhoff's proof rules, as well as the more succinct proofs by chain derivation. We will look at the automated equational theorem prover Prover9 and counterexample generator Mace4, which have discovered solutions to real open problems in mathematics.

After a brief detour into syntactic unification, we will ask whether there are good general purpose techniques for equational reasoning. This will lead us to term rewriting, where we replace our equals signs by arrows (also called directed equations), and hence turn our logical theories into nondeterministic programs. Basic concepts of term rewriting such as termination, confluence and critical pairs will be covered, and we will see how reduction orders and Knuth-Bendix completion can help us turn some equational theories into equally powerful, but more useable, term rewriting systems. Finally, we will glimpse some advanced topics in the area, including ways to cope with some equational theories that are not amenable to the conventional term rewriting approach.

Pre-requisites: Some abstract algebra (groups, rings and fields) would be a bonus but is not essential.

Background reading: Stanley N. Burris, Logic for Mathematics and Computer Science; or Franz Baader and Tobias Nipkow, Term Rewriting and All That.

Lecturer: Ranald Clouston is a postdoctoral research fellow with the Logic and Computation group at the Australian National University's Research School of Computer Science. Originally a student at Victoria University of Wellington, he completed a PhD at the University of Cambridge, where he co-developed Nominal Equational Logic, an extension of equational logic to deal with side conditions concerning free and bound names. His research interests continue to revolve around the application of logic, particularly equational logic, to the problems of names in computing. He attended the Logic Summer School as a student in 2003.

Reasoning in discrete event systems

Contents: logical reasoning about transition systems; planning; solution techniques.

Course description: Reasoning about discrete state/transition systems is common to many problems in AI, such as diagnosis and planning, as well as in other areas of computer science (e.g., model checking or parsing). This course is intended to give a basic introduction to some of these problems, show how they are related and describe some of the methods that can be used to solve them.

Lecturer: Patrik Haslum is a research fellow at the Australian National University. He did his PhD at Linkoping University and did a post-doc with NICTA (in Canberra). His research has focused mainly on heuristic search methods for optimal planning.

Computability and incompleteness

Contents: Computability; recursive Functions and Turing machines; diagonalisation; Peano arithmetic and Gödel numbering; undecidability of first-order logic; incompleteness of Peano arithmetic.

Course Description: We begin with two formal accounts of the intuitive notion of computability: recursive functions and Turing machines. They turn out to be the same, hence Church's Thesis: functions that can be computed by any means are precisely the partial recursive functions. Then we revisit the old Cretan who says that all Cretans always lie, and other forms of diagonalisation argument such as Halting Problem. Next we look at an axiomatic theory of arithmetic, known as Peano Arithmetic (PA), and show how we can represent all recursive functions in PA. This will lead to Goedel numbering: a neat trick enabling us to effectively encode notions like "theorem", "proof" and "provability in PA" within PA itself. We spend a while discussing Diagonalisation Lemma and Derivability Conditions. Finally, in one fell swoop we prove undecidability of first-order logic (Church's Theorem), undefinability of truth (Tarski's Theorem), incompleteness of PA given consistency of PA (First Goedel's Theorem) and unprovability of consistency of PA given consistency of PA (Second Goedel's Theorem).

Pre-requisites: Foundations of first-order logic

Background reading: G. Boolos and R. Jeffrey, Computability and Logic.

Lecturer: Michael Norrish is a Senior Researcher in NICTA's Canberra Laboratory. He is originally from Wellington, New Zealand, and is very happy to be back in the southern hemisphere, after an extended stint in Cambridge, England. It was there that he did his PhD, and then spent three years as a research fellow at St. Catharine's College. His research interests are in interactive theorem-proving, and the application of this technology to areas of theoretical computer science, particularly the semantics of programming languages.

Programming in higher-order logic

Contents: 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.

Course description: In this course we examine the use of logic as a programming language. Logic programming, in its commonly known manifestation in the Prolog language, uses only a simple fragment of first-order logic, i.e., the Horn fragment. There has been an active research area, called "abstract logic programming", that broadens the scope of logic programming beyond Horn clauses. Underlying this notion of abstract logic programming is the equation:

Computation = Proof Search.

More specifically, computation is modelled as a certain kind of complete proof search strategy, called goal-directed proof search. A wide range of proof systems, e.g., sequent calculi for intuitionistic logic, fragments of classical logic and various fragments of linear logic, have been shown to be complete under this notion of goal-directed proof search. In this course, we will examine the notion of goal-directed proof search in a sequent calculus for higher-order intuitionistic logic, and a logic programming language, called lambda-Prolog, that arises from a fragment of higher-order logic under this notion of goal-directed proof search. In particular, we will see that certain notions in programming languages, i.e., modules and abstract datatypes, arise naturally from the behaviors of logical connectives. A wide range of examples of lambda-Prolog programs which exploit the higher-order features of the language will be presented, e.g., we will look at an encoding of a lazy data structure (streams) using higher-order prediates, and an implementation of an interpreter for a mini functional language in lambda-Prolog.

Pre-requisites: It is assumed that students are familiar with first-order logic and sequent calculus, which are covered in the first week of the summer school. Some familiarity with lambda calculus will be helpful but not neccessary, as a brief overview will be given in the first lecture. Familiarity with Prolog and logic programming in general will also be helpful.

Lecturer: Alwen Tiu is a research fellow at the Australian National University since 2006. He did his PhD at the Pennsylvania State University from 2001 - 2004, but he spent the last two years of his PhD at Ecole Polytechnique, France. Prior joining ANU, he spent one year at LORIA (France) as a postdoc. His research interests include proof theory, logical frameworks, process calculi and theorem proving.

Logic and Natural Language Semantics

Contents: Non-classical logics for natural language analysis; Formal semantics, lambda calculus and the Curry-Howard correspondence; Lambek calculis; Entailment in natural language systems.

Course Description: We will present logics weaker (or at least not stronger) than classical logic, namely substructural logics, i.e., logics whose Gentzen calculi lack some (zero or more) of the three structural rules, namely: weakening, exchange or contraction. In particular, we will see them at work by taking natural language as a case study.

We will look at how their expressivity increases by starting from the minimum logic of residuation, non associative Lambek calculus, and move to some extensions of it by adding structural rules. By focusing on this application, we will introduce the lambda-calculus and its Curry-Howard Correspondence with the Lambek Calculi. Some basic concept of Formal Semantics of Natural Language will be provided too. The main goal of this first part will be to show how algebraic semantics can be used as a unifying framework for studying substructural logics, and how these logics can be applied to other fields, such as Linguistics.

We will then end the course by giving a look at applications of the logic view to natural language semantics within language technology systems, like those for Question Answering or Textual Entailment. By looking at these applications, we will highlight some strengths and weakness of the logic view and introduce a complementary analysis of natural language semantics, called Distributional Semantics, showing how Logic and Distributional Models can be combined to better capture the analysis of natural language semantics.

Pre-requisites: Basic background on propositional logic is required. Some knowledge of model and proof theory may be useful.

Lecturer: Rafaella Bernardi is an Assistant Professor at the University of Trento, Italy. Her main research interest is in the area where formal logic intersects natural language analysis. She has worked on this both from the perspective of non-classical logical theory and from the more practical concerns of natural language interfaces to ontologies and databases. She has taught in the Logic Summer School before, in 2005.

Logic-based Probabilistic Reasoning

Contents: Probability calculus and Bayesian networks; traditional methods of probabilistic inference; inference by logical encoding and compilation

Course description: Bayesian networks are an important tool for representing probability distributions and reasoning about probabilistic beliefs.We review traditional reasoning methods, including variable elimination and jointree algorithms, whose complexity is exponential in the treewidth of the network, and then discuss a recent technique based on encoding Bayesian networks into formulas in propositional logic and compiling the formulas into circuits with specific properties. We show how the new technique can escape the complexity bound based on treewidth, allowing many problems to be solved for the first time.

Lecturer: Jinbo Huang is a senior researcher at NICTA and adjunct Fellow of the Australian National University. He did his PhD at UCLA and joined NICTA immediately afterwards. His research interests include logical and probabilistic reasoning and their applications, and artificial intelligence in general.

Non-classical logic

Contents: Substructural proof theory; the Routley-Meyer semantics; philosophical reflections

Course description: Rather than attempt an overview of all of non-classical logic, we concentrate on systems differing from classical logic (mainly) in that the rules about how proof is structured are weakened. We look at a range of such "substructural" logics and their close relatives both from the standpoint of deduction and in terms of their semantics. We also explore both technical and philosophical issues arising from the various non-classical viewpoints.

Lecturers: John Slaney is the same guy who spoke the truth about orthodox classical logic in the first week. By the second week, he is fed up with orthodoxy and reveals his non-classical colours.