Abstract
Temporal logics and their intuitionistic counterparts are of growing importance in Computer Science. These intuitionistic counterparts, called intuitionistic (or constructive) temporal logics, are known to be useful for formalizing functional programming. To show a clear relationship between temporal logics and their intuitionistic counterparts has thus been required. In this paper, a theorem for embedding first-order linear-time temporal logic into its intuitionistic counterpart is proved using Baratella-Masini’s temporal extension of the Gödel-Gentzen negative translation of classical logic into intuitionistic logic.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Baratella, S., Masini, A.: A proof-theoretic investigation of a logic of positions. Annals of Pure and Applied Logic 123, 135–162 (2003)
Baratella, S., Masini, A.: An approach to infinitary temporal proof theory. Archive for Mathematical Logic 43(8), 965–990 (2004)
Ishihara, H.: A note on the Gödel-Gentzen translation. Mathematical Logic Quarterly 46(1), 135–137 (2000)
Kamide, N.: An equivalence between sequent calculi for linear-time temporal logic. Bulletin of the Section of the Logic 35(4), 187–194 (2006)
Kamide, N., Wansing, H.: Combining linear-time temporal logic with constructiveness and parconsistency. Journal of Applied Logic 8, 33–61 (2010)
Kawai, H.: Sequential calculus for a first order infinitary temporal logic. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33, 423–432 (1987)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)
Troelstra, A.S., van Dalen, D.: Constructivism in mathematics, vol. 1. North-Holland Publishing Company, Amsterdam (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kamide, N. (2011). On Temporal Gödel-Gentzen Translation. In: König, A., Dengel, A., Hinkelmann, K., Kise, K., Howlett, R.J., Jain, L.C. (eds) Knowlege-Based and Intelligent Information and Engineering Systems. KES 2011. Lecture Notes in Computer Science(), vol 6882. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23863-5_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-23863-5_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23862-8
Online ISBN: 978-3-642-23863-5
eBook Packages: Computer ScienceComputer Science (R0)