Implementations


PDLtableau:
A prototypical implementation of the tableau calculus for
PDL of De Giacomo and Massacci (2000).
With the help of the tool we discovered that the cutfree version of
the calculus is not sound, which means that the longstanding
problem of the existence of a cutfree calculus for PDL remains open.
To our knowledge PDLtableau is the only existing
implementation of a prover for PDL.

An ADL parser:
A collection of classes and Java implementation of a lexical analyser
and parser of formulae in ADL syntax.
It generates abstract syntax tree (AST) representations which are in
turn are used by a series of translators to produce inputs for provers.

Series of translators:
(a) From ADL to CPDL. An implementation
of an EXPTIMEtranslation of ADLformulae
into CPDLAST representations.
Using the technique in Schmidt, Tishkovsky, Hustadt (2004)
the translation can be improved to a
polynomial time translation.
(b) From CPDL to PDL.
A PTIMEalgorithm translating a
CPDLAST representation into a PDLAST representation using the
technique of De Giacomo for eliminating the converse operator.
(c) From PDL to the syntax of the DLP prover of PatelSchneider
and the PDLTABLEAU prover.
Linear algorithms which translate a given
PDLAST representation into text files suitable for
input to DLP and PDLTABLEAU.

ml2dfg:
Implements the axiomatic translation principle for a range of modal
logics.
In conjunction with the translator FLOTTER and
dfg2tptp (both are part of the MSPASS distribution) it can
be used with any firstorder logic theorem prover recognising DFG or
TPTP input.
This combination of tools effectively renders the most powerful and
flexible fully automated theorem prover for modal logic and firstorder
logic available to date.

TRP:
The first fullyautomatic theorem prover implementing the temporal resolution
calculus of Fisher, Dixon and Peim (2001).
TRP was used to show the practicality of temporal resolution as a
decision procedure for PLTL and to illustrate the new scientific
benchmarking paradigm.

PLTLmona:
A translator from PLTL into WS1S.
Using the MONA tool, a decision procedure for WS1S,
this provides a decision procedure for PLTL.

K. Nellas (2001) developed a tableau prover for Peirce
logic.
By the duality result shown in Schmidt, Orlowska and Hustadt (2003) the
prover can also be used as a prover for the RasiowaSikorski
calculus for Peirce logic.
Besides MSPASS this is the only implemented prover for Peirce logic.

C. Livadiotis (2003) developed ACT, a description
logic ABox reasoner.
This project has implemented and studied the use of very efficient
data structures and algorithms in C.

Z. Li (2003) developed MLTP, a modal logic tableau
prover implemented in C.
It includes a number of optimisation techniques and Initial experiments
on randomly generated problems are encouraging.
The extension of this prover into a prover for agent logics is the
topic of further studies.

Journal papers


R. A. Schmidt, D. Tishkovsky, and U. Hustadt.
Interactions between knowledge, action and commitment within agent dynamic logic.
Studia Logica. Accepted for publication.
[Abstract]

R. A. Schmidt and D. Tishkovsky,
Multiagent dynamic logics with informational test.
Annals of Mathematics and Artificial Intelligence,
Special issue on Computational Logic in MultiAgent Systems.
Accepted for publication.
[Abstract]
 C. Dixon, M. Fisher, and A. Bolotov,
Clausal Resolution in a Logic of Rational Agency.
Artificial Intelligence,
139 (1), 2002, pp. 4789.
 R. A. Schmidt and D. Tishkovsky,
On Axiomatic Products of PDL and S5:
Substitution, Tests and Knowledge.
Bulletin of the Section of Logic,
Vol. 31(1),
pp. 2736.
[Compressed PostScript,
PDF]
 B. Bennett, C. Dixon, M. Fisher, U. Hustadt, E. Franconi, I. Horrocks,
and M. de Rijke,
Combinations of Modal Logics.
Artificial Intelligence Review 17(1):120.
 M. Fisher, C. Dixon, and M. Peim,
Clausal Temporal Resolution.
ACM Transactions on Computational Logic 2 (1).
[PostScript]

Book chapters


R. A. Schmidt and U. Hustadt.
Mechanised Reasoning and Model Generation for Extended Modal Logics.
In de Swart, H. C. M. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds),
Theory and Applications of Relational Structures as Knowledge Instruments.
Lecture Notes in Computer Science
Vol. 2929,
Springer,
3867, 2003.
Survey commissioned for the Kickoff Volume of COST Action 274.
[Abstract,
PDF]
 R. A. Schmidt and D. Tishkovsky,
Combining Dynamic Logic with Doxastic Modal Logics.
Advances in Modal Logic,
Volume 4,
pp. 371392,
King's College Publ., 2003.
[Abstract]

U. Hustadt,
C. Dixon,
R. A. Schmidt,
M. Fisher,
J.J. Meyer and W. van der Hoek,
Verification within the KARO Agent Theory.
In
Formal Approaches to AgentBased Systems.
Accepted for publication.
[Abstract,
Compressed PostScript]

Major conference contributions


V. Goranko, U. Hustadt, R. A. Schmidt, and D. Vakarelov.
SCAN is complete for all Sahlqvist formulae.
In
Proc. of the Seventh International Seminar on Relational Methods in Computer Science (RelMiCS 7).
Lecture Notes in Artificial Intelligence,
Springer.
Accepted for publication.
[Abstract]

R. A. Schmidt, E. Orlowska and U. Hustadt.
Two Proof Systems for Peirce Algebras
In
Proc. of the Seventh International Seminar on Relational Methods in Computer Science (RelMiCS 7).
Lecture Notes in Artificial Intelligence,
Springer.
Accepted for publication.
[Abstract]
 R. A. Schmidt and U. Hustadt,
