Abstract
We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms that characterise such systems. We discuss soundness, completeness, and termination of the method. In particular, completeness can be modularly proved by showing that the conclusions of each newly added inference rule ensures that the corresponding conditions on frames hold. Some examples are given in order to illustrate the use of the method.
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
Baldoni, M., Giordano, L., Martelli, A.: A tableau calculus for multimodal logics and some (un)decidability results. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 44–59. Springer, Heidelberg (1998)
Basin, D., Matthews, S., Viganò, L.: Labelled propositional modal logics: Theory and practice. J. Log. Comput 7(6), 685–717 (1997)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)
Blackburn, P., Dialogue, E.L.E., Cate, B.T.: Beyond pure axioms: Node creating rules in hybrid tableaux. In: Areces, C.E., Blackburn, P., Marx, M., Sattler, U. (eds.) Hybrid Logics, pp. 21–35 (July 25, 2002)
Boolos, G.S.: The Logic of Provability. Cambridge University Press (1993)
Carnielli, W.A., Pizzi, C.: Modalities and Multimodalities. Logic, Epistemology, and the Unity of Science, vol. 12. Springer (2008)
Castilho, M.A., del Cerro, L.F., Gasquet, O., Herzig, A.: Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae 32(3-4), 281–297 (1997)
del Cerro, L.F., Gasquet, O.: Tableaux based decision procedures for modal logics of confluence and density. Fundamenta Informaticae 40(4), 317–333 (1999)
Chellas, B.: Modal Logic: An Introduction. Cambridge University Press (1980)
Demri, S., Nivelle, H.: Deciding regular grammar logics with converse through first-order logic. Journal of Logic, Language and Information 14(3), 289–329 (2005)
Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. MIT Press (1995)
Goré, R., Postniece, L., Tiu, A.: On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Logical Methods in Computer Science 7(2) (2011)
Goré, R., Thomson, J., Widmann, F.: An experimental comparison of theorem provers for CTL. In: Combi, C., Leucker, M., Wolter, F. (eds.) TIME 2011, Lübeck, Germany, September 12-14, pp. 49–56. IEEE (2011)
Hustadt, U., Schmidt, R.A.: Scientific benchmarking with temporal logic decision procedures. In: Fensel, D., Giunchiglia, F., McGuinness, D., Williams, M.-A. (eds.) Proceedings of the KR 2002, pp. 533–544. Morgan Kaufmann (2002)
Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6(3), 467–480 (1977)
Lemmon, E.J., Scott, D.: The Lemmon Notes: An Introduction to Modal Logic. Segerberg, K. (ed.). Basil Blackwell (1977)
Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. J. Algorithms 62, 117–134 (2007)
Nalon, C., Marcos, J., Dixon, C.: Clausal resolution for modal logics of confluence – extended version. Technical Report ULCS-14-001, University of Liverpool, Liverpool, UK (May 2014), http://intranet.csc.liv.ac.uk/research/techreports/?id=ULCS-14-001
de Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-Based Methods for Modal Logics. Logic Journal of the IGPL 8(3), 265–292 (2000)
Plaisted, D.A., Greenbaum, S.A.: A Structure-Preserving Clause Form Translation. Journal of Logic and Computation 2, 293–304 (1986)
Rao, A., Georgeff, M.: Modeling Rational Agents within a BDI-Architecture. In: Fikes, R., Sandewall, E. (eds.) Proceedings of KR&R-91, pp. 473–484. Morgan-Kaufmann (April 1991)
Schild, K.: A Correspondence Theory for Terminological Logics. In: Proceedings of the 12th IJCAI, pp. 466–471 (1991)
Schmidt, R.A., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Transactions on Computational Logic 8(4), 1–55 (2007)
Silva, G.B.: Implementação de um provador de teoremas por resolução para lógicas modais normais. Monografia de Conclusão de Curso, Bacharelado em Ciência da Computação, Universidade de Brasília (2013), http://www.cic.unb.br/~nalon/#software
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Nalon, C., Marcos, J., Dixon, C. (2014). Clausal Resolution for Modal Logics of Confluence. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-08587-6_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08586-9
Online ISBN: 978-3-319-08587-6
eBook Packages: Computer ScienceComputer Science (R0)