Temporal non-commutative logic: Expressing time, resource, order and hierarchy
DOI:
https://doi.org/10.12775/LLP.2009.007Keywords
Keywords, temporal non-commutative logic, cut-elimination, sequent calculus, completeness, decidabilityAbstract
A first-order temporal non-commutative logic TN[l], which has no structural rules and has some l-bounded linear-time temporal operators, is introduced as a Gentzen-type sequent calculus. The logic TN[l] allows us to provide not only time-dependent, resource-sensitive, ordered, but also hierarchical reasoning. Decidability, cut-elimination and completeness (w.r.t. phase semantics) theorems are shown for TN[l]. An advantage of TN[l] is its decidability, because the standard first-order linear-time temporal logic is undecidable. A correspondence theorem between TN[l] and a resource indexed non-commutative logic RN[l] is also shown. This theorem is intended to state that “time” is regarded as a “resource”.References
Abrusci, V.M., “Non-commutative intuitionistic linear logic”, Ztschr. f. Math. Logik 36 (1990): 297–318.
Baratella, S., and A. Masini, “An approach to infinitary temporal proof theory”, Archive for Mathematical Logic 43, 8 (2004): 965–990.
Biere, A., A. Cimatti, E.M. Clarke, O. Strichman and Y. Zhu, “Bounded model checking”, Advances in Computers 58 (2003): 118–149.
Cerrito, S., M.C. Mayer and S. Prand, “First order linear temporal logic over finite time structures”, pp. 62–76 in: Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR’99), Lecture Notes in Computer Science 1705, Springer-Verlag, Berlin, 1999.
Girard, J.-Y., “Linear logic”, Theoretical Computer Science 50 (1987): 1–102.
Hodkinson, I., F. Wolter and M. Zakharyaschev, “Decidable fragments of first-order temporal logics”, Annals of Pure and Applied Logic 106 (2000): 85–134.
Kamide, N., “Linear and affine logics with temporal, spatial and epistemic operators”, Theoretical Computer Science 353, 1–3 (2006): 165–207.
Kamide, N., “An equivalence between sequent calculi for linear-time temporal logic”, Bulletin of the Section of the Logic 35, 4 (2006): 187–194.
Kamide, N., “A uniform proof-theoretic foundation for abstract paraconsistent logic programming”, Journal of Functional and Logic Programming, 2007.
Kamide, N., “Linear exponentials as resource operators: A decidable first-order linear logic with bounded exponentials”, pp. 245–257 in: Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA2008), Lecture Notes in Artificial Intelligence 5293, 2008.
Kamide, N., “Embedding linear-time temporal logic into infinitary logic: Application to cut-elimination for multi-agent infinitary epistemic linear-time temporal logic”, pp. 57–76 in Proceedings of the 9th International Workshop on Computational Logic in Multi-agent Systems (CLIMA-9), Lecture Notes in Artificial Intelligence 5405, 2009.
Kawai, H., “Sequential calculus for a first order infinitary temporal logic”, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33 (1987): 423–432.
Komori, Y., “Predicate logics without the structure rules”, Studia Logica 45 (1986): 393–404.
Kröger, F., “LAR: a logic of algorithmic reasoning”, Acta Informatica 8 (1977): 243–266.
Lambek, J., “The mathematics of sentence structure”, The American Mathematical Monthly 65 (1958): 154–170.
Okada, M., “A uniform semantic proof for cut-elimination and completeness of various first and higher order logics”, Theoretical Computer Science 281 (2002): 471–498.
Pym, D.J., P.W. O’Hearn and H. Yang, “Possible worlds and resources: The semantics of BI”, Theoretical Computer Science 315, 1 (2004): 257–305.
Russell, S., and P. Norvig, Artificial intelligence: A modern approach (Second edition), Pearson Education, Inc., 2003.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 581
Number of citations: 0
