### Citations

854 |
A companion to modal logic
- Hughes, Cresswell
- 1984
(Show Context)
Citation Context ...ic HKt + _p → q is not the inconsistent logic but instead the tense counterpart of the maximal (in the sense of axiomatic extensions) consistent modal logic Ver which is usually axiomatised asHK +⊥ [=-=Hughes and Cresswell 1996-=-]. Remark 5.8. We have already seen above that a disadvantage of applying Ackermann’s lemma directly to ∨1≤j≤MDj rather than applying invertible right rules first is that the former (Kracht’s method) ... |

691 |
1935], Untersuchungen über das logische Schliessen
- Gentzen
(Show Context)
Citation Context ...manayake, 2014. Power and Limits of Structural Display Rules. ACM Trans. Embedd. Comput. Syst. V, N, Article A (January YYYY), 35 pages. DOI:http://dx.doi.org/10.1145/0000000.0000000 1. INTRODUCTION [=-=Gentzen 1935-=-] introduced a proof system called the sequent calculus as a tool for studying the structure of proofs in classical and intuitionistic logic. The main result is the cut-elimination theorem which shows... |

419 | Logic Programming with Focusing Proofs in Linear Logic,
- Andreoli
- 1992
(Show Context)
Citation Context ...(A ` I) (resp. ∈ inv(I ` A)) containing no logical connectives. The most external connective of an a-soluble formula has left introduction rules that are invertible (i.e. it is a positive connective [=-=Andreoli 1992-=-]), while the most external connective of an s-soluble formula has invertible right introduction rules (i.e. it is a negative connective). Definition 3.11 (I0(C), I1(C), I2(C)). Let C be an amenable c... |

304 |
Proof Methods for Modal and Intuitionistic Logics.
- Fitting
- 1983
(Show Context)
Citation Context ...ate the problem of modularity while still retaining cut-elimination. Prominent examples include the hypersequent calculus [Avron 1987], the display calculus [Belnap 1982], labelled deductive systems [=-=Fitting 1983-=-; Negri 2005], nested sequent systems [Kashima 1994; Brünnler 2006] and the calculus of structures [Guglielmi 2007]. And yet, despite a large number of papers in the literature dealing with this topi... |

134 |
Display logic,
- Belnap
- 1982
(Show Context)
Citation Context ...t-free sequent formalisation and to alleviate the problem of modularity while still retaining cut-elimination. Prominent examples include the hypersequent calculus [Avron 1987], the display calculus [=-=Belnap 1982-=-], labelled deductive systems [Fitting 1983; Negri 2005], nested sequent systems [Kashima 1994; Brünnler 2006] and the calculus of structures [Guglielmi 2007]. And yet, despite a large number of pape... |

