From Display to Labelled Proofs for Tense Logics

A. Ciabattoni, T. Lyon*, R. Ramanayake

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)

Abstract

We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt , the image is shown to be the set of all proofs in the labelled calculus G3Kt .
Original languageEnglish
Title of host publicationLogical Foundations of Computer Science
EditorsSergei Artemov, Anil Nerode
PublisherSpringer
Pages120-139
Number of pages20
ISBN (Electronic)978-3-319-72056-2
ISBN (Print)978-3-319-72055-5
DOIs
Publication statusPublished - 2018
Externally publishedYes
EventInternational Symposium, LFCS 2018 - Deerfield Beach, United States
Duration: 8-Jan-201811-Jan-2018

Publication series

NameLecture Notes in Computer Science (LNCS)
PublisherSpringer
Volume10703

Conference

ConferenceInternational Symposium, LFCS 2018
Country/TerritoryUnited States
CityDeerfield Beach
Period08/01/201811/01/2018

Cite this