The Logic of Sequences

Norihiro Kamide


The notion of “sequences” is fundamental to practical reasoning in computer science, because it can appropriately represent “data (information) sequences”, “program (execution) sequences”, “action sequences”, “time sequences”, “trees”, “orders” etc. The aim of this paper is thus to provide a basic logic for reasoning with sequences. A propositional modal logic LS of sequences is introduced as a Gentzen-type sequent calculus by extending Gentzen’s LK for classical propositional logic. The completeness theorem with respect to a sequence-indexed semantics for LS is proved, and the cut-elimination theorem for LS is shown. Moreover, a first-order modal logic FLS of sequences, which is a first-order extension of LS, is introduced. The completeness theorem with respect to a first-order sequence-indexed semantics for FLS is proved, and the cut-elimination theorem for FLS is shown. LS and the monadic fragment of FLS are shown to be decidable.

[1] M. Bezem, T. Langholm and M. Walicki, Completeness and decidability in sequence logic, Proceedings of the 14-th International Conference on Logic for programming, artificial intelligence, and reasoning (LPAR 2007), N. Dershowitz and A. Voronkov (Eds.), Lecture Notes in Computer Science 4790 (2007), pp. 123–137. 
[2] R.A. Bull, Cut elimination for propositional dynamic logic without *, Zeitscr. f. Math. Logik und Grundlagen d. Math., 38 (1992), pp. 85–100. 
[3] P. C´egielski and D. Richard, On arithmetical first-order theories allowing encoding and decoding of lists, Theoretical Computer Science 22 (1-2) (1999), pp. 55–75. 
[4] S. Giambrone and A. Urquhart, Proof theories for semilattice logics, Zeitschrift fu¨r Mathematische Logik und Grundlagen der Mathematik 33 (1987), pp. 433–439. 
[5] E.A. Emerson, Temporal and modal logic, In: Handbook of Theoretical Computer Science, Formal Models and Semantics (B), Jan van Leeuwen (Ed.), Elsevier and MIT Press, 1990, pp. 995–1072. 
[6] D. Harel, D. Kozen and J. Tiuryn, Dynamic logic (Foundations of Computing Series), The MIT Press, 2000.
[7] N. Kamide, Dynamic non-commutative logic, Journal of Logic, Language and Information 19 (1) (2010), pp. 33–51.
[8] N. Kamide and K. Kaneiwa, Extended full computation-tree logic with sequence modal operator: Representing hierarchical tree structures, Proceedings of the 22nd Australasian Joint Conference on Artificial Intelligence (AI’09), Lecture Notes in Artificial Intelligence 5866 (2009), pp. 485–494.
[9] R. Kashima, On semilattice relevant logics, Mathematical Logic Quarterly 49(4) (2003), pp. 401–414.
[10] T. Kutsia and B. Buchberger, Predicate logic with sequence variables and sequence function symbols, Proceedings of the 3rd International Conference on Mathematical Knowledge Management (MKM 2004), A. Asperti, G. Bancerek and A. Trybulec (Eds.), Lecture Notes in Computer Science 3119 (2004), pp. 205–219.
[11] J. Lambek, The mathematics of sentence structure, The American Mathematical Monthly 65, pp. 154-170, 1958.
[12] A.N. Prior, Past, present and future, Oxford: Clarendon Press, 1967.
[13] J.C. Reynolds, Separation logic: A logic for shared mutable data structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 55–74.
[14] A. Urquhart, Semantics for relevant logics, Journal of Symbolic Logic 37(1) (1972), pp. 159–169.
[15] M. Walicki, M. Bezem and W. Szajnkenig, A strongly complete logic of dense time intervals, Proceedings of the Workshop on Logics for Resource-Bounded Agents, ESSLLI, Malaga, Spain, 2006.
[16] H. Wansing, The logic of information structures, Lecture Notes in Artificial Intelligence 681 (1993), 163 pages.

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.