7 found
Order:
  1.  20
    An Analysis of the Rules of Gentzen’s _Nj__ and __Lj_.Mirjana Borisavljević - 2018 - Review of Symbolic Logic 11 (2):347-370.
    The connection between the rules and derivations of Gentzen’s calculiNJandLJwill be explained by several steps (i.e., systems), and an analysis of the well-known problems of the connection between reduction steps of normalization and cut elimination, from Zucker (1974) and Urban (2014), will be given.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  2.  29
    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  
     
    Bookmark   2 citations  
  3.  26
    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   4 citations  
  4.  39
    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   4 citations  
  5.  19
    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   2 citations  
  6.  13
    The Elimination of Maximum Cuts in Linear Logic and BCK Logic.Mirjana Borisavljevic - 2023 - Studia Logica 111 (3):391-429.
    In the sequent systems for exponential-free linear logic and BCK logic a procedure of elimination of maximum cuts, cuts which correspond to maximum segments from natural deduction derivations, will be presented.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  7.  15
    Maximum Segments as Natural Deduction Images of Some Cuts.Mirjana Borisavljević - 2022 - Logica Universalis 16 (3):499-533.
    A special kind of maximum cuts in sequent derivations, actual maximum cuts, is defined. It is shown that (1) each actual maximum cut of a sequent derivation makes maximum segments in its natural deduction image, and (2) each maximum segment of a natural deduction derivation makes an actual maximum cut in its sequent image.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark