LIPIcs.CSL.2017.15.pdf
- Filesize: 0.56 MB
- 15 pages
Document
Decidable Logics with Associative Binary Modalities
Author
-
Part of:
Volume:
26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-08-16
Cite As Get BibTex
Joseph Boudou. Decidable Logics with Associative Binary Modalities. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CSL.2017.15
Abstract
A new family of modal logics with an associative binary modality, called counting logics is proposed. These propositional logics allow to express finite cardinalities of sets and more generally to count the number of subsets satisfying some properties. We show that these logics can be seen both as specializations of the Boolean logic of bunched implications and as generalizations of the propositional dependence logic. Moreover, whereas most logics with an associative binary modality are undecidable, we prove that some counting logics are decidable, in particular the basic counting logic bCL. We conjecture that this interesting result is due to the valuation constraints in counting logics' semantics and prove that the logic corresponding to bCL without these constraints is undecidable. Finally, we give lower and upper bounds for the complexity of bCL's validity problem.
Subject Classification
Keywords
- modal logics
- abstract separation logics
- team semantics
- resource logics
- substructural logics
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Samson Abramsky and Jouko A. Väänänen. From IF to BI. Synthese, 167(2):207-230, 2009. URL: http://dx.doi.org/10.1007/s11229-008-9415-6.
- Robert Berger. The undecidability of the domino problem. Memoirs of the American Mathematical Society, 66, 1966. URL: http://dx.doi.org/10.1090/memo/0066.
- James Brotherston and Max I. Kanovich. Undecidability of propositional separation logic and its neighbours. In Logic in Computer Science - LICS, pages 130-139. IEEE Computer Society, 2010. URL: http://dx.doi.org/10.1109/LICS.2010.24.
- Cristiano Calcagno, Hongseok Yang, and Peter W. O'Hearn. Computability and complexity results for a spatial assertion language for data structures. In Foundations of Software Technology and Theoretical Computer Science - FSTTCS, volume 2245 of LNCS, pages 108-119. Springer, 2001. URL: http://dx.doi.org/10.1007/3-540-45294-X_10.
- Luca Cardelli and Andrew D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Symposium on Principles of Programming Languages - POPL, pages 365-377. ACM, 2000. URL: http://dx.doi.org/10.1145/325694.325742.
- David Harel. Recurring dominoes: Making the highly undecidable highly understandable (preliminary report). In Fundamentals of Computation Theory - FCT, volume 158 of LNCS, pages 177-194, 1983. URL: http://dx.doi.org/10.1007/3-540-12689-9_103.
- Wilfrid Hodges. Compositional semantics for a language of imperfect information. Logic Journal of the IGPL, 5(4):539-563, 1997. URL: http://dx.doi.org/10.1093/jigpal/5.4.539.
- Ágnes Kurucz, István Németi, Ildikó Sain, and András Simon. Decidable and undecidable logics with a binary modality. Journal of Logic, Language and Information, 4(3):191-206, 1995. URL: http://dx.doi.org/10.1007/BF01049412.
- Dominique Larchey-Wendling and Didier Galmiche. The undecidability of boolean BI through phase semantics. In Logic in Computer Science - LICS, pages 140-149. IEEE Computer Society, 2010. URL: http://dx.doi.org/10.1109/LICS.2010.18.
-
Leopold Löwenheim. Über möglichkeiten im relativkalkül. Mathematische Annalen, 76(4):447-470, 1915. translated in [15].
- Derek C. Oppen. A 2^2^2^pn upper bound on the complexity of presburger arithmetic. Journal of Computer and System Sciences, 16(3):323-332, 1978. URL: http://dx.doi.org/10.1016/0022-0000(78)90021-1.
- Paritosh K. Pandya. Some extensions to propositional mean-value caculus: Expressiveness and decidability. In Computer Science Logic - CSL, volume 1092 of LNCS, pages 434-451. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-61377-3_52.
-
David J Pym. The semantics and proof theory of the logic of bunched implications, volume 26 of Applied Logic Series. Kluwer Academic Publishers, 2002.
- John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science - LICS, pages 55-74. IEEE Computer Society, 2002. URL: http://dx.doi.org/10.1109/LICS.2002.1029817.
-
Jean van Heijenoort. From Frege to Gödel: a source book in mathematical logic, 1879-1931, volume 9. Harvard University Press, 1967.
- Yde Venema. A modal logic for chopping intervals. Journal of Logic and Computation, 1(4):453-476, 1991. URL: http://dx.doi.org/10.1093/logcom/1.4.453.
- Jonni Virtema. Complexity of validity for propositional dependence logics. In Games, Automata, Logics and Formal Verification - GandALF, volume 161 of EPTCS, pages 18-31, 2014. URL: http://dx.doi.org/10.4204/EPTCS.161.5.
- Fan Yang and Jouko Väänänen. Propositional logics of dependence. Annals of Pure and Applied Logic, 167(7):557-589, 2016. URL: http://dx.doi.org/10.1016/j.apal.2016.03.003.
- Fan Yang and Jouko Väänänen. Propositional team logics. Annals of Pure and Applied Logic, 2017. URL: http://dx.doi.org/10.1016/j.apal.2017.01.007.