# From Display to Labelled Proofs for Tense Logics

From International Center for Computational Logic

# From Display to Labelled Proofs for Tense Logics

##### Tim LyonTim Lyon, Agata CiabattoniAgata Ciabattoni, Revantha RamanayakeRevantha Ramanayake

Tim Lyon, Agata Ciabattoni, Revantha Ramanayake

In Artemov, Sergei and Nerode, Anil, eds.,

**From Display to Labelled Proofs for Tense Logics**In Artemov, Sergei and Nerode, Anil, eds.,

*From Display to Labelled Proofs for Tense Logics*, volume 10703, 120-139, 2018. Springer International Publishing**Kurzfassung****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.**Weitere Informationen unter:****Other info:**Link**Forschungsgruppe:****Research Group:**Computational Logic

```
@InProceedings{10.1007/978-3-319-72056-2_8,
author="Ciabattoni, Agata
and Lyon, Tim
and Ramanayake, Revantha",
editor="Artemov, Sergei
and Nerode, Anil",
title="From Display to Labelled Proofs for Tense Logics",
booktitle="Logical Foundations of Computer Science",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="120--139",
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.",
isbn="978-3-319-72056-2"
}
```