|AI Speakers >>||
Logic Speakers >>
|Machine Learning Speakers >>|
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 an 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. Students without that much background are advised to study an introductory logic textbook (of which there are many, mostly called something like "Introduction to Logic") before the start of the Summer School.
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 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. Currently, he leads the Logic and Computation group at the ANU, and was formerly the leader of the NICTA program of the same name."
Content: Kripke models, Hilbert calculi, Frame correspondences, Tableaux-based decisions procedures and Propositional linear-time 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. Some very basic notions from graph theory would also be useful, but are not essential.
Background Reading: Complete beginners may find it useful to read "An Introduction to Classical Propositional Logic: Syntax, Semantics, Sequents" available from http://web.rsise.anu.edu.au/~rpg/publications.html
Rajeev Goré is a Senior Fellow in the ANU. 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.
Content: Automated propositional theorem proving, Automated first-order theorem proving and 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 briefly at several varieties of mechanical reasoning. The first is automated deduction, whereby conclusions are derived from assumptions purely by following an algorithm, without user intervention. Automated deduction 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. A third important area covered in the course is dealing with interactive theorem proving. Interactive theorem proving requires certain amount of instructions from the user to tell the proving program (the theorem prover) how to proceed with a proof. Such interaction is required usually because of the use of higher-order logics, whose expressive formalisms allow natural modeling of complex systems, such as operating system or various protocols. A recent trend in the development of interactive proving is to improve its automation, by combining the power of automatic provers.
Pre-requisites: Elementary logic, as provided by the "Fundamentals of Metalogic" course of this Summer School.
Peter Baumgartner is a Principal Researcher and the Research Group Manager for the Managing Complexity research theme at NICTA. 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 Ph.D. and a Habilitation degree in Computer Science.
Michael Norrish is a Senior Researcher in NICTA's Managing Complexity research theme. 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.
Contents: Computability and Recursive Functions, Proof that exactly the partial recursive functions are computable, Gödel’s Incompleteness Theorems, Löb's Theorem.
Course Description: In these lectures we cover the following topics: Computability and Recursive Functions, Proof that exactly the partial recursive functions are computable, Gödel’s Incompleteness Theorems, Löb's Theorem.These very deep and very powerful results in metalogic from the 1930s were unexpected. They arose in a context in which it was expected that a finitary proof of consistency of arithmetic would shortly be forthcoming. This followed the proposal by the mathematician David Hilbert (1862-1943) for the complete axiomatisation and formalisation of all mathematical knowledge and proofs. Although committed to formal methods, many of Hilbert’s proofs were existential in nature, which ran counter to the finitistic, constructivist methods of mathematics. To deal with this criticism, Hilbert proposed that the formal methods program should establish that all of the “Ideal” existential arguments could in principle be replaced by “Real” constructive arguments, by showing some sort of conservation result. However, the incompleteness results showed that this ‘program’ could not be carried out in a simple way.
References: These notes are mainly based on the texts of Boolos and Jeffrey, and Y.I. Manin. The article by Smorynski in the Handbook of Mathematical Logic also gives a good condensed coverage. The Incompleteness Theorems are discussed in more or less detail in many logic texts.
Errol Martin took degrees in philosophy and mathematics at the University of Queensland and University of New South Wales before undertaking a Ph.D. in mathematical logic at ANU, supervised by Richard Routley and Robert K. Meyer. His thesis studied weak contraction free logics and provided the first solution of the P-W problem, showing that no instances of the implicational law of Identity can be proved in a system with just the 'syllogistic' principles of Prefixing and Suffixing. Errol has held teaching positions at the University of New South Wales, the University of Queensland, and the University of Canberra. He has held research positions at the University of Melbourne and the Australian National University. Errol was Head of the Information Systems and Computing Departments at the University of Canberra in the period 1988 -1995. From 1999 he has been a freelance consultant, providing strategic advice to government on the design of information systems.
Contents: The modal mu-calculus, Alternating tree automata, Translation of the mu-calculus into alternating tree automata, Two-player games; parity games, Alternating tree automata and parity games and Model-checking and satisfiability problems for the modal mu-calculus.
Course Description: This course provides the students with fundamental notions of temporal logic, mu-calculus, two-player infinite games, alternating tree automata, and with their relationship to answer the model-checking and satisfiability problems.
Pre-requisites: propositional logic, automata theory, basis on computational complexity.
Sophie Pinchinat (University of Rennes, France). Since September 1994, Sophie Pinchinat has been an Associate Professor in Computer Science at the University of Rennes 1 in France, and an active research partner of the IRISA research center (Institute for Computer Science and Stochastic Systems), which comprises INRIA, CNRS, University and INSA staff. From 1999 to 2001, she was seconded to INRIA as a research scientist without teaching load, while remaining at the IRISA. Sophie focused first on Programming Environments for Real-Time Applications and since 2000, on System Synthesis and Supervision Scenarios. Sophie received a Marie Curie outgoing international fellowship months at the Australian National University from August 2006 until July 2007.
Contents: Propositional dynamic logic, first-order dynamic logic for regular actions, extensions of the dynamic logic for regular actions, dynamic logic for the JavaCard programming language, the KeY verification system.
Course Description: Dynamic Logic was developed in the late 1970s by David Harel building on previous work by V.R.Pratt. It is a modal logic and as any modal logic it allows to reason about the truth of statements in different states (or worlds). It extends classical modal logic however by taking explicitly into account the transitions from one state to the next state(s). Descriptions of actions (events, or programs) are part of the syntax of Dynamic Logic. This course will start with an introduction into the logical theory of propositional and first-order dynamic logic with respect to a very fine grained notion of actions. At the next level a Dynamic Logic for an abstract programing language will be considered. We will end by presenting a Dynamic Logic for a real programming language and show how this can be used in software verification including a demo of a working system.
Pre-requisites: Knowledge of first-order and modal logic as it is taught in the first week of this summer school would be beneficial.
Background Reading:(1) D.Harel, D.Kozen, J.Tiuryn. Dynamic Logic, The MIT Press 2000
Peter H. Schmitt received his Doctorate and his Habilitation in the area of mathematical logic at the University of Heidelberg, Germany. His main research contributions are in the area of model theory. 1984 he joined IBM Deutschland GmbH. Since 1988 he holds a chair on Theoretical Computer Science at Universität Karlsruhe. His main research interest are in software verification. He is one of the leaders of the KeY project.
Contents: Intuitionist logic, substructural Logics, resource sensitivity, logics of information flow, relevant logic.
Course Description: Non-classical logics are used to characterize phenomena with which classical logic has difficulty or to represent alternative views of reasoning. Relevant logic, for example, rejects the rule of classical logic that allows us to add new premises to an already valid inference to produce another valid inference. Relevant logic, as its name suggests, demands that all the premises of a valid argument be actually relevant to the derivation of the conclusion. In contrast, a weaker form of relevant logic – linear logic – is not supposed to represent an alternative view of valid inference, but rather describe relationships between different sorts of entities than classical (or relevant logic). Traditionally, logics are thought to represent relationships between propositions but linear logic represents relationships between resources and actions. The resulting logic is quite different from traditional logics and is interestingly related to the other logics that we will study such as relevant logic. A variant of linear logic, that we will also examine, is used to study the flow of information between agents.
Pre-requisites: Some knowledge of proof theory and modal logic will be useful.
Lecturer: Edwin Mares is a professor of philosophy and a member of the Centre for Logic, Language, and Computation and Victoria University of Wellington in New Zealand. He is the author of Relevant Logic: A Philosophical Interpretation (Cambridge University Press, 2004) and (with Stuart Brock) Realism and Anti-Realism (Acumen, 2007). He is currently writing a book on quantified modal and substructural logic.
Contents: propositional logic, satisfiability, binary decision diagrams, first-order logic, modal logics
Course Description: This course provides a very basic introduction to formal logics. It is meant to provide some essential logic backgrounds to the Machine Learning students, in order to prepare them for the AI courses in the second week of this summer school. We start with the most basic logic of all, the propositional logic, and discuss some important structures and algorithms related to this logic, notably, (conjunctive/disjunctive) normal forms, satisfiability testing, and binary decision diagrams (BDD). This is then followed by an overview of first-order and modal logics, covering their syntax and semantics, and some basic theoretical results.
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.