The Tableau WorkBench (TWB)

To be delivered at TABLEAUX 2007 : http://tableaux2007.univ-cezanne.fr

Authors: Pietro Abate and Rajeev Gore

Level: You should know the basics of tableau/sequent calculi as
explained in the Handbook of Tableau Methods (for example).
Only rudimentary programming knowledge is required but basic
functional programming knowledge would be ideal.

The following notions would be useful for understanding some of
the more advanced concepts: termination methods like
loop-checks and histories; optimisation methods like

This evening I committed the core changes I've done to the TWB in the last month or so. I committed all the changes
in one batch and now I'll be adding bug fixes till the next major release of the code.

The major changes in the upcoming release will be:

* '''new connectives and grammar definition.''' The connective definition in the previous release
wasn't flexible enough to define complicated grammars ala' PDL. Now the user is in charge of
defining both the connectives and the grammar used in the rule definition. For example, a
definition for PDL will be of the form:

Abstract:

The Tableau Workbench (TWB) is a generic framework for building automated theorem provers for
arbitrary propositional logics. The TWB has a small core that defines its general architecture, some extra
machinery to specify tableau-based provers and an abstraction language for expressing tableau rules.
This language allows users to ``cut and paste'' tableau rules from textbooks and to specify a search
strategy for applying those rules in a systematic manner. A new logic module defined by a user is

Abstract:

The tableau method is widely used by logicians to give decision procedure for classical and non classical logics. But the move from proof-theoretic tool to an efficient automated theorem prover is often difficult for researchers with no technical background. The main ``problem'' is the non-determinism inherent in the tableau method. In this paper we give a functional algorithm to mechanize the tableau method which is concise and easy to re-use. We also briefly describe an implementation of this algorithm called the Tableau Workbench.

Paper sumbitted to Tableaux 2007
http://ta

The formulae used in a TWB file are defined according to the CONNECTIVES definition given at the top of the file.


CONNECTIVES
DImp, "_<->_", Two;
And, "_&_", One;
Or, "_v_", One;
Imp, "_->_", One;
Not, "~_", Zero;
Falsum, Const;
Verum, Const
END


However, since data type are currently hardwired in the TWB library, writing more complex formulae is at the moment fairly complicated. To fix this shortcoming I worked to a camlp4 extension to extend the TWB syntax on the fly using an initial grammar definition.

These (links below) are the slides presented at the LAMAS workshop 2007.

Abstract:

Pietro Abate and Rajeev Goré, Australian National University, A Cut-free Tableau Calculus for the Logic of Common Knowledge

Reasoning about knowledge, in particular about the knowledge of agents who reason about the world and each other's knowledge, plays an important role in several areas of computer science, philosophy, game theory and many other fields. The notion of Common Knowledge (CK), where everybody knows, every- one knows that everyone knows, etc has also proved fundamental in the analysis of interacting groups of agents (see [FHMV95] for an extensive overview).

Abstract
In this paper we focus on the development of a cut-free nitary tableau calculus with histories for n-agent modal logics with common knowledge (LCK). Thus, we get a proof system where proof-search becomes feasible and we lay the basis for developing a uniform framework for the treatment of the family of logics of common knowledge. Unlike two-pass decision methods like those for temporal logics, our calculus gives a single-pass decision procedure which is space-optimal.

These are the slides from a recent talk I gave in several research labs in europe.

I've almost finished to write a paper for lamas 06 ( http://www.cs.otago.ac.nz/staffpriv/hans/lamas2.html ) about the logic of common knowledge. I've a working implementation of LCK with two agents with the TWB that I'll put online in the next few days in the d3mo section. The LCK calculus is very closely related to the UB calculus I've proposed in my thesis.

This week has been pretty full on. Raj implemented several calculi from his handbokk chapter. At the moment we've a working implementaion of S45, K4, KD, K4D .

I've fixed few minors bus to the twb-stable and I've managed to find a problem with the ocaml pre-processor ( http://caml.inria.fr/mantis/view.php?id=4165 ).

I've spent the last 10 days fighting with a nasty bug in the tactic component of the TWB. The problem was that I didn't implement the semicolon ";" operator in the strategy correctly. after a bit of pain an sweat, I finally managed to fix this problem, that btw affects the "stable" version of the TWB as well, and now I should be back on track to work on the sequent interface and all the old new feature that I had planned.

By fixing this problem I've also realized that I can express a more general fixpoint operator in the TWB. Up until now the strategy for modal logic K was specified by ((Id|Or|And)* | K)* where the star operator means "repeat until impossible" . However, the semantic of the star operator also implied that when no more rule are applicable, the strategy should fail. Coupling a failing strategy with the alternation operator "|" would always lead to an erroneous answer. By accident, and by mistake, I've managed to make this work anyway.