×

Positive logic with adjoint modalities: proof theory, semantics and reasoning about information. (English) Zbl 1337.03031

Abramsky, Samson (ed.) et al., Proceedings of the 25th conference on the mathematical foundations of programming semantics (MFPS 2009), Oxford, UK, April 3–7, 2009. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 249, 451-470 (2009).
Summary: We consider a simple modal logic whose non-modal part has conjunction and disjunction as connectives and whose modalities come in adjoint pairs, but are not in general closure operators. Despite absence of negation and implication, and of axioms corresponding to the characteristic axioms of (e.g.,) T, S4 and S5, such logics are useful, as shown in previous work by Baltag, Coecke and the first author, for encoding and reasoning about information and misinformation in multi-agent systems. For such a logic we present an algebraic semantics, using lattices with agent-indexed families of adjoint pairs of operators, and a cut-free sequent calculus. The calculus exploits operators on sequents, in the style of “nested” or “tree-sequent” calculi; cut-admissibility is shown by constructive syntactic methods. The applicability of the logic is illustrated by reasoning about the muddy children puzzle, for which the calculus is augmented with extra rules to express the facts of the muddy children scenario.
For the entire collection see [Zbl 1281.68012].

MSC:

03B45 Modal logic (including the logic of norms)
03B42 Logics of knowledge and belief (including belief change)
03G10 Logical aspects of lattices and related structures
03F05 Cut-elimination and normal-form theorems
68T27 Logic in artificial intelligence
68T42 Agent technology and artificial intelligence

Software:

Aximo
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baltag, A.; Coecke, B.; Sadrzadeh, M., Epistemic actions as resources, Journal of Logic and Computation, 17, 3, 555-585 (2007) · Zbl 1183.03010
[2] Baltag, A.; Moss, L. S., Logics for epistemic programs, Synthese, 139, 165-224 (2004) · Zbl 1100.03010
[3] Blackburn, P.; de Rijke, M.; Venema, Y., Modal Logic (2001), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0988.03006
[4] Belnap, N., Display Logic, Journal of Philosophical Logic, 11, 375-417 (1982) · Zbl 0509.03008
[5] Bonette, N.; Goré, R., A labelled sequent system for tense logic \(K_t\), (Australian Joint Conference on Artificial Intelligence. Australian Joint Conference on Artificial Intelligence, Lecture Notes in Computer Science, 1502 (1998)), 71-82 · Zbl 0928.03005
[6] Brünnler, K., Deep Sequent Systems for Modal Logic, Advances in Modal Logic, 6, 107-119 (2006) · Zbl 1150.03006
[7] Celani, S.; Jansana, R., Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic, Logic Journal of IGPL, 7, 683-715 (1999) · Zbl 0948.03013
[8] Davey, B. A.; Priestley, H. A., Introduction to Lattices and Order (1990), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0701.06001
[9] Dunn, M., Positive modal logic, Studia Logica, 55, 301-317 (2005) · Zbl 0831.03007
[10] Gehrke, M.; Nagahashi, H.; Venema, Y., A Sahlqvist theorem for distributive modal logic, Annals of Pure and Applied Logic, 131, 65-102 (2005) · Zbl 1077.03009
[11] Goré, R., Substructural Logics on Display, Logic Journal of the IGPL, 6, 451-504 (1998) · Zbl 0906.03020
[12] Huth, M.; Ryan, M., Logic in Computer Science (2000), Cambridge University Press: Cambridge University Press Cambridge
[13] von Karger, B., Temporal Algebras, Mathematical Structures in Computer Science, 8, 277-320 (1998) · Zbl 0917.03011
[14] Kashima, R., Cut-Free Sequent Calculi for Some Tense Logics, Studia Logica, 53, 119-135 (1994) · Zbl 0813.03012
[15] Kriener, J., M. Sadrzadeh and R. Dyckhoff, Implementation of a cut-free sequent calculus for logics with adjoint modalities; Kriener, J., M. Sadrzadeh and R. Dyckhoff, Implementation of a cut-free sequent calculus for logics with adjoint modalities
[16] Moortgat, M., Multimodal linguistic inference, Bull. IGPL, 3, 371-401 (1995) · Zbl 0840.03022
[17] Negri, S., Proof analysis in modal logic, Journal of Philosophical Logic, 34, 507-544 (2005) · Zbl 1086.03045
[18] Ono, H.; Komori, Y., Logics without the contraction rule, Journal of Symbolic Logic, 50, 169-201 (1985) · Zbl 0583.03018
[19] Prior, A., Time and Tense (1968), Oxford University Press
[20] Richards, S., and M. Sadrzadeh, Aximo: Automated Axiomatic Reasoning for Information UpdateElectronic Notes in Theoretical Computer Science; Richards, S., and M. Sadrzadeh, Aximo: Automated Axiomatic Reasoning for Information UpdateElectronic Notes in Theoretical Computer Science
[21] Sadrzadeh, M., Ockham’s Razor and Reasoning about Information Flow, SyntheseDOI: 10.1007/s11229-008-9414-7; Sadrzadeh, M., Ockham’s Razor and Reasoning about Information Flow, SyntheseDOI: 10.1007/s11229-008-9414-7
[22] Sadrzadeh, M.; Dyckhoff, R., Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information, [full version] · Zbl 1337.03031
[23] Sadrzadeh, M., “Actions and Resources in Epistemic Logic”, PhD Thesis, Université du Québec à Montréal, 2006. http://eprints.ecs.soton.ac.uk/12823/01/all.pdf; Sadrzadeh, M., “Actions and Resources in Epistemic Logic”, PhD Thesis, Université du Québec à Montréal, 2006. http://eprints.ecs.soton.ac.uk/12823/01/all.pdf
[24] Simpson, A., “The Proof Theory and Semantics of Intuitionistic Modal Logic”, PhD Thesis, University of Edinburgh, 1993; Simpson, A., “The Proof Theory and Semantics of Intuitionistic Modal Logic”, PhD Thesis, University of Edinburgh, 1993
[25] Troelstra, A.; Schwichtenberg, H., Basic Proof Theory (2001), CUP · Zbl 0957.03053
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.