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