Switch to: References

Add citations

You must login to add citations.
  1. Cut elimination by unthreading.Gabriele Pulcini - 2023 - Archive for Mathematical Logic 63 (1):211-223.
    We provide a non-Gentzen, though fully syntactical, cut-elimination algorithm for classical propositional logic. The designed procedure is implemented on $$\textsf{GS4}$$ GS 4, the one-sided version of Kleene’s sequent system $$\textsf{G4}$$ G 4. The algorithm here proposed proves to be more ‘dexterous’ than other, more traditional, Gentzen-style techniques as the size of proofs decreases at each step of reduction. As a corollary result, we show that analyticity always guarantees minimality of the size of $$\textsf{GS4}$$ GS 4 -proofs.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • A Proof Theory for the Logic of Provability in True Arithmetic.Hirohiko Kushida - 2020 - Studia Logica 108 (4):857-875.
    In a classical 1976 paper, Solovay proved the arithmetical completeness of the modal logic GL; provability of a formula in GL coincides with provability of its arithmetical interpretations of it in Peano Arithmetic. In that paper, he also provided an axiomatic system GLS and proved arithmetical completeness for GLS; provability of a formula in GLS coincides with truth of its arithmetical interpretations in the standard model of arithmetic. Proof theory for GL has been studied intensively up to the present day. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Tautology Elimination, Cut Elimination, and S5.Andrezj Indrzejczak - 2017 - Logic and Logical Philosophy 26 (4):461-471.
    Tautology elimination rule was successfully applied in automated deduction and recently considered in the framework of sequent calculi where it is provably equivalent to cut rule. In this paper we focus on the advantages of proving admissibility of tautology elimination rule instead of cut for sequent calculi. It seems that one may find simpler proofs of admissibility for tautology elimination than for cut admissibility. Moreover, one may prove its admissibility for some calculi where constructive proofs of cut admissibility fail. As (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics.Feng Gao & George Tourlakis - 2015 - Bulletin of the Section of Logic 44 (3/4):131-147.
    A well established technique toward developing the proof theory of a Hilbert-style modal logic is to introduce a Gentzen-style equivalent (a Gentzenisation), then develop the proof theory of the latter, and finally transfer the metatheoretical results to the original logic (e.g., [1, 6, 8, 18, 10, 12]). In the first-order modal case, on one hand we know that the Gentzenisation of the straightforward first-order extension of GL, the logic QGL, admits no cut elimination (if the rule is included as primitive; (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations