Proof Methods for Multi-Agent Systems

EPSRC reseach grant GR/M88761

Case For Support

General

Dates

Start date: 15 January 2001
End date: 14 January 2004

Personnel

Principal investigator: Renate A. Schmidt
Research Associate: Dmitry Tishkovsky
Co-Investigators:

Collaborators

The work in this project benefited from significant collaborations with:


Outputs

In total the project has produced 9 implemented tools and 29 publications (including 6 journal papers, 3 book chapters, 8 major conference contributions, 8 other publications, 3 MSc theses, and 4 preprints).

Implementations
  1. PDL-tableau: 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 cut-free version of the calculus is not sound, which means that the long-standing problem of the existence of a cut-free calculus for PDL remains open. To our knowledge PDL-tableau is the only existing implementation of a prover for PDL.
  2. 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.
  3. Series of translators: (a) From ADL to CPDL. An implementation of an EXPTIME-translation of ADL-formulae into CPDL-AST 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 PTIME-algorithm translating a CPDL-AST representation into a PDL-AST representation using the technique of De Giacomo for eliminating the converse operator. (c) From PDL to the syntax of the DLP prover of Patel-Schneider and the PDL-TABLEAU prover. Linear algorithms which translate a given PDL-AST representation into text files suitable for input to DLP and PDL-TABLEAU.
  4. 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 first-order 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 first-order logic available to date.
  5. TRP: The first fully-automatic 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.
  6. PLTLmona: A translator from PLTL into WS1S. Using the MONA tool, a decision procedure for WS1S, this provides a decision procedure for PLTL.
  7. 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 Rasiowa-Sikorski calculus for Peirce logic. Besides MSPASS this is the only implemented prover for Peirce logic.
  8. 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.
  9. 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
  1. R. A. Schmidt, D. Tishkovsky, and U. Hustadt. Interactions between knowledge, action and commitment within agent dynamic logic. Studia Logica. Accepted for publication. [Abstract]
  2. R. A. Schmidt and D. Tishkovsky, Multi-agent dynamic logics with informational test. Annals of Mathematics and Artificial Intelligence, Special issue on Computational Logic in Multi-Agent Systems. Accepted for publication. [Abstract]
  3. C. Dixon, M. Fisher, and A. Bolotov, Clausal Resolution in a Logic of Rational Agency. Artificial Intelligence, 139 (1), 2002, pp. 47-89.
  4. 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. 27-36. [Compressed PostScript, PDF]
  5. 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):1-20.
  6. M. Fisher, C. Dixon, and M. Peim, Clausal Temporal Resolution. ACM Transactions on Computational Logic 2 (1). [PostScript]
Book chapters
  1. 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, 38-67, 2003. Survey commissioned for the Kickoff Volume of COST Action 274. [Abstract, PDF]
  2. R. A. Schmidt and D. Tishkovsky, Combining Dynamic Logic with Doxastic Modal Logics. Advances in Modal Logic, Volume 4, pp. 371-392, King's College Publ., 2003. [Abstract]
  3. 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 Agent-Based Systems. Accepted for publication. [Abstract, Compressed PostScript]
Major conference contributions
  1. 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]
  2. 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]
  3. R. A. Schmidt and U. Hustadt, A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. In Baader, F. (ed.), Automated Deduction-CADE-19. Lecture Notes in Artificial Intelligence Vol. 2741, Springer, 412-426, 2003. [Abstract, Compressed Postscript]
  4. C. Dixon, C. Nalon, and M. Fisher, Tableaux for Temporal Logics of Knowledge: Synchronous Systems of Perfect Recall or No Learning. In Proceedings of TIME-ICTL 2003, IEEE, 2003. [Postscript]
  5. R. A. Schmidt and D. Tishkovsky, Multi-Agent 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. 38-49, 2002. [Abstract, PostScript]
  6. 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. 533-544, 2002. [Abstract]
  7. 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.206-213, 2001. [Abstract]
  8. 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 Agent-Based Systems. Lecture Notes in Artificial Intelligence, Vol. 1871, Springer, pp. 33-47, 2001. [Abstract]
Other publications
  1. R. A. Schmidt and D. Tishkovsky, An Agent Logic Tableaux System. Book of abstracts of the Tenth Workshop on Automated Reasoning, University of Liverpool, 15-16, 2003.
  2. 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 3-5 2002.
  3. R. A. Schmidt and D. Tishkovsky, A Decidable Dynamic Logic for Agents with Motivational Attitudes. In Method for Modalities-2 Workshop Proceedings (M4M-2) , 12 pp., Amsterdam, November 2001. [Compressed PostScript, PDF; long version: compressed PostScript, PDF]
  4. B. Hirsch and U. Hustadt, Translating PLTL into WS1S: Application Description. In Method for Modalities-2 Workshop Proceedings (M4M-2) , Amsterdam, November 2001.
    [Abstract, PostScript] Software: TRP
  5. 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.68-76. [Abstract, Compressed PostScript]
  6. R. A. Schmidt and D. Tishkovsky, An extension of *-free PDL for agent-based theories. Book of abstracts of the Logic Colloquium'2001 (LC'2001), p. 154, Vienna, August 2001.
  7. R. A. Schmidt and D. Tishkovsky, On Calculi and Kripke Semantics for Multi-Agent Systems within the KARO Framework. International Joint Conference on Automated Reasoning, IJCAR-2001, Short papers, Edited by R.Gore, A.Leitsch, T.Nipkow, p.150-159, Siena, Italy, June 19-23 2001.
  8. R. A. Schmidt and D. Tishkovsky, On Calculi and Kripke Semantics for Multi-Agent 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 22-23 2001.
Preprints
  1. R. A. Schmidt and U. Hustadt, A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Preprint CSPP-22 , University of Manchester, 2004.
  2. R. A. Schmidt, D. Tishkovsky, and U. Hustadt. Interaction between knowledge, action and commitment within agent dynamic logic. Preprint CSPP-27 , University of Manchester, 2003. [Abstract, PostScript]
  3. R. A. Schmidt and D. Tishkovsky. Combining dynamic logic with doxastic modal logics. Preprint CSPP-23 , University of Manchester, 2003. [Compressed PostScript]
  4. R. A. Schmidt and U. Hustadt, Mechanised Reasoning and Model Generation for Extended Modal Logics. Preprint CSPP-19, University of Manchester, UK. [Abstract, Compressed PostScript]
MSc theses
  1. C. Livadiotis, Designing and Implementing a Description Logic ABox Reasoner. University of Manchester, 2003.
  2. Z. Li, An Automated Proof System for Reasoning About Agents. University of Manchester, 2003.
  3. K. Nellas, Reasoning About Sets and Relations: A Tableaux-based Automated Theorem Prover for Peirce Logic. University of Manchester, 2001.