Agent Dynamic Logic package


The aim of this package is to provide an implementation of algorithms for reduction of the satisfiability problem in Agent Dynamic Logic (ADL) to the satisfiability problems in Propositional Dynamic Logic with Converse (CPDL) and Propositional Dynamic Logic (PDL). Together with any implementation of a decision procedure, i.e. prover, for PDL or CPDL it gives a prover for ADL. Given a prover for PDL or CPDL the package can be extended to produce an appropriate input for such a prover. At the current state it supports formats for two provers: Description Logic Prover (DLP) and PDL-tableau prover.

The package consists of the following parts.

  • A parser of ADL expressions. It accepts a string representation of ADL formulae and constructs their internal representation, so-called abstract syntax tree (AST).
    This is LL1-parser (one token of lookahead) generated by ANTLR parser generator.
  • A translator of AST of an ADL expression to AST of a CPDL expression. It implements EXPTIME algorithm of Schmidt and Tishkovsky (2001). The algorithm preserves satisfiability of formulae.
  • A translator of AST of CPDL expression to AST of a PDL expression. It implements PTIME algorithm of De Giacomo (1996) of elimination of the converse operator from CPDL preserving satisfiability of formulae.
  • A bunch of functions which provide various string representation formats of given AST of (C)PDL expression. At the moment, only formats of DLP and PDL-tableau prover are supported.
Valid XHTML 1.0! Valid CSS! There were 14768 visits of this page since Wed, 03 May 2006 20:57:56 BST.
Last modified: Sat, 17 Mar 2007 18:58:32 GMT.
Copyright ©2006 Dmitry Tishkovsky, School of Computer Science, The University of Manchester