Abstract
A deduction-based decision procedure is presented for a fragment of mutual belief logic with quantified agent variables (MBQL). The language of MBQL contains belief, everybody believes and mutual belief modalities, variables and constants for agents. The language of MBQL is convenient to describe the properties of rational agents when the number of agents is not known in advance. On the other hand, even if the exact number of agents is known, a language with quantified agent variables allows us to use more compact expressions. For the MBQL a sequent calculus MBQ * with invertible (in some sense) rules is proposed. The presented decision procedure is realized by means of the calculus MBQ * that allows us to simplify a procedure of loop-check sharply. For a fragment of MBQL (without positive occurrences of mutual belief modality), the loop-check-free sequent calculus is proposed. To this end, special rules for belief and everybody believes modalities (introducing marked modalities and indices) and special sequents serving as a termination criterion for non-derivability are introduced. For sequents containing positive occurrences of mutual belief modality sequents of special shape are used to specialize a loop-check and to find non-logical (loop-type) axioms.
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.
References
Alberucci, L.: The modal μ-calculus and the logic of common knowledge. Ph.D. thesis, Institut für Informatic and angewandte mathematik, Universität Bern (2002)
Aldewereld, H., van der Hoek, W., Meyer, J.J.C.: Rational teams: logical aspects of multiagent systems. Fundamenta Informaticae 63(2-3), 159–183 (2004)
Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic 57, 795–807 (1992)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about knowledge. MIT Press, Cambridge (1995)
Fitting, M., Thalmann, L., Voronkov, A.: Term-modal logics. Studia Logica 69(1), 133–169 (2001)
Gough, G.D.: Decision procedures for temporal logic. Master’s thesis, Department of Computer Science, Manchester University, Oxford Rd., Manchester, M139PL, UK (October 1984)
Halpern, J.Y., Shore, R.A.: Reasoning about common knowledge with infinitely many agents. Information and Computation 191, 1–40 (2004)
Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical propositional logics. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 210–225. Springer, Heidelberg (1996)
Hudelmaier, J.: A contraction-free sequent calculus for S4. In: Wansing, H. (ed.) Proof Theory for Modal Logic, pp. 3–16. Kluwer Academic Publishers, Dordrecht (1996)
Kanger, S.: A simplified proof method for elementary logic. In: Computer Programming and Formal Systems, Studies in Logic and the Foundations of Mathematics, pp. 87–93. North-Holland, Amsterdam (1963)
Kawai, H.: Sequential calculus for a first-order infinitary temporal logic. Zeitchr. für Math. Logic and Grundlagen der Math. 33, 423–432 (1987)
Kleene, S.C.: Introduction to metamathematics. D.Van Nostrand Company, North-Holland Publishing Co., P. Noordhoff LTD (1952)
Lomuscio, A., Colombetti, M.: QLB: A quantified logic for belief. In: Jennings, N.R., Wooldridge, M.J., Müller, J.P. (eds.) ECAI-WS 1996 and ATAL 1996. LNCS, vol. 1193, pp. 71–85. Springer, Heidelberg (1997)
Meyer, J.J.C., van der Hoek, W.: Epistemic Logic for AI and Computer Science. Cambridge University Press, Cambridge (1995)
Nide, N., Takata, S.: Deduction systems for BDI logics using sequent calculus. In: Proc. of AAMAS 2002, pp. 928–935 (2002)
Pliuškevičius, R., Pliuškevićienė, A.: Decision procedure for a fragment of temporal logic of belief and actions with quantified agent and action variables. Annals of Mathematics, Computing & Teleinformatics 1(2), 51–72 (2004)
Shwarts, G.F.: Gentzen style systems for K45 and K45D. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 245–256. Springer, Heidelberg (1989)
Wolper, P.: The tableaux method for temporal logic: an overview. Logique et Analyse 28, 119–136 (1985)
Wooldridge, M.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)
Wooldridge, M.: An introduction to multiagent systems. John Wiley & Sons Ltd, Chichester (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pliuškevičius, R., Pliuškevičienė, A. (2006). Decision Procedure for a Fragment of Mutual Belief Logic with Quantified Agent Variables. In: Toni, F., Torroni, P. (eds) Computational Logic in Multi-Agent Systems. CLIMA 2005. Lecture Notes in Computer Science(), vol 3900. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11750734_7
Download citation
DOI: https://doi.org/10.1007/11750734_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33996-0
Online ISBN: 978-3-540-33997-7
eBook Packages: Computer ScienceComputer Science (R0)