Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic

Afshari, Bahareh; Grotenhuis, Lide; Leigh, Graham E; Zenger, Lukas (2023). Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic. Lecture notes in computer science, 14278, pp. 223-241. Springer 10.1007/978-3-031-43513-3_13

Text 978-3-031-43513-3_13.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (396kB)

We introduce ill-founded sequent calculi for two intuitionistic linear-time temporal logics. Both logics are based on the language of intuitionistic propositional logic with ‘next’and ‘until’operators and are evaluated on dynamic Kripke models wherein the intuitionistic and temporal accessibility relations are assumed to satisfy one of two natural confluence properties: forward confluence in one case, and both forward and backward confluence in the other. The presented sequent calculi are cut-free and incorporate a simple form of formula nesting. Soundness of the calculi is shown by a standard argument and completeness via proof search.

Interest & Impact

Downloads

1 since deposited on 20 Mar 2024
1 in the past 12 months

Citations

5 Citations in Web of Science ®
6 Citations in Scopus

Search

in Google Scholar™

Services

Actions (login required)

Edit item

Actions (login required)

Edit item