Sequent calculus in the topos of trees

Ranald Clouston, Rajeev Goré

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

    7 Citations (Scopus)

    Abstract

    Nakano’s “later” modality, inspired by Gödel-Löb provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that the semantics of the propositional fragment of this logic can be given by linear converse-well-founded intuitionistic Kripke frames, so this logic is a marriage of the intuitionistic modal logic KM and the intermediate logic LC. We therefore call this logic KMlin. We give a sound and cut-free complete sequent calculus for KMlin via a strategy that decomposes implication into its static and irreflexive components. Our calculus provides deterministic and terminating backward proof-search, yields decidability of the logic and the coNP-completeness of its validity problem. Our calculus and decision procedure can be restricted to drop linearity and hence capture KM.

    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    EditorsAndrew Pitts
    PublisherSpringer Verlag
    Pages133-147
    Number of pages15
    ISBN (Print)9783662466773
    DOIs
    Publication statusPublished - 2015
    Event18th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
    Duration: 11 Apr 201518 Apr 2015

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume9034
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference18th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
    Country/TerritoryUnited Kingdom
    CityLondon
    Period11/04/1518/04/15

    Fingerprint

    Dive into the research topics of 'Sequent calculus in the topos of trees'. Together they form a unique fingerprint.

    Cite this