Constructing cut free sequent systems with context restrictions based on classical or intuitionistic logic

Björn Lellmann*, Dirk Pattinson

*Corresponding author for this work

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

    12 Citations (Scopus)

    Abstract

    We consider a general format for sequent rules for not necessarily normal modal logics based on classical or intuitionistic propositional logic and provide relatively simple local conditions ensuring cut elimination for such rule sets. The rule format encompasses e.g. rules for the boolean connectives and transitive modal logics such as S4 or its constructive version. We also adapt the method of constructing suitable rule sets by saturation to the intuitionistic setting and provide a criterium for translating axioms for intuitionistic modal logics into sequent rules. Examples include constructive modal logics and conditional logic.

    Original languageEnglish
    Title of host publicationLogic and Its Applications - 5th Indian Conference, ICLA 2013, Proceedings
    PublisherSpringer Verlag
    Pages148-160
    Number of pages13
    ISBN (Print)9783642360381
    DOIs
    Publication statusPublished - 2013
    Event5th Indian Conference on Logic and Its Applications, ICLA 2013 - Chennai, India
    Duration: 10 Jan 201312 Jan 2013

    Publication series

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

    Conference

    Conference5th Indian Conference on Logic and Its Applications, ICLA 2013
    Country/TerritoryIndia
    CityChennai
    Period10/01/1312/01/13

    Fingerprint

    Dive into the research topics of 'Constructing cut free sequent systems with context restrictions based on classical or intuitionistic logic'. Together they form a unique fingerprint.

    Cite this