5 found
  1.  13
    An Analysis of the Rules of Gentzen’s Nj and Lj.Mirjana Borisavljević - 2018 - Review of Symbolic Logic 11 (2):347-370.
  2.  15
    A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
    A new set of conversions for derivations in the system of sequents for intuitionistic predicate logic will be defined. These conversions will be some modifications of Zucker's conversions from the system of sequents from [11], which will have the following characteristics: (1) these conversions will be sufficient for transforming a derivation into a cut-free one, and (2) in the natural deduction the image of each of these conversions will be either in the set of conversions for normalization procedure, or an (...)
    Direct download (3 more)  
    Export citation  
    Bookmark   2 citations  
  3.  25
    A Cut-Elimination Proof in Intuitionistic Predicate Logic.Mirjana Borisavljević - 1999 - Annals of Pure and Applied Logic 99 (1-3):105-136.
    In this paper we give a new proof of cut elimination in Gentzen's sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.
    Direct download (4 more)  
    Export citation  
    Bookmark   2 citations  
  4.  11
    The Subformula Property of Natural Deduction Derivations and Analytic Cuts.Mirjana Borisavljević - forthcoming - Logic Journal of the IGPL.
    In derivations of a sequent system, $\mathcal{L}\mathcal{J}$, and a natural deduction system, $\mathcal{N}\mathcal{J}$, the trails of formulae and the subformula property based on these trails will be defined. The derivations of $\mathcal{N}\mathcal{J}$ and $\mathcal{L}\mathcal{J}$ will be connected by the map $g$, and it will be proved the following: an $\mathcal{N}\mathcal{J}$-derivation is normal $\Longleftrightarrow $ it has the subformula property based on trails $\Longleftrightarrow $ its $g$-image in $\mathcal{L}\mathcal{J}$ is without maximum cuts $\Longrightarrow $ that $g$-image has the subformula property based (...)
    Direct download (2 more)  
    Export citation  
  5.  15
    Two Measures for Proving Gentzen's Hauptsatz Without Mix.Mirjana Borisavljević - 2003 - Archive for Mathematical Logic 42 (4):371-387.
    This paper presents a cut-elimination procedure for classical and intuitionistic logic, in which cut is eliminated directly, without introducing the mix rule. The well-known problem of cut eliminations, when in the derivation the contractions of the cut-formulae are above the premisses of the cut, will be solved by new transformations of the derivation.
    Direct download (3 more)  
    Export citation  
    Bookmark   1 citation