Abstract
We present an implementation of an automated reasoning system for multi-robot cooperation. A multi-robot cooperation environment is expressed by a set of multi-robot knowledge and time modal logic formulas. The reasoning procedure of our system is based on a so-called semantic method, that is, a set of multi-robot knowledge and time modal logic formulas is first translated, according to the possible world semantics, into the set of corresponding first-order clauses. Then, instead of checking the satisfiability of the given multi-robot knowledge and time formulas, we check the satisfiability of the set of translated first-order clauses by a general purpose first-order theorem proof procedure ME (the model elimination), augmented with the capabilities of handling transitive axioms and inequality predicates introduced by the translation. We also consider how to use the framework of the possible-world semantics to capture the notions of common knowledge and implicit knowledge, which are essential when considering reasoning, planning and cooperating problem solving in distributed and dynamically changing environments. We then discuss how to translate common knowledge and implicit knowledge into their corresponding first-order formulas. We apply the idea of theory resolution for reasoning about transitive axioms efficiently. We also show some experimental results of our automated reasoning system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E. Ephrati, M.E. Pollack and S. Ur, ‘Deriving Multi-Agent Coordination through Filtering Strategies’, Proceedings of IJCAI, pp. 679–685, 1995.
E. Ephrati and J.S. Rosenschein, ‘Multi-Agent Planning as a Dynamic Search for Social Consensus’, IJCAI, pp. 423–429, 1993.
T. Hogg and C.P. Williams, ‘Solving the Really Hard Problems with Cooperative Search’, pp.231–236, Proceedings of AAAI, 1993.
J.Y. Halpern and Y. Moses, ‘A Guide to the Modal Logics of Knowledge and Belief: Preliminary Draft’, IJCAI, pp. 480–490, 1985.
J.Y. Halpern and Y. Moses, ‘Knowledge and Common Knowledge in a Distributed Environment’, Proceedings of the 3rd ACM Conference on Principles of Distributed Computing, pp. 50–61, 1984.
C. Morgan, ‘Methods for Automated Theorem Proving in Nonclassical Logics’, IEEE, Transactions on Computers, vol. c-25, No. 8, August 1976.
D.W. Loveland, ‘Mechanical Theorem Proving by Model Elimination’, J. of the ACM 15, pp. 236–251, 1968.
M. Stickel, ‘Automated Deduction by Theory Reasoning’, International Joint Conference on AI, pp. 1181–1186, 1985.
J.Y. Halpern and M.Y. Vardi, ‘The Complexity of Reasoning About Knowledge and Time: Extended Abstract’, Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing, pp. 304–315, 1986.
G.E. Hughes and M.J. Cresswell, ‘An Introduction to Modal Logic’, Methuen, London, 1968.
L. He, H. Seki and H. Itoh, ‘WEIHE: An Automated Reasoning System for Multi-Agent Knowledge and Time’, Proceedings of PRICAI, pp 14–19, 1994.
R. Anderson and W.W. Bledsoe, ‘A Linear format for resolution with merging and a new technique for establishing completeness’, J. ACM 28, pp 193–214, 1970.
C.L. Chang and R.C.T. Lee, ‘Symbolic Logic and Mechanical Theorem Proving’, Academic Press, 1973.
R. Manthey and F. Bry ‘SATCHMO: a theorem prover implemented in Prolog’, Proceedings of 9th Conference on Automated Deduction, 1988.
H.J. Ohlbach, ‘A Resolution Calculus for Modal Logics’, CADE’88 (LNCS 310), pp. 500–516, 1986.
A. Nonmengart, ‘First-Order Modal Logic Theorem Proving and Functional Simulation’, IJCAI’93, pp. 80–85, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Springer Japan
About this paper
Cite this paper
He, L., Seki, H., Itoh, H. (1996). Implementing an Automated Reasoning System for Multi-Robot Cooperation. In: Asama, H., Fukuda, T., Arai, T., Endo, I. (eds) Distributed Autonomous Robotic Systems 2. Springer, Tokyo. https://doi.org/10.1007/978-4-431-66942-5_25
Download citation
DOI: https://doi.org/10.1007/978-4-431-66942-5_25
Publisher Name: Springer, Tokyo
Print ISBN: 978-4-431-66944-9
Online ISBN: 978-4-431-66942-5
eBook Packages: Springer Book Archive