Interpolation theorems for some variants of LTL

• Autorzy: Kamide N.

Identyfikatory

DOI

10.4467/20842589RM.15.001.3910

• Języki publikacji: EN

Abstrakty

EN

It is known that Craig interpolation theorem does not hold for LTL. In this paper, Craig interpolation theorems are shown for some fragments and extensions of LTL. These theorems are simply proved based on an embedding-based proof method with Gentzen-type sequent calculi. Maksimova separation theorems (Maksimova principle of variable separation) are also shown for these LTL variants.

Słowa kluczowe

EN

Craig interpolation theorem; linear-time temporal logic; infinitary logic; paraconsistent logic; sequent calculus

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2015
• Tom: Vol. 50
• Strony: 3--30
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Kamide N.

• Teikyo University Faculty of Science and Engineering Department of Information and Electronic Engineering Toyosatodai 1-1, Utsunomiya-shi, Tochigi 320-8551, Japan

Bibliografia

• [1] A. Almukdad and D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic 49 (1984), 231–233.
• [2] S. Baratella and A. Masini, An approach to infinitary temporal proof theory, Archive for Mathematical Logic 43:8 (2004), 965–990.
• [3] W. Craig, Three uses of the Herbrand-Gentzen theorems in relating model theory and proof theory, Journal of Symbolic Logic 22:3 (1957), 269–285.
• [4] E.M. Clarke, O. Grumberg, and D.A. Peled, Model checking, The MIT Press, 1999.
• [5] A. Gheerbrant and B. ten Cate, Craig interpolation for linear temporal languages, Proceedings of the 23rd International Conference on Computer Science Logic, Lecture Notes in Computer Science 5771, 2009, pp. 287–301.
• [6] Y. Gurevich, Intuitionistic logic with strong negation, Studia Logica 36 (1977), pp.49–59.
• [7] N. Kamide, An equivalence between sequent calculi for linear-time temporal logic, Bulletin of the Section of the Logic 35:4 (2006), 187–194.
• [8] N. Kamide, Embedding linear-time temporal logic into infinitary logic: Application to cut-elimination for multi-agent infinitary epistemic linear-time temporal logic, Lecture Notes in Artificial Intelligence 5405, 2009, pp. 57–76.
• [9] N. Kamide, Notes on Craig interpolation for LJ with strong negation, Mathematical Logic Quarterly 57:4 (2011), 395–399.
• [10] N. Kamide, Bounded linear-time temporal logic: A proof-theoretic investigation, it Annals of Pure and Applied Logic 163:4 (2012), 439–466.
• [11] N. Kamide and H. Wansing, A paraconsistent linear-time temporal logic, Fundamenta Infomaticae 106:1 (2011), 1–23.
• [12] H. Kawai, Sequential calculus for a first order infinitary temporal logic, Zeitschrift f¨ur Mathematische Logik und Grundlagen der Mathematik 33 (1987), 423–432.
• [13] B. Knov, D. Walther and F. Wolter, Forgetting and uniform interpolation in largescale description logic terminologies, Proceedings of the 21st International Joint Conference on Artificial Intelligence, 2009, pp. 830–835.
• [14] E.G.K. Lopez-Escobar, An interpolation theorem for denumerably long sentences, Fund. Math. 57 (1965), 253–272.
• [15] S. Maehara, Craig interpolation theorem (in Japanese), Suugaku 12 (1960), 235–237.
• [16] L. Maksimova, The principle of separation of variables in propositional logics, Algebra i Logika 15 (1976), 168–184.
• [17] L.L. Maksimova, Temporal logics with “the next” operator do not have interpolation or Beth property, Siberian Mathematical Journal 32:6 (1991), 989–993.
• [18] J. Malitz, Infinitary analogues of theorems from first-order model theory, Journal of Symbolic Logic 36 (1971), 216–228.
• [19] K. L. McMillan, Applications of Craig interpolants in model checking, The 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACS), Lecture Notes in Computer Science 3440, 2005, pp. 1–12.
• [20] D. Nelson, Constructible falsity, Journal of Symbolic Logic 14 (1949), 16–26.
• [21] A. Pnueli, The temporal logic of programs, Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, 1977, pp. 46–57.
• [22] W. Rautenberg, Klassische und nicht-klassische Aussagenlogik, Vieweg, Braunschweig, 1979.
• [23] G. Takeuti, Proof theory, North-Holland Pub. Co., 1975.
• [24] N. Vorob’ev, A constructive propositional logic with strong negation (in Russian), Doklady Akademii Nauk SSSR 85 (1952), 465–468.