Switch to: References

Add citations

You must login to add citations.
  1. Substitution Frege and Extended Frege Proof Systems in Non-Classical Logics.Emil Jeřábek - 2009 - Annals of Pure and Applied Logic 159 (1-2):1-48.
    We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , all tabular logics, all logics (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Proof Complexity of Intuitionistic Implicational Formulas.Emil Jeřábek - 2017 - Annals of Pure and Applied Logic 168 (1):150-190.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Independent Bases of Admissible Rules.Emil Jerábek - 2008 - Logic Journal of the IGPL 16 (3):249-267.
    We show that IPC, K4, GL, and S4, as well as all logics inheriting their admissible rules, have independent bases of admissible rules.
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • Proof Complexity of Propositional Default Logic.Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas & Heribert Vollmer - 2011 - Archive for Mathematical Logic 50 (7-8):727-742.
    Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen’s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Canonical Rules.Emil Jeřábek - 2009 - Journal of Symbolic Logic 74 (4):1171 - 1205.
    We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia (...)
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Rules with Parameters in Modal Logic I.Emil Jeřábek - 2015 - Annals of Pure and Applied Logic 166 (9):881-933.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • On Lengths of Proofs in Non-Classical Logics.Pavel Hrubeš - 2009 - Annals of Pure and Applied Logic 157 (2-3):194-205.
    We give proofs of the effective monotone interpolation property for the system of modal logic K, and others, and the system IL of intuitionistic propositional logic. Hence we obtain exponential lower bounds on the number of proof-lines in those systems. The main results have been given in [P. Hrubeš, Lower bounds for modal logics, Journal of Symbolic Logic 72 941–958; P. Hrubeš, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 72–90]; here, we give considerably simplified (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations