Two tutorials will be given as part of the Tableaux 2009 programme.
The tutorials will be held in parallel on the morning of Wednesday, 7 July.
The Theory of Canonical Systems
This tutorial will be presented by Arnon Avron and Anna Zamansky from Tel-Aviv University, Israel.
NEW: Download the Slides shown at the tutorial.
Description:
Canonical Gentzen-type systems form a natural class of systems, which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a connective is introduced and no other connective is mentioned. Cut-elimination in these systems is fully characterized by a simple constructive criterion called coherence. Moreover, there is a remarkable correspondence in these systems between the criterion of coherence, cut-elimination and a natural semantic characterization of these systems in terms of two-valued non-deterministic matrices. We believe that many researchers in the community of automated reasoning could benefit from the approach of applying non-deterministic matrices to (fully or partially) characterize cut-elimination in various deduction systems.
In this tutorial we cover the theory of canonical systems, focusing mainly on multiple- and single-conclusioned Gentzen-type canonical calculi on the propositional level. However, we shall also discuss the extension of these results to languages with quantifiers and to signed calculi (of which the Gentzen-type systems are particular instances). The content of this tutorial is mainly self-contained and the level is introductory. The only previous knowledge we assume is that of Gentzen-type systems. We shall also provide a short introduction of the theory of non-deterministic matrices.
LoTREC: Theory and Practice. Proving by Tableau becomes easier...
This tutorial will be presented by Bilal Said and Olivier Gasquet from the Université Paul Sabatier in Toulouse, France.
Description:
Unless they strictly use standard modal logics, people who work on the formalization of such and such concept are likely to be interested in the possibility of quickly implementing a prover or a model builder for their logics. LoTREC allows to handle almost any logic having a Kripke semantics, or more generally a semantics based in transition system, as long as a model builder for it can be expressed as a graph rewriting system, i.e. as long as we are able to express its semantical constraints with graph rewriting rules.
One main feature of LoTREC is to offer a high-level language for describing rewrite rules over a graph, and a very simple language for describing what we call a strategy, i.e. a description of the rules application order. This allows LoTREC to be used for one’s own logic by non-computer scientists since only small programming skills are necessary.
Another good reason for choosing LoTREC is that it is accessible via the web with one click installation. It has a rich graphical user interface that makes it easy to define new tableau calculi and to visualize the graph models.
Currently in LoTREC, we have tableau provers for various propositional logics such as CPL, K, KT, S4, KD45, S5, K + Confluence, K + the universal modality, LTL, PDL and many others...
In this tutorial, we give an overview of the theoretical basis of LoTREC, and then we give a demonstration on how to use LoTREC to build tableau provers for various propositional non-classical logics with a bunch of examples. This tutorial requires a basic knowledge of tableau calculi for propositional standard modal logics and some of its basic techniques such as loop-check.