Switch to: Citations

Add references

You must login to add references.
  1. A focused approach to combining logics.Chuck Liang & Dale Miller - 2011 - Annals of Pure and Applied Logic 162 (9):679-697.
    We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative–additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut-elimination holds in such fragments. From cut-elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Investigations into Logical Deduction.Gerhard Gentzen - 1964 - American Philosophical Quarterly 1 (4):288 - 306.
    Download  
     
    Export citation  
     
    Bookmark   151 citations  
  • A formalization of the propositional calculus of H-B logic.Cecylia Rauszer - 1974 - Studia Logica 33 (1):23 - 34.
    Download  
     
    Export citation  
     
    Bookmark   49 citations  
  • (1 other version)Semantical Analysis of Intuitionistic Logic I.Saul A. Kripke - 1963 - In Michael Dummett & J. N. Crossley (eds.), Formal Systems and Recursive Functions. Amsterdam,: North Holland. pp. 92-130.
    Download  
     
    Export citation  
     
    Bookmark   112 citations  
  • Mathematical Intuitionism. Introduction to Proof Theory.A. G. Dragalin & E. Mendelson - 1990 - Journal of Symbolic Logic 55 (3):1308-1309.
    Download  
     
    Export citation  
     
    Bookmark   28 citations  
  • On the unity of logic.Jean-Yves Girard - 1993 - Annals of Pure and Applied Logic 59 (3):201-217.
    We present a single sequent calculus common to classical, intuitionistic and linear logics. The main novelty is that classical, intuitionistic and linear logics appear as fragments, i.e. as particular classes of formulas and sequents. For instance, a proof of an intuitionistic formula A may use classical or linear lemmas without any restriction: but after cut-elimination the proof of A is wholly intuitionistic, what is superficially achieved by the subformula property and more deeply by a very careful treatment of structural rules. (...)
    Download  
     
    Export citation  
     
    Bookmark   25 citations  
  • An intuitiomstic completeness theorem for intuitionistic predicate logic.Wim Veldman - 1976 - Journal of Symbolic Logic 41 (1):159-166.
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • Contraction-free sequent calculi for intuitionistic logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.
    Download  
     
    Export citation  
     
    Bookmark   33 citations  
  • .[author unknown] - 2016 - Journal of Medicine and Philosophy 41 (5):NP-NP.
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • Kripke models for classical logic.Danko Ilik, Gyesik Lee & Hugo Herbelin - 2010 - Annals of Pure and Applied Logic 161 (11):1367-1378.
    We introduce a notion of the Kripke model for classical logic for which we constructively prove the soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.
    Download  
     
    Export citation  
     
    Bookmark   3 citations