Bunched sequential information. (English) Zbl 1436.03144
Summary: It is known that the logic BI of bunched implications is a logic of resources. Many studies have reported on the applications of BI to computer science. In this paper, an extension BIS of BI by adding a sequence modal operator is introduced and studied in order to formalize more fine-grained resource-sensitive reasoning. By the sequence modal operator of BIS, we can appropriately express “sequential information” in resource-sensitive reasoning. A Gentzen-type sequent calculus SBIS for BIS is introduced, and the cut-elimination and decidability theorems for SBIS are proved. An extension of the Grothendieck topological semantics for BI is introduced for BIS, and the completeness theorem with respect to this semantics is proved. The cut-elimination, decidability and completeness theorems for SBIS and BIS are proved using some theorems for embedding BIS into BI.
MSC:
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 03B45 | Modal logic (including the logic of norms) |
| 03B70 | Logic in computer science |
| 03F05 | Cut-elimination and normal-form theorems |
| 03B25 | Decidability of theories and sets of sentences |
Keywords:
logic BI of bunched implications; sequential information; completeness theorem; cut-elimination theoremReferences:
| [1] | Cégielski, P.; Richard, D., On arithmetical first-order theories allowing encoding and decoding of lists, Theor. Comput. Sci., 22, 1-2, 55-75 (1999) · Zbl 0930.68032 |
| [2] | Collinson, M.; Monahan, B.; Pym, D. J., A logical and computational theory of located resource, J. Log. Comput., 19, 6, 1207-1244 (2009) · Zbl 1185.68440 |
| [3] | Collinson, M.; Pym, D. J., Algebra and logic for resource-based systems modelling, Math. Struct. Comput. Sci., 19, 5, 959-1027 (2009) · Zbl 1185.68441 |
| [4] | Dunn, J. M., Relevance logic and entailment, (Gabbay, D.; Guenthner, F., Handbook of Philosophical Logic, vol. 3 (1986), Reidel Publishing Company), 117-224 · Zbl 0875.03051 |
| [5] | Galmiche, D.; Méry, D., Semantic labelled tableaux for propositional \(BI^⊥\), J. Log. Comput., 13, 5, 707-753 (2003) · Zbl 1041.03047 |
| [6] | Galmiche, D.; Méry, D.; Pym, D. J., The semantics of BI and resource tableaux, Math. Struct. Comput. Sci., 15, 6, 1033-1088 (2005) · Zbl 1145.03308 |
| [7] | Girard, J.-Y., Linear logic, Theor. Comput. Sci., 50, 1-102 (1987) · Zbl 0625.03037 |
| [8] | Harland, J.; Pym, D. J., Resource-distribution via Boolean constraints, ACM Trans. Comput. Log., 4, 1, 56-90 (2003) · Zbl 1407.03078 |
| [9] | Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021 |
| [10] | Ishtiaq, S. S.; O’Hearn, P. W., BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM SIGPLAN Not., 36, 3, 14-26 (2001) · Zbl 1323.68077 |
| [11] | Kamide, N., Linear and affine logics with temporal, spatial and epistemic operators, Theor. Comput. Sci., 353, 1-3, 165-207 (2006) · Zbl 1175.03039 |
| [12] | Kamide, N., Dynamic non-commutative logic, J. Log. Lang. Inf., 19, 1, 33-51 (2010) · Zbl 1193.03062 |
| [13] | Kamide, N., A proof system for temporal reasoning with sequential information, (Proceedings of the 20th Brazilian Symposium on Artificial Intelligence (SBIA’10). Proceedings of the 20th Brazilian Symposium on Artificial Intelligence (SBIA’10), Lecture Notes in Computer Science, vol. 6404 (2010)), 283-292 |
| [14] | Kamide, N., The logic of sequences, Rep. Math. Log., 46, 29-57 (2011) · Zbl 1261.03086 |
| [15] | Kamide, N., Temporal BI: proof system, semantics and translations, Theor. Comput. Sci., 492, 40-69 (2013) · Zbl 1296.03014 |
| [16] | Kamide, N.; Kaneiwa, K., 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). Proceedings of the 22nd Australasian Joint Conference on Artificial Intelligence (AI’09), Lecture Notes in Artificial Intelligence, vol. 5866 (2009)), 485-494 |
| [17] | Kamide, N.; Kaneiwa, K., Resource-sensitive reasoning with sequential information, (Proceedings of the 23rd Australasian Joint Conference on Artificial Intelligence (AI’10). Proceedings of the 23rd Australasian Joint Conference on Artificial Intelligence (AI’10), Lecture Notes in Artificial Intelligence, vol. 6464 (2010)), 22-31 |
| [18] | Kamide, N.; Kaneiwa, K., Reasoning about resources and information: a linear logic approach, Fundam. Inform., 125, 1, 51-70 (2013) · Zbl 1315.03044 |
| [19] | Kaneiwa, K.; Kamide, N., Sequence-indexed linear-time temporal logic: proof system and application, Appl. Artif. Intell., 24, 896-913 (2010) |
| [20] | Kaneiwa, K.; Kamide, N., Conceptual modeling in full computation-tree logic with sequence modal operator, Int. J. Intell. Syst., 26, 7, 636-651 (2011) |
| [21] | Mac Lane, S.; Moerdijk, I., Sheaves in Geometry and Logic: A First Introduction to Topos Theory, Universitext (1994), Springer |
| [22] | O’Hearn, P. W., On bunched typing, J. Funct. Program., 13, 4, 747-796 (2003) · Zbl 1056.03013 |
| [23] | O’Hearn, P. W.; Pym, D. J., The logic of bunched implications, Bull. Symb. Log., 5, 2, 215-244 (1999) · Zbl 0930.03095 |
| [24] | Pym, D. J., The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series, vol. 26 (2002), Kluwer Academic Publishers · Zbl 1068.03001 |
| [25] | Pym, D. J.; O’Hearn, P. W.; Yang, H., Possible worlds and resources: the semantics of BI, Theor. Comput. Sci., 315, 1, 257-305 (2004) · Zbl 1055.03021 |
| [26] | Pym, D. J.; Tofts, C. M.N., A calculus and logic of resources and processes, Form. Asp. Comput., 18, 4, 495-517 (2006) · Zbl 1111.68086 |
| [27] | Pym, D. J.; Tofts, C. M.N., Systems modelling via resources and processes: philosophy, calculus, semantics, and logic, Electron. Notes Theor. Comput. Sci., 172, 545-587 (2007) · Zbl 1277.68202 |
| [28] | Reynolds, J. C., Separation logic: a logic for shared mutable data structures, (Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (2002)), 55-74 |
| [29] | Russell, S.; Norvig, P., Artificial Intelligence: A Modern Approach (2003), Pearson Education, Inc. |
| [30] | Slaney, J., Solution to a problem of Ono and Komori, J. Philos. Log., 18, 103-111 (1989) · Zbl 0671.03036 |
| [31] | Wansing, H., The Logic of Information Structures, Lecture Notes in Artificial Intelligence, vol. 681 (1993), 163 pp · Zbl 0788.03001 |
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.