109 | A system of interaction and structure
- Guglielmi
- 2002
(Show Context)
Citation Context ...calculus [Avron 1987], the display calculus [Belnap 1982], labelled deductive systems [Fitting 1983; Negri 2005], nested sequent systems [Kashima 1994; Brünnler 2006] and the calculus of structures [=-=Guglielmi 2007-=-]. And yet, despite a large number of papers in the literature dealing with this topic some logics still lack an analytic calculus (e.g. the logic of cancellative residuated lattices [Bahls et al. 200... |

50 |
A constructive analysis of RM
- Avron
- 1987
(Show Context)
Citation Context ... for logics apparently lacking a cut-free sequent formalisation and to alleviate the problem of modularity while still retaining cut-elimination. Prominent examples include the hypersequent calculus [=-=Avron 1987-=-], the display calculus [Belnap 1982], labelled deductive systems [Fitting 1983; Negri 2005], nested sequent systems [Kashima 1994; Brünnler 2006] and the calculus of structures [Guglielmi 2007]. And... |

49 | Substructural logics on display - Goré - 1997 |

43 | Deep sequent systems for modal logic, - Brunnler - 2009 |

29 | From axioms to analytic rules in nonclassical logics
- Ciabattoni, Galatos, et al.
- 2008
(Show Context)
Citation Context ...rules i.e. structural rules satisfying C1–C7. Various algorithms have been proposed to define analytic calculi for extensions of logics in a uniform and modular manner, e.g. [Kracht 1996; Negri 2005; =-=Ciabattoni et al. 2008-=-; Ciabattoni et al. 2009; Goré et al. 2011; Ciabattoni et al. 2012; Lellmann and Pattinson 2013; Lahav 2013; Marin and Straßburger 2014; Lellmann 2014]. Yet, they all start with a specific calculus i... |

26 |
Cut-free sequent calculi for some tense logics,
- Kashima
- 1994
(Show Context)
Citation Context ... cut-elimination. Prominent examples include the hypersequent calculus [Avron 1987], the display calculus [Belnap 1982], labelled deductive systems [Fitting 1983; Negri 2005], nested sequent systems [=-=Kashima 1994-=-; Brünnler 2006] and the calculus of structures [Guglielmi 2007]. And yet, despite a large number of papers in the literature dealing with this topic some logics still lack an analytic calculus (e.g.... |

24 | Power and weakness of the modal display calculus
- Kracht
- 1996
(Show Context)
Citation Context ...erful and semantic-independent formalism that has been used to formalise a variety of different logics ranging from resource-oriented logics [Goré 1998b; 1998a; Brotherston 2012] to temporal logics [=-=Kracht 1996-=-]. The display calculus extends Gentzen’s language of sequent, comprising of the structural connectives comma and `, with new n-ary connectives. While the comma is usually assumed to be associative (a... |

22 |
Displaying Modal Logic
- Wansing
- 1998
(Show Context)
Citation Context ... characterisation of analytic structural rule extensions, does not appear in that work. The paper is organized as follows: Section 2 provides a short introduction to the display calculus (see, e.g., [=-=Wansing 1998-=-; Restall 1998; Ciabattoni et al. 2014] for more details). The algorithm for transforming axioms into structural display rules is described in Section 3, and compared in 3.3 with ACM Transactions on E... |

21 | Modal Logic,” Cambridge Tracts - Blackburn, Rijke, et al. - 2001 |

14 | Algorithmic correspondence and canonicity for distributive modal logic
- Conradie, Palmigiano
- 2012
(Show Context)
Citation Context ... calculus ACM Transactions on Embedded Computing Systems, Vol. V, No. N, Article A, Publication date: January YYYY. A:9 formulation, below, of the so-called Ackermann’s lemma [Ciabattoni et al. 2008; =-=Conradie and Palmigiano 2012-=-] allowing a formula in a rule to switch sides of the sequent moving from conclusion to premises. LEMMA 3.6 (ACKERMANN’S LEMMA). Each of the following pairs of rules is pairwise equivalent in an amena... |

14 | Gaggles, Gentzen and Galois: How to display your favourite substructural logic - Goré - 1998 |

8 | Bunched logics displayed - Brotherston |

7 |
Cancellative residuated lattices, Algebra Universalis
- Bahls, Cole, et al.
(Show Context)
Citation Context ... [Guglielmi 2007]. And yet, despite a large number of papers in the literature dealing with this topic some logics still lack an analytic calculus (e.g. the logic of cancellative residuated lattices [=-=Bahls et al. 2003-=-]). It is not known if this is due to the lack of the “correct” inference rule(s) and/or cut-elimination proof, or the lack of an appropriate formalism, or if there is some fundamental obstacle preven... |

7 | Expanding the realm of systematic proof theory
- Ciabattoni, Straßburger, et al.
- 2009
(Show Context)
Citation Context ...les satisfying C1–C7. Various algorithms have been proposed to define analytic calculi for extensions of logics in a uniform and modular manner, e.g. [Kracht 1996; Negri 2005; Ciabattoni et al. 2008; =-=Ciabattoni et al. 2009-=-; Goré et al. 2011; Ciabattoni et al. 2012; Lellmann and Pattinson 2013; Lahav 2013; Marin and Straßburger 2014; Lellmann 2014]. Yet, they all start with a specific calculus in some proof-theoretic f... |

7 | Theoremhood-preserving maps characterizing cut elimination for modal provability logics - Demri, Goré - 2002 |

7 |
Displaying and deciding substructural logics. I. Logics with contraposition
- Restall
- 1998
(Show Context)
Citation Context ...ion of analytic structural rule extensions, does not appear in that work. The paper is organized as follows: Section 2 provides a short introduction to the display calculus (see, e.g., [Wansing 1998; =-=Restall 1998-=-; Ciabattoni et al. 2014] for more details). The algorithm for transforming axioms into structural display rules is described in Section 3, and compared in 3.3 with ACM Transactions on Embedded Comput... |

7 |
Constructive negation, implication, and co-implication
- Wansing
(Show Context)
Citation Context ...change (first row) and right contraction and left contraction, right associativity and left associativity (second row). Then, using Theorem 3.36, and following some simplification to get the form in [=-=Wansing 2008-=-], we obtain corresponding analytic structural rules (given below each axiom). Their addition to δBi-FL yields a display calculus corresponding to a Hilbert calculus for HB. A→ (A+B) L `M L `M,N A ·B→... |

4 | Label-free modular systems for classical and intuitionistic modal logics. In: Gore,
- Marin, Straßburger
- 2014
(Show Context)
Citation Context ...ics in a uniform and modular manner, e.g. [Kracht 1996; Negri 2005; Ciabattoni et al. 2008; Ciabattoni et al. 2009; Goré et al. 2011; Ciabattoni et al. 2012; Lellmann and Pattinson 2013; Lahav 2013; =-=Marin and Straßburger 2014-=-; Lellmann 2014]. Yet, they all start with a specific calculus in some proof-theoretic framework and transform Hilbert axioms or semantic conditions into suitable rules. Moreover, excepting [Ciabatton... |

3 | From categorical grammar to bilinear logic - Lambek - 1993 |

2 | Structural rule extensions of display calculi: a general recipe - Ciabattoni, Ramanayake |

2 |
Hypersequent and display calculi – a unified perspective
- Ciabattoni, Ramanayake, et al.
(Show Context)
Citation Context ...c structural rule extensions, does not appear in that work. The paper is organized as follows: Section 2 provides a short introduction to the display calculus (see, e.g., [Wansing 1998; Restall 1998; =-=Ciabattoni et al. 2014-=-] for more details). The algorithm for transforming axioms into structural display rules is described in Section 3, and compared in 3.3 with ACM Transactions on Embedded Computing Systems, Vol. V, No.... |

2 | Correspondence between modal Hilbert axioms and sequent rules with an application to S5
- Lellmann, Pattinson
- 2013
(Show Context)
Citation Context ...ne analytic calculi for extensions of logics in a uniform and modular manner, e.g. [Kracht 1996; Negri 2005; Ciabattoni et al. 2008; Ciabattoni et al. 2009; Goré et al. 2011; Ciabattoni et al. 2012; =-=Lellmann and Pattinson 2013-=-; Lahav 2013; Marin and Straßburger 2014; Lellmann 2014]. Yet, they all start with a specific calculus in some proof-theoretic framework and transform Hilbert axioms or semantic conditions into suitab... |

1 |
Algebraic proof theory I: cut-elimination and completions
- Ciabattoni, Galatos, et al.
- 2012
(Show Context)
Citation Context ...ve been proposed to define analytic calculi for extensions of logics in a uniform and modular manner, e.g. [Kracht 1996; Negri 2005; Ciabattoni et al. 2008; Ciabattoni et al. 2009; Goré et al. 2011; =-=Ciabattoni et al. 2012-=-; Lellmann and Pattinson 2013; Lahav 2013; Marin and Straßburger 2014; Lellmann 2014]. Yet, they all start with a specific calculus in some proof-theoretic framework and transform Hilbert axioms or se... |

1 | Article A, Publication date: January YYYY. A:35 - unknown authors - 1997 |

1 | A note on the substructural hierarchy. preprint - Jeřábek - 2015 |