We just discovered a small bug in the CTL prover in the demo section of the website.

The bug was a trivial problem with the nnf procedure and it's now fixed.

We just discovered a small bug in the CTL prover in the demo section of the website.

The bug was a trivial problem with the nnf procedure and it's now fixed.

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 ).