A Principle for Incorporating Axioms into
the FirstOrder Translation of Modal Formulae.
In Baader, F. (ed.),
Automated DeductionCADE19.
Lecture Notes in Artificial Intelligence
Vol. 2741,
Springer,
412426, 2003.
[Abstract,
Compressed Postscript]
 C. Dixon, C. Nalon, and M. Fisher,
Tableaux for Temporal Logics of Knowledge: Synchronous Systems of
Perfect Recall or No Learning.
In Proceedings of TIMEICTL 2003, IEEE, 2003.
[Postscript]
 R. A. Schmidt and D. Tishkovsky,
MultiAgent Logic of Dynamic Belief and Knowledge.
In Flesca, S. and Greco, S. and Leone, N. and Ianni, G. (eds),
Proceedings of the 8th European Conference on
Logics in Artificial Intelligence (JELIA),
Lecture Notes in Artificial Intelligence,
Vol. 2424,
Springer,
pp. 3849, 2002.
[Abstract,
PostScript]
 R. A. Schmidt and U. Hustadt,
Scientific Benchmarking with Temporal Logic Decision Procedures.
In Fensel, D. and Giunchiglia, F. and McGuinness, D. and Williams, M.A. (eds),
Principles of Knowledge Representation and Reasoning:
Proceedings of the Eighth International Conference (KR'2002),
Morgan Kaufmann,
pp. 533544, 2002.
[Abstract]
 U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher,
J.J. Meyer and W. van der Hoek,
Reasoning about Agents in the KARO Framework,
In Bettini, C. and Montanari, A. (eds),
Proceedings of the Eighth International Symposium
on Temporal Representation and Reasoing (TIME'2001).
IEEE Computer Society, pp.206213, 2001.
[Abstract]
 U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.J. Meyer and W. van der Hoek
Verification within the KARO Agent Theory.
In Rash, J. L., Rouff, C. A., Truszkowski, W.,
Gordon, D. and Hinchey, M. G. (eds),
Formal Approaches to AgentBased Systems.
Lecture Notes in Artificial Intelligence,
Vol. 1871, Springer, pp. 3347, 2001.
[Abstract]

Other publications

 R. A. Schmidt and D. Tishkovsky,
An Agent Logic Tableaux System.
Book of abstracts of the Tenth Workshop on Automated Reasoning,
University of Liverpool,
1516, 2003.
 R. A. Schmidt and D. Tishkovsky,
On Axiomatic Products of PDL and S5: Substitution, Tests and Knowledge.
Book of abstracts of the Ninth Workshop on Automated Reasoning,
Collocated with AISB 2002
,
Imperial College of Science, Technology and Medicine,
April 35 2002.
 R. A. Schmidt and D. Tishkovsky,
A Decidable Dynamic Logic for Agents with Motivational Attitudes.
In Method for Modalities2 Workshop Proceedings (M4M2)
,
12 pp., Amsterdam, November 2001.
[Compressed PostScript,
PDF;
long version: compressed PostScript,
PDF]

B. Hirsch and U. Hustadt,
Translating PLTL into WS1S: Application Description.
In Method for Modalities2 Workshop Proceedings (M4M2)
, Amsterdam, November 2001.
[Abstract,
PostScript]
Software: TRP
 R. A. Schmidt and U. Hustadt,
Formulae which Highlight Differences
between Temporal Logic and Dynamic Logic Provers.
In Giunchiglia, E. and Massacci, F. (eds),
Issues in the Design and Experimental Evaluation
of Systems for Modal and Temporal Logics.
Technical Report DII 14/01,
Dipartimento di Ingegneria dell'Informazione,
Unversitä degli Studi di Siena, Siena, Italy, pp.6876.
[Abstract,
Compressed PostScript]
 R. A. Schmidt and D. Tishkovsky,
An extension of *free PDL for agentbased theories.
Book of abstracts of the Logic Colloquium'2001 (LC'2001),
p. 154, Vienna, August 2001.
 R. A. Schmidt and D. Tishkovsky,
On Calculi and Kripke Semantics for MultiAgent Systems
within the KARO Framework.
International Joint Conference on Automated Reasoning, IJCAR2001,
Short papers, Edited by R.Gore, A.Leitsch, T.Nipkow,
p.150159, Siena, Italy, June 1923 2001.
 R. A. Schmidt and D. Tishkovsky,
On Calculi and Kripke Semantics for MultiAgent Systems
within the KARO Framework.
Book of abstracts of the Eight Workshop on Automated Reasoning,
Collocated with AISB 2001, p.30, The University of York,
March 2223 2001.

Preprints

 R. A. Schmidt and U. Hustadt,
A Principle for Incorporating Axioms into
the FirstOrder Translation of Modal Formulae.
Preprint CSPP22
,
University of Manchester, 2004.

R. A. Schmidt, D. Tishkovsky, and U. Hustadt.
Interaction between knowledge, action and commitment within agent dynamic logic.
Preprint CSPP27
,
University of Manchester, 2003.
[Abstract,
PostScript]

R. A. Schmidt and D. Tishkovsky.
Combining dynamic logic with doxastic modal logics.
Preprint CSPP23
,
University of Manchester, 2003.
[Compressed PostScript]
 R. A. Schmidt and U. Hustadt,
Mechanised Reasoning and Model Generation for Extended Modal Logics.
Preprint CSPP19,
University of Manchester, UK.
[Abstract,
Compressed PostScript]

MSc theses

 C. Livadiotis,
Designing and Implementing a Description Logic ABox Reasoner.
University of Manchester, 2003.
 Z. Li,
An Automated Proof System for Reasoning About Agents.
University of Manchester, 2003.
 K. Nellas,
Reasoning About Sets and Relations: A Tableauxbased Automated Theorem Prover for Peirce Logic.
University of Manchester, 2001.
