Distributed modal theorem proving with KE. (English) Zbl 1412.68254
Migliolo, P. (ed.) et al., Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15–17, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1071, 160-176 (1996).
Summary: This paper describes an approach to distributed modal theorem proving by bringing together and exploiting two software packages. The first is the implementation of a theorem prover for normal modal logics based on KE and a generalization of Fitting’s prefixed tableaux. The second is a library for implementing brokered inter-process communication over the internet. We describe three demonstrators which combine these implementations and illustrate potential applications of the new technology, enabling theorem provers connected to the internet to cooperate, compete, or be used by third parties.
For the entire collection see [Zbl 0939.00023].
For the entire collection see [Zbl 0939.00023].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B45 | Modal logic (including the logic of norms) |
References:
| [1] | G. Almasi, A. Suvaaiala, I. Muslea, C. Cascaval, T. Davis, and V. Jagannathan. Web\^{}{*}: A technlogy to make information available on the web. Technical Report, Concurrent Engineering Research Center, West Virginia University, 1995. |
| [2] | ANSA. The ANSA Model for Trading and Federation. Architecture Report AR.005.00, 1993. |
| [3] | B. Beckert and J. Posegga. lean \(T\)\^{}{A}\(P\): Lean tableau-based thereom proving. \(Journal of Automated Reasoning\), 1995. · Zbl 0838.68097 |
| [4] | A. Beitz and M. Bearman. An ODP trading service for DCE. In \(Proceedings First International Workshop on Services in Distributed and Networked Environments\), pages 42-49. 1994. |
| [5] | B. Burmeister, A. Haddadi, and K. Sundermeyer. Generic configurable cooperation protocols for multi-agent systems. In \(MAAMAW'93, Neuchatel\), 1993. |
| [6] | L. Catach. Tableaux: A general theorem prover for modal logics. \(Journal of Automated Reasoning\), 7:489-510, 1991. · Zbl 0743.03008 |
| [7] | B. Chellas. \(Modal Logic: An Introduction\). CUP, 1980. · Zbl 0431.03009 |
| [8] | J. Cunningham. Investigations into modular and concurrent deduction. CEC Esprit Project Medlar (Esprit 6471) Periodic Progress Report 2, Department of Computing, Imperial College of Science, Technology and Medicine, 1994. |
| [9] | J. Cunningham and J. Pitt. Towards model building in multi-modal logics using KE and constraint satisfaction. CEC Esprit Project Medlar (Esprit 6471) PPR3, Department of Computing, Imperial College of Science, Technology and Medicine, 1995. |
| [10] | M. D’Agostino and D. Gabbay. A generalization of analytic deduction via labelled deductive systems. part I: Basic substructural logics. \(Journal of Automated Reasoning\), 13:243-281, 1994. · Zbl 0816.03012 |
| [11] | M. D’Agostino and M. Mondadori. The Taming of the Cut. \(Journal of Logic and Computation\), 4:285-319, 1994. · Zbl 0806.03037 |
| [12] | ECRC and ICL. ECL\^{}{i}PS\^{}{e} user manual release 3.4.5. ECRC, Munich, 1994. |
| [13] | T. Finin and R. Fritzson. KQML — a language and protocol for knowledge and information exchange. In \(Proceedings of the Thirteenth International Workshop on Distributed Artificial Intelligence\), pages 126-136, Lake Quinalt, WA, 1994. |
| [14] | M. Fitting. Basic modal logic. In D. Gabbay, C. Hogger, and J. Robinson, editors, \(Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 1\), pages 368-448. OUP, 1993. |
| [15] | D. Gabbay. \(Labelled Deductive Systems\). OUP, to appear (1996). |
| [16] | E. Germain. Software’s special agents. New Scientist, 9th April, 1994. |
| [17] | G. Governatori. Labelled tableaux for multi-modal logics. In P. Baumgartner, R. Hähnle, and J. Posegga, editors, \(Proceedings 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods\), LNAI, pages 79-94. Springer-Verlag, 1995. |
| [18] | A. Heuerding, G. Jäger, S. Schwendimann, and M. Seyfried. Propositional logics on the computer. In P. Baumgartner, R. Hähnle, and J. Posegga, editors, \(Proceedings 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods\), LNAI, pages 310-323. Springer-Verlag, 1995. |
| [19] | H.-J. Ohlbach. SCAN — elimination of predicate quantifiers system description. CEC Esprit Project Medlar (Esprit 6471) Periodic Progress Report 3, Department of Computing, Imperial College of Science, Technology and Medicine, 1995. |
| [20] | OMG. The Common Object Request Broker: Architecture and Specification. OMG Document Number 91.12.1 (Revision 1.1), Wiley & Sons, 1992. |
| [21] | J. Pitt, M. Anderton, and J. Cunningham. Normalized interactions between autonomous agents: A case study in inter-organizational project management. \(Computer-Supported Cooperative Work\), to appear. |
| [22] | J. Pitt and J. Cunningham. Blending the Balkans: One approach to integrating and combining inference engines. CEC Esprit Project Medlar (Esprit 6471) PPR3, Department of Computing, Imperial College of Science, Technology and Medicine, 1995. |
| [23] | J. Pitt and J. Cunningham. Theorem proving and model building with the calculus KE. \(Journal of the IGPL\), 4(1):127-148, 1996. · Zbl 0847.68108 |
| [24] | L. Wallen. \(Automated Deduction in Non-Classical Logics\). MIT Press, 1990. · Zbl 0782.03003 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
