Abstract
We present a software tool for reasoning in and about propositional sequent calculi for modal logics of actions. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. The tool generates embeddings of the calculus in the theorem prover Isabelle/HOL for formalising proofs about D.EAK. Integrating propositional reasoning in D.EAK with inductive reasoning in Isabelle/HOL, we verify the solution of the muddy children puzzle for any number of muddy children. There also is a set of meta-tools that allows us to adapt the software for a wide variety of user defined calculi.
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
Similar content being viewed by others
Notes
- 1.
For example, taking into account the correspondence between operational and structural connectives, the rule \((;,>)\) above says precisely that the operation that maps C to \(A\rightarrow C\) is right-adjoint to the operation that maps B to \(A\wedge B\). Similarly, \((>,;)\) expresses that
is left adjoint to \(A\vee \_\). - 2.
which implies that one can derive \(\langle \upalpha \rangle X\vdash [\upalpha ] X\).
- 3.
which implies that one can derive \([\texttt {a}] Y\vdash Y\).
- 4.
Compiled version available for download at: https://github.com/goodlyrottenapple/calculus-toolbox/raw/master/calculi/DEAK.jar.
- 5.
It is at this point where our implementation of the deep embedding is currently tailored towards substructural logics: For each rule r and each sequent s, there is only one list of premises to consider. Generalising the deep embedding to sequent calculi with rules such as (2) would require a modification: If we interpret the structure \(W,X,A\vee B\) in (2) not as a structure (i.e. tree) but as a list, then matching the rule (2) against a sequent would typically not determine the sublists matching W and X in a unique way. More information is available at [3].
- 6.
The presence of the \\ instead of just one \ is unfortunate but \ is a reserved character that needs to be escaped using \.
is left adjoint to References
Aucher, G., Schwarzentruber, F.: On the complexity of dynamic epistemic logic. In: Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2013)
Balbiani, P., van Ditmarsch, H., Herzig, A., de Lima, T.: Tableaux for public announcement logic. J. Logic Comput. 20(1), 55–76 (2010)
Balco, S.: The calculus toolbox. https://goodlyrottenapple.github.io/calculus-toolbox/
Balco, S.: The calculus toolbox 2. https://github.com/goodlyrottenapple/calculus-toolbox-2
Balco, S., Frittella, S.: Muddy children in Isabelle. https://goodlyrottenapple.github.io/muddy-children/
Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements, common knowledge and private suspicious. Technical Report SEN-R9922, CWI, Amsterdam (1999)
Belnap, N.: Display logic. J. Philos. Logic 11, 375–417 (1982)
Blackburn, P., van Benthem, J., Wolter, F. (eds.): Handbook of Modal Logic. Elsevier, Amsterdam (2006)
Brotherston, J.: Bunched logics displayed. Stud. Logica. 100(6), 1223–1254 (2012)
Ciabattoni, A., Galatos, N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008)
Ciabattoni, A., Ramanayake, R.: Power and limits of structural display rules. ACM Trans. Comput. Logic (TOCL) 17(3), 17 (2016)
Ciabattoni, A., Ramanayake, R., Wansing, H.: Hypersequent and display calculi - a unified perspective. Stud. Logica. 102(6), 1245–1294 (2014)
Dawson, J.E., Goré, R.: Embedding display calculi into logical frameworks: comparing twelf and Isabelle. Electr. Notes Theor. Comput. Sci. 42, 89–103 (2001)
Dawson, J.E., Goré, R.: Formalised cut admissibility for display logic. In: Proceedings of 15th International Conference Theorem Proving in Higher Order Logics, TPHOLs (2002)
Dyckhoff, R., Sadrzadeh, M., Truffaut, J.: Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators. ACM Trans. Comput. Logic 14(4), 1–37 (2013)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Fitting, M.: Proof Methods for Modal and Intuitionistic Logic. Springer, Netherlands (1983). https://doi.org/10.1007/978-94-017-2794-5
Frittella, S., Greco, G., Kurz, A., Palmigiano, A.: Multi-type display calculus for propositional dynamic logic. J. Log. Comput. 26(6), 2067–2104 (2016)
Frittella, S., Greco, G., Kurz, A., Palmigiano, A., Sikimic, V.: Multi-type display calculus for dynamic epistemic logic. J. Log. Comput. 26(6), 2017–2065 (2016)
Frittella, S., Greco, G., Kurz, A., Palmigiano, A., Sikimić, V.: Multi-type sequent calculi. In: Andrzej Indrzejczak, M.Z., Kaczmarek, J. (ed.) Trends in Logic XIII, pp. 81–93. Lodź University Press (2014). https://arxiv.org/abs/1609.05343
Frittella, S., Greco, G., Palmigiano, A., Yang, F.: A multi-type calculus for inquisitive logic. In: Väänänen, J., Hirvonen, Å., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 215–233. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-52921-8_14
Frittella, S., Greco, G., Kurz, A., Palmigiano, A., Sikimic, V.: A proof-theoretic semantic analysis of dynamic epistemic logic. J. Log. Comput. 26(6), 1961–2015 (2016)
Goré, R.: Substructural logics on display. Logic J. IGPL 6(3), 451–504 (1998)
Goré, R.: Tableau methods for modal and temporal logics. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods. Springer, Dordrecht (1999). https://doi.org/10.1007/978-94-017-1754-0_6
Greco, G., Ma, M., Palmigiano, A., Tzimoulis, A., Zhao, Z.: Unified correspondence as a proof-theoretic tool. J. Log. Comput. (2016). https://doi.org/10.1093/logcom/exw022
Greco, G., Palmigiano, A.: Linear logic properly displayed. CoRR, abs/1611.04181 (2016)
Greco, G., Palmigiano, A.: Lattice logic properly displayed. In: Kennedy, J., de Queiroz, R.J.G.B. (eds.) WoLLIC 2017. LNCS, vol. 10388, pp. 153–169. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55386-2_11
Greco, G., Liang, F., Moshier, M.A., Palmigiano, A.: Multi-type display calculus for semi de morgan logic. In: Kennedy, J., de Queiroz, R.J.G.B. (eds.) WoLLIC 2017. LNCS, vol. 10388, pp. 199–215. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55386-2_14
Halpern, J.Y., Vardi, M.Y.: Model checking vs. theorem proving: a manifesto. In: Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), pp. 325–334 (1991)
Kracht, M.: Power and weakness of the modal display calculus. In: Proof Theory of Modal Logic, pp. 93–121. Kluwer, Netherlands (1996)
Lescanne, P.: Mechanizing common knowledge logic using COQ. Ann. Math. Artif. Intell. 48(1–2), 15–43 (2006)
Lescanne, P.: Common knowledge logic in a higher order proof assistant. In: Programming Logics - Essays in Memory of Harald Ganzinger, pp. 271–284 (2013)
Lescanne, P., Puisségur, J.: Dynamic logic of common knowledge in a proof assistant. CoRR, abs/0712.3146 (2007)
Ma, M., Palmigiano, A., Sadrzadeh, M.: Algebraic semantics and model completeness for intuitionistic public announcement logic. Ann. Pure Appl. Logic 165(4), 963–995 (2014)
Ma, M., Sano, K., Schwarzentruber, F., Velázquez-Quesada, F.R.: Tableaux for non-normal public announcement logic. In: Banerjee, M., Krishna, S.N. (eds.) ICLA 2015. LNCS, vol. 8923, pp. 132–145. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-45824-2_9
Piecha, T., Schroeder-Heister, P., (eds.): Advances in Proof-Theoretic Semantics. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-22686-6
Restall, G.: An Introduction to Substructural Logics. Routledge, London (2000)
Schroeder-Heister, P.: Proof-theoretic semantics. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2016 edition (2016)
Truffaut, J.: Implementation and improvements of a cut-free sequent calculus for dynamic epistemic logic. M.Sc. thesis, University of Oxford (2011)
van Ditmarsch, H., van Eijck, J., Hernández-Antón, I., Sietsma, F., Simon, S., Soler-Toscano, F.: Modelling cryptographic keys in dynamic epistemic logic with DEMO. In: Proceedings of 10th International Conference on Practical Applications of Agents and Multi-Agent Systems, PAAMS (2012)
van Ditmarsch, H.P., Kooi, B.: One Hundred Prisoners and a Light Bulb. Springer, Switzerland (2015). https://doi.org/10.1007/978-3-319-16694-0
van Ditmarsch, H.P., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic, Springer, Netherlands (2007). https://doi.org/10.1007/978-1-4020-5839-4
Wansing, H.: Displaying Modal Logic. Kluwer, Netherlands (1998)
Acknowledgements
At several crucial points, we profited from expert advice on Isabelle by Tom Ridge, Thomas Tuerk and Christian Urban. We thank Roy Crole and Hans van Ditmarsch for valuable comments on an earlier draft.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Balco, S., Frittella, S., Greco, G., Kurz, A., Palmigiano, A. (2018). Software Tool Support for Modular Reasoning in Modal Logics of Actions. In: Avigad, J., Mahboubi, A. (eds) Interactive Theorem Proving. ITP 2018. Lecture Notes in Computer Science(), vol 10895. Springer, Cham. https://doi.org/10.1007/978-3-319-94821-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-94821-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94820-1
Online ISBN: 978-3-319-94821-8
eBook Packages: Computer ScienceComputer Science (R0)