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

[img] 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.

Item Type:

Journal Article (Original Article)

Division/Institute:

08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG)
08 Faculty of Science > Institute of Computer Science (INF)

UniBE Contributor:

Zenger, Lukas Matthias

Subjects:

000 Computer science, knowledge & systems
500 Science > 510 Mathematics

ISSN:

0302-9743

Publisher:

Springer

Language:

English

Submitter:

Armand Singh Satjeevan Feuilleaubois

Date Deposited:

20 Mar 2024 12:15

Last Modified:

20 Mar 2024 12:15

Publisher DOI:

10.1007/978-3-031-43513-3_13

Related URLs:

Additional Information:

Automated Reasoning with Analytic Tableaux and Related Methods

Uncontrolled Keywords:

sequent calculus, intuitionistic logic, temporal logic, ill-founded proofs

BORIS DOI:

10.48350/194290

URI:

https://boris.unibe.ch/id/eprint/194290

Actions (login required)

Edit item Edit item
Provide Feedback