Loop-Check Specification for a Sequent Calculus of Temporal Logic

Studia Logica 110 (6):1507-1536 (2022)
  Copy   BIBTEX

Abstract

In our previous work we have introduced loop-type sequent calculi for propositional linear discrete tense logic and proved that these calculi are sound and complete. Decision procedures using the calculi have been constructed for the considered logic. In the present paper we restrict ourselves to the logic with the unary temporal operators “next” and “henceforth always”. Proof-theory of the sequent calculus of this logic is considered, focusing on loop specification in backward proof-search. We describe cyclic sequents and prove that any loop consists of only cyclic sequents. A class of sequents for which backward proof-search do not require loop-check is presented. It is shown how sequents can be coded by binary strings that are used in backward proof-search for the sake of more efficient loop-check.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,752

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Labeled Sequent Calculus for Orthologic.Tomoaki Kawano - 2018 - Bulletin of the Section of Logic 47 (4):217-232.
Canonical proof nets for classical logic.Richard McKinley - 2013 - Annals of Pure and Applied Logic 164 (6):702-732.
A proof-search system for the logic of likelihood.R. Alonderis & H. Giedra - 2020 - Logic Journal of the IGPL 28 (3):261-280.
2-Sequent calculus: a proof theory of modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.
A Sequent Calculus for Urn Logic.Rohan French - 2015 - Journal of Logic, Language and Information 24 (2):131-147.
Sequent Calculi And Quasivarieties.Katarzyna Palasinska - 2000 - Reports on Mathematical Logic:107-131.
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.

Analytics

Added to PP
2022-08-31

Downloads
14 (#986,446)

6 months
7 (#421,763)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Contraction-free sequent calculi for intuitionistic logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.
The tableau method for temporal logic: An overview.Pierre Wolper - 1985 - Logique Et Analyse 28 (110-111):119-136.
A Completeness Proof For An Infinitary Tense Logic.Goran Sundholm - 1977 - Bulletin of the Section of Logic 6 (2):70-72.

View all 6 references / Add more references