Tutorials
Tableaux(-like) Methods for the Satisfiability Problems of Temporal Logics
Martin Lange
Temporal logics are modal logics over infinite flows of time. They form important tools for the specification of program behaviour. Their satisfiability problems therefore form the algorithmic essence of consistency checks for logical specifications of correct program behaviour.
Temporal operators usually have elegant characterisations in terms of fixpoint solutions to certain recursive equations. This often makes the evaluation of temporal formulas in Kripke structures relatively simple using fixpoint iteration techniques. It also introduces very particular difficulties for deciding satisfiability: one has to ensure that iterations corresponding to least fixpoint constructs are well-founded.
In this tutorial we will review basic temporal logics and tableau-based methods for their satisfiability problems. We will illustrate the problems arising with a mixture of least and greatest fixpoint constructs in such tableaux and discuss known solutions as well as related and open questions in this area.
The tutorial will be held at an introductory level. No particular knowledge about temporal logics will be required. However, participant will be expected to have some knowledge and logic in general. Some knowledge on automata theory will be helpful but is not essential.
Introduction to Proof Nets
Lutz Straßburger
This tutorial is intended to be a basic introduction to proof nets. The term proof net has been coined by Girard for his bureaucracy-free presentation of proofs in linear logic. He used the term bureaucracy for the phenomenon of trivial rule permutations in the sequent calculus that do not change the essence of a proof. From the beginning, proof nets served two purposes: first, provide a concise presentation of proofs, similar to lambda-terms for intuitionistic logic, and second, to simplify the cut elimination proof and to study the normalization of proofs. In the first part of the tutorial I will introduce proof nets for various fragments of linear logic and discuss various correctness criteria. In the second part of the tutorial I will present more recent developments in the area of classical logic. There are, on one side, proof nets that follow the tradition of the linear logic proof nets, and on the other side, there are proof net variants that follow the tradition of Andrews' matings, Bibel's matrix proofs, and Buss' logical flow graphs. The normalization behaviour of these objects is very different from the usual one in the sequent calculus.