6 found
Order:
  1.  17
    Deep Sequent Systems for Modal Logic.Kai Brünnler - 2009 - Archive for Mathematical Logic 48 (6):551-577.
    We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen’s sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, weakening and (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  2.  5
    Syntactic Cut-Elimination for Common Knowledge.Kai Brünnler & Thomas Studer - 2009 - Annals of Pure and Applied Logic 160 (1):82-95.
    We first look at an existing infinitary sequent system for common knowledge for which there is no known syntactic cut-elimination procedure and also no known non-trivial bound on the proof-depth. We then present another infinitary sequent system based on nested sequents that are essentially trees and with inference rules that apply deeply inside these trees. Thus we call this system “deep” while we call the former system “shallow”. In contrast to the shallow system, the deep system allows one to give (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  3.  14
    Locality for Classical Logic.Kai Brünnler - 2006 - Notre Dame Journal of Formal Logic 47 (4):557-580.
    In this paper we will see deductive systems for classical propositional and predicate logic in the calculus of structures. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they drop the restriction that rules only apply to the main connective of a formula: their rules apply anywhere deeply inside a formula. This allows to observe very clearly the symmetry between identity axiom and the cut rule. This symmetry allows to reduce the cut rule to atomic (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  11
    Syntactic Cut-Elimination for a Fragment of the Modal Mu-Calculus.Kai Brünnler & Thomas Studer - 2012 - Annals of Pure and Applied Logic 163 (12):1838-1853.
    For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius [15] for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge [5] and by Hill and Poggiolesi for PDL[8], which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach can (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  49
    Cut Elimination Inside a Deep Inference System for Classical Predicate Logic.Kai Brünnler - 2006 - Studia Logica 82 (1):51-71.
    Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  6.  17
    On Contraction and the Modal Fragment.Kai Brünnler, Dieter Probst & Thomas Studer - 2008 - Mathematical Logic Quarterly 54 (4):345-349.
    We observe that removing contraction from a standard sequent calculus for first-order predicate logic preserves completeness for the modal fragment.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark