{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:00:58Z","timestamp":1747173658193,"version":"3.40.5"},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2021,4,22]],"date-time":"2021-04-22T00:00:00Z","timestamp":1619049600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2021,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The importance of intuitionistic temporal logics in Computer Science and Artificial Intelligence has become increasingly clear in the last few years. From the proof-theory point of view, intuitionistic temporal logics have made it possible to extend functional programming languages with new features via type theory, while from the semantics perspective, several logics for reasoning about dynamical systems and several semantics for logic programming have their roots in this framework. We consider several axiomatic systems for intuitionistic linear temporal logic and show that each of these systems is sound for a class of structures based either on Kripke frames or on dynamic topological systems. We provide two distinct interpretations of \u201chenceforth\u201d, both of which are natural intuitionistic variants of the classical one. We completely establish the order relation between the semantically defined logics based on both interpretations of \u201chenceforth\u201d and, using our soundness results, show that the axiomatically defined logics enjoy the same order relations.<\/jats:p>","DOI":"10.1017\/s1471068421000089","type":"journal-article","created":{"date-parts":[[2021,4,22]],"date-time":"2021-04-22T13:26:03Z","timestamp":1619097963000},"page":"459-492","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["Exploring the Jungle of Intuitionistic Temporal Logics"],"prefix":"10.1017","volume":"21","author":[{"given":"JOSEPH","family":"BOUDOU","sequence":"first","affiliation":[]},{"given":"MART\u00cdN","family":"DI\u00c9GUEZ","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8604-4183","authenticated-orcid":false,"given":"DAVID","family":"FERN\u00c1NDEZ-DUQUE","sequence":"additional","affiliation":[]},{"given":"PHILIP","family":"KREMER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,4,22]]},"reference":[{"key":"S1471068421000089_ref35","doi-asserted-by":"publisher","DOI":"10.2307\/2267135"},{"key":"S1471068421000089_ref4","unstructured":"Boudou, J. , Di\u00e9guez, M. and Fern\u00e1ndez-Duque, D. 2017. A decidable intuitionistic temporal logic. In 26th EACSL Annual Conference on Computer Science Logic (CSL), Vol. 82, 14:1\u201314:17."},{"key":"S1471068421000089_ref19","unstructured":"Fischer Servi, G. 1984. Axiomatisations for some intuitionistic modal logics. In Rendiconti del Seminario Matematico, Vol. 42. Universitie Politecnico Torino, 179\u2013194."},{"key":"S1471068421000089_ref32","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.1.55"},{"key":"S1471068421000089_ref16","first-page":"77","article-title":"Dynamic topological completeness for 2","volume":"1","author":"Fern\u00e1ndez-Duque","year":"2007","journal-title":"Logic Journal of the IGPL 15"},{"key":"S1471068421000089_ref33","doi-asserted-by":"crossref","unstructured":"Maier, P. 2004. Intuitionistic LTL and a new characterization of safety and liveness. In 18th EACSL Annual Conference on Computer Science Logic (CSL), Marcinkowski, J. and Tarlecki, A. , Eds. Springer Berlin Heidelberg, Berlin, Heidelberg, 295\u2013309.","DOI":"10.1007\/978-3-540-30124-0_24"},{"key":"S1471068421000089_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043195"},{"key":"S1471068421000089_ref24","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"Howard","year":"1980"},{"key":"S1471068421000089_ref40","unstructured":"Simpson, A. K. 1994. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh, UK."},{"key":"S1471068421000089_ref12","unstructured":"Davoren, J. M. , Coulthard, V. , Moor, T. , Gor, R. and Nerode, A. 2002. Topological semantics for intuitionistic modal logics, and spatial discretisation by A\/D maps. In Workshop on Intuitionistic Modal Logic and Applications (IMLA)."},{"key":"S1471068421000089_ref2","first-page":"2","article-title":"Intuitionistic linear temporal logics","author":"Balbiani","year":"2019","journal-title":"Transactions on Computational Logic 21"},{"key":"S1471068421000089_ref23","unstructured":"Heyting, A. 1930. Die formalen regeln der intuitionistischen logik. In Sitzungsberichte der preu\u00c3\u0178ischen Akademie der Wissenschaften. Physikalisch-mathematische Klasse, 42\u201356."},{"key":"S1471068421000089_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/S1755020313000087"},{"key":"S1471068421000089_ref36","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn034"},{"key":"S1471068421000089_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(77)90078-3"},{"key":"S1471068421000089_ref1","first-page":"501","article-title":"Diskrete R\u00e4ume","volume":"44","author":"Aleksandroff","year":"1937","journal-title":"Matematicheskii Sbornik 2"},{"key":"S1471068421000089_ref42","doi-asserted-by":"publisher","DOI":"10.4064\/fm-31-1-103-134"},{"key":"S1471068421000089_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2009.06.001"},{"key":"S1471068421000089_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"S1471068421000089_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.07.009"},{"key":"S1471068421000089_ref17","first-page":"308","article-title":"Dynamic topological logic interpreted over metric spaces","author":"Fern\u00e1ndez-Duque","year":"2011","journal-title":"Journal of Symbolic Logic"},{"key":"S1471068421000089_ref18","first-page":"1","article-title":"The intuitionistic temporal logic of dynamical systems","volume":"3","author":"Fern\u00e1ndez-Duque","year":"2018","journal-title":"Logical Methods in Computer Science 14"},{"key":"S1471068421000089_ref28","unstructured":"Kremer, P. 2004. A small counterexample in intuitionistic dynamic topological logic. http:\/\/individual.utoronto.ca\/philipkremer\/onlinepapers\/counterex.pdf."},{"key":"S1471068421000089_ref41","unstructured":"Slavnov, S. 2003. TR-2003015: Two counterexamples in the logic of dynamic topological systems. CUNY Academic Works."},{"key":"S1471068421000089_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.01.001"},{"key":"S1471068421000089_ref13","unstructured":"Di\u00e9guez, M. and Fern\u00e1ndez-Duque, D. 2018. An intuitionistic axiomatization of \u2018eventually\u2019. In Advances in Modal Logic, Vol. 12, 199\u2013218."},{"key":"S1471068421000089_ref31","first-page":"1","article-title":"Many-Dimensional Modal Logics: Theory and Applications","volume":"148","author":"Kurucz","year":"2003","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"S1471068421000089_ref38","doi-asserted-by":"crossref","unstructured":"Pnueli, A. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"S1471068421000089_ref22","unstructured":"Goldblatt, R. 1992. Logics of Time and Computation, 2 ed., Lecture Notes, CSLI , Vol. 7. Center for the Study of Language and Information, Stanford, CA."},{"key":"S1471068421000089_ref39","unstructured":"Rasiowa, H. and Sikorski, R. 1963. The Mathematics of Metamathematics. Pa\u0144stowowe Wydawnictwo Naukowe, Warsaw."},{"key":"S1471068421000089_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.008"},{"key":"S1471068421000089_ref7","first-page":"241","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST\u201907","author":"Cabalar","year":"2007"},{"key":"S1471068421000089_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.06.004"},{"key":"S1471068421000089_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370321"},{"key":"S1471068421000089_ref9","first-page":"1","article-title":"A temporal logic approach to binding-time analysis","author":"Davies","year":"2017","journal-title":"Journal of the ACM 64"},{"volume-title":"Topology","year":"1975","author":"Dugundji","key":"S1471068421000089_ref14"},{"key":"S1471068421000089_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67149-9"},{"key":"S1471068421000089_ref8","unstructured":"Davies, R. 1996. A temporal-logic approach to binding-time analysis. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27\u201330, 1996, 184\u2013195."},{"key":"S1471068421000089_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48758-8_6"},{"key":"S1471068421000089_ref5","doi-asserted-by":"crossref","unstructured":"Boudou, J. , Di\u00e9guez, M. , Fern\u00e1ndez-Duque, D. and Romero, F. 2019. Axiomatic systems and topological semantics for intuitionistic temporal logic. In Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Rende, Italy, May 7\u201311, 2019, Proceedings, 763\u2013777.","DOI":"10.1007\/978-3-030-19570-0_49"},{"volume-title":"A Short Introduction to Intuitionistic Logic","year":"2000","author":"Mints","key":"S1471068421000089_ref34"},{"key":"S1471068421000089_ref43","doi-asserted-by":"crossref","unstructured":"Yuse, Y. and Igarashi, A. 2006. A modal type system for multi-level generating extensions with persistent code. In Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. PPDP\u201906, 201\u2013212.","DOI":"10.1145\/1140335.1140360"},{"key":"S1471068421000089_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-9005-x"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068421000089","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,31]],"date-time":"2021-08-31T06:47:43Z","timestamp":1630392463000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068421000089\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,22]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,7]]}},"alternative-id":["S1471068421000089"],"URL":"https:\/\/doi.org\/10.1017\/s1471068421000089","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2021,4,22]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}