The Tableau WorkBench (TWB)

I've uploaded my honours thesis, looking at the tactic semantics of the TWB.

I have ported the TWB to the new version of the ocaml compile. However since the TWB is heavily dependent on the old ocaml pre-processor, I've decided to postpone the re-write of the parser for the new pre-processor relesed with OCaml 3.10 and to use camlp5 instead.

Camlp5 is the old version of OCaml Pre-processor and it is now distributed as stand-alone library.

I've created a second branch of the TWB source code available via darcs .
http://twb.rsise.anu.edu.au/cgi-bin/darcsweb/darcsweb.cgi

These are the slides of our presentation at LPAR07

'''NB''': We are working to make the implementation of this calculus available on this website by the end of the week. '''UPDATE''': * pdlMarkedNoSnf.ml : http://twb.rsise.anu.edu.au/propositional_dynamic_logic_no_snf * pdlMarked.ml: http://twb.rsise.anu.edu.au/propositional_dynamic_logic_snf alternatively you can also check this out : http://users.rsise.anu.edu.au/~rpg/pdlweb/ paper accepted to m4m http://m4m.loria.fr/M4M5/ ==Abstract== We present a tableau-based algorithm for deciding satisfiability for propositional dynamic logic (PDL) which builds a finite rooted tree

paper accepted to m4m http://m4m.loria.fr/M4M5/ ==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

Paper accepted to LPAR 07 : http://www.lpar.net/2007/

Abstract:

I read a few interesting papers about the relation of modal logic (and in particular fix-point modal logics) with description logics and automata techniques. == Description Logics: Modal Logics for Class-Based Modeling == http://www.dis.uniroma1.it/~degiacom/ftp/00/Degi00aiml.ps.gz In this paper De Giacomo gives a clear overview regarding the relation of several description logics with well known modal logics.

* Online Tutorial (still incomplete) : http://twb.rsise.anu.edu.au/tutorial * Slides from the presentation : http://twb.rsise.anu.edu.au/files/twbtutorial.pdf * Latest Version of the TWB: (I'm working on it ...) == Instructions to Compile the TWB == ===Pre-Requesites === To install and run the TWB is essential to have the following software installed on the system * ocaml compiler version 3.09.2 * findlib * extlib 1- the ocaml compiler can be downloaded from: * http://caml.inria.fr/ocaml/index.en.html

We are going to present this paper at a satellite workshop at TABLEAUX 2007 : http://tableaux2007.univ-cezanne.fr/scientific-program.html

paper submitted to AGENTS, LOGIC AND THEOREM PROVING workshop at TABLEAUX 2007

Abstract:

Abstract. We present a cut-free tableau calculus with histories and variables for
the EXPTIME-complete multi-modal logic of common knowledge (LCK). Our
calculus constructs the tableau using only one pass, so proof-search for testing
theoremhood of j does not exhibit the worst-case EXPTIME-behaviour for all j
as in two-pass methods. Our calculus also does not contain a “finitized w-rule”
so that it detects cyclic branches as soon as they arise rather than by worst-case