Switch to: References

Add citations

You must login to add citations.
  1. Sufficient conditions for cut elimination with complexity analysis.João Rasga - 2007 - Annals of Pure and Applied Logic 149 (1-3):81-99.
    Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • The Geometry of Non-Distributive Logics.Greg Restall & Francesco Paoli - 2005 - Journal of Symbolic Logic 70 (4):1108 - 1126.
    In this paper we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness, and we show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic. This natural deduction system is inspired both by Shoesmith and Smiley's multiple conclusion systems (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • The cost of a cycle is a square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.
    The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with O(k n+l ) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Modal Sequent Calculi Labelled with Truth Values: Completeness, Duality and Analyticity.Paulo Mateus, Amílcar Sernadas, Cristina Sernadas & Luca Viganò - 2004 - Logic Journal of the IGPL 12 (3):227-274.
    Labelled sequent calculi are provided for a wide class of normal modal systems using truth values as labels. The rules for formula constructors are common to all modal systems. For each modal system, specific rules for truth values are provided that reflect the envisaged properties of the accessibility relation. Both local and global reasoning are supported. Strong completeness is proved for a natural two-sorted algebraic semantics. As a corollary, strong completeness is also obtained over general Kripke semantics. A duality result (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Logical structures and genus of proofs.Alessandra Carbone - 2010 - Annals of Pure and Applied Logic 161 (2):139-149.
    Any arbitrarily complicated non-oriented graph, that is a graph of arbitrarily large genus, can be encoded in a cut-free proof. This unpublished result of Statman was shown in the early seventies. We provide a proof of it, and of a number of other related facts.
    Download  
     
    Export citation  
     
    Bookmark   2 citations