Honours thesis now available

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

TWB for Ocaml 3.10 / camlp5 5.02

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 .

Slides for LPAR07

These are the slides of our presentation at LPAR07

An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability

'''NB''': We are working to make the implementation of this calculus available on this website by the end of the week. '''UPDATE''': * : * alternatively you can also check this out : paper accepted to m4m ==Abstract== We present a tableau-based algorithm for deciding satisfiability for propositional dynamic logic (PDL) which builds a finite rooted tree

TWB system description

paper accepted to m4m ==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

One-pass Tableaux for Computation Tree Logic (CTL)

Paper accepted to LPAR 07 :


Automata, description logics and other complexity matters

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 == In this paper De Giacomo gives a clear overview regarding the relation of several description logics with well known modal logics.

Material For the TWB Tutorial

* Online Tutorial (still incomplete) : * Slides from the presentation : * 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: *

Cut-Free Single-pass Tableaux for the Logic of Common Knowledge

We are going to present this paper at a satellite workshop at TABLEAUX 2007 :

Cut-Free Single-pass Tableaux for the Logic of Common Knowledge

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


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

Syndicate content