Switch to: References

Add citations

You must login to add citations.
  1. Cut Elimination for Extended Sequent Calculi.Simone Martini, Andrea Masini & Margherita Zorzi - 2023 - Bulletin of the Section of Logic 52 (4):459-495.
    We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \(\Box\) and \(\Diamond\). Starting points for this research are 2-sequents and indexed-based calculi (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Substructural Negations.Takuro Onishi - 2015 - Australasian Journal of Logic 12 (4).
    We present substructural negations, a family of negations classified in terms of structural rules of an extended kind of sequent calculus, display calculus. In considering the whole picture, we emphasize the duality of negation. Two types of negative modality, impossibility and unnecessity, are discussed and "self-dual" negations like Classical, De Morgan, or Ockham negation are redefined as the fusions of two negative modalities. We also consider how to identify, using intuitionistic and dual intuitionistic negations, two accessibility relations associated with impossibility (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • The Basics of Display Calculi.Tim Lyon, Christian Ittner, Timo Eckhardt & Norbert Gratzl - 2017 - Kriterion - Journal of Philosophy 31 (2):55-100.
    The aim of this paper is to introduce and explain display calculi for a variety of logics. We provide a survey of key results concerning such calculi, though we focus mainly on the global cut elimination theorem. Propositional, first-order, and modal display calculi are considered and their properties detailed.
    Download  
     
    Export citation  
     
    Bookmark  
  • Knowledge, belief, normality, and introspection.Dominik Klein, Olivier Roy & Norbert Gratzl - 2017 - Synthese:1-30.
    We study two logics of knowledge and belief stemming from the work of Stalnaker, omitting positive introspection for knowledge. The two systems are equivalent with positive introspection, but not without. We show that while the logic of beliefs remains unaffected by omitting introspection for knowledge in one system, it brings significant changes to the other. The resulting logic of belief is non-normal, and its complete axiomatization uses an infinite hierarchy of coherence constraints. We conclude by returning to the philosophical interpretation (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Knowledge, belief, normality, and introspection.Dominik Klein, Olivier Roy & Norbert Gratzl - 2017 - Synthese 195 (10):4343-4372.
    We study two logics of knowledge and belief stemming from the work of Stalnaker, omitting positive introspection for knowledge. The two systems are equivalent with positive introspection, but not without. We show that while the logic of beliefs remains unaffected by omitting introspection for knowledge in one system, it brings significant changes to the other. The resulting logic of belief is non-normal, and its complete axiomatization uses an infinite hierarchy of coherence constraints. We conclude by returning to the philosophical interpretation (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Linear time in hypersequent framework.Andrzej Indrzejczak - 2016 - Bulletin of Symbolic Logic 22 (1):121-144.
    Hypersequent calculus, developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi. In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Natural deduction calculi for classical and intuitionistic S5.S. Guerrini, A. Masini & M. Zorzi - 2023 - Journal of Applied Non-Classical Logics 33 (2):165-205.
    1. It is a fact that developing a good proof theory for modal logics is a difficult task. The problem is not in having deductive systems. In fact, all the main modal logics enjoy an axiomatic prese...
    Download  
     
    Export citation  
     
    Bookmark  
  • Disentangling Structural Connectives or Life Without Display Property.Sergey Drobyshevich - 2019 - Journal of Philosophical Logic 48 (2):279-303.
    The work is concerned with the so called display property of display logic. The motivation behind it is discussed and challenged. It is shown using one display calculus for intuitionistic logic as an example that the display property can be abandoned without losing subformula, cut elimination and completeness properties in such a way that results in additional expressive power of the system. This is done by disentangling structural connectives so that they are no longer context-sensitive. A recipe for characterizing structural (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Hypersequent Calculi for S5: The Methods of Cut Elimination.Kaja Bednarska & Andrzej Indrzejczak - 2015 - Logic and Logical Philosophy 24 (3):277–311.
    Download  
     
    Export citation  
     
    Bookmark   11 citations