{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T04:13:01Z","timestamp":1730002381711,"version":"3.28.0"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,11]]},"abstract":"Intuitionistic linear temporal logic (iLTL) has been studied extensively, especially in the last decade. It enjoys natural semantics over intuitionistic Kripke frames equipped with an order-preserving function representing the temporal dynamics, known as 'expanding models'. This leads to a logic that is known to be decidable but whose axiomatisation has long remained open.\n\n\n\nWe propose an extension of iLTL with the co-implication connective of Hilbert\u2013Brouwer logic and call it 'bi-intuitionistic linear temporal logic' (biLTL). We establish that this extension is still decidable for the class of expanding models. We moreover give a sound and complete Hilbert-style calculus for it, the first for any logic extending iLTL. As a corollary, the topological semantics for intuitionistic propositional logic cannot be extended to a topological semantics for Hilbert-Brouwer logic, which thus establishes co-implication as a distinctive feature of the Kripke semantics for bi-intuitionistic logic.<\/jats:p>","DOI":"10.24963\/kr.2024\/33","type":"proceedings-article","created":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T06:30:28Z","timestamp":1729924228000},"page":"350-360","source":"Crossref","is-referenced-by-count":0,"title":["A Sound and Complete Axiomatisation for Intuitionistic Linear Temporal Logic"],"prefix":"10.24963","author":[{"given":"David","family":"Fern\u00e1ndez-Duque","sequence":"first","affiliation":[{"name":"Universitat de Barcelona"}]},{"given":"Brett","family":"McLean","sequence":"additional","affiliation":[{"name":"Ghent University"}]},{"given":"Lukas","family":"Zenger","sequence":"additional","affiliation":[{"name":"University of Bern"}]}],"member":"10584","event":{"name":"21st International Conference on Principles of Knowledge Representation and Reasoning {KR-2023}","theme":"Artificial Intelligence","location":"Hanoi, Vietnam","acronym":"KR-2024","number":"21","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","Academic College of Tel-Aviv","European Association for Artificial Intelligence","National Science Foundation"],"start":{"date-parts":[[2024,11,1]]},"end":{"date-parts":[[2024,11,8]]}},"container-title":["Proceedings of the TwentyFirst International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T06:30:35Z","timestamp":1729924235000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2024\/33"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2024,11]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2024\/33","relation":{},"subject":[],"published":{"date-parts":[[2024,11]]}}}