Switch to: References

Add citations

You must login to add citations.
  1. Strong Normalization via Natural Ordinal.Daniel Durante Pereira Alves - 1999 - Dissertation,
    The main objective of this PhD Thesis is to present a method of obtaining strong normalization via natural ordinal, which is applicable to natural deduction systems and typed lambda calculus. The method includes (a) the definition of a numerical assignment that associates each derivation (or lambda term) to a natural number and (b) the proof that this assignment decreases with reductions of maximal formulas (or redex). Besides, because the numerical assignment used coincide with the length of a specific sequence of (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Types of I -free hereditary right maximal terms.Katalin Bimbó - 2005 - Journal of Philosophical Logic 34 (5/6):607 - 620.
    The implicational fragment of the relevance logic "ticket entailment" is closely related to the so-called hereditary right maximal terms. I prove that the terms that need to be considered as inhabitants of the types which are theorems of $T_\rightarrow$ are in normal form and built in all but one casefrom B, B' and W only. As a tool in the proof ordered term rewriting systems are introduced. Based on the main theorem I define $FIT_\rightarrow$ - a Fitch-style calculus (related to (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Relevant predication 1: The formal theory. [REVIEW]J. Michael Dunn - 1987 - Journal of Philosophical Logic 16 (4):347-381.
    Download  
     
    Export citation  
     
    Bookmark   38 citations  
  • Types of $\mathsf{I}$ -Free Hereditary Right Maximal Terms.Katalin Bimbó - 2005 - Journal of Philosophical Logic 34 (5-6):607-620.
    The implicational fragment of the relevance logic "ticket entailment" is closely related to the so-called hereditary right maximal terms. I prove that the terms that need to be considered as inhabitants of the types which are theorems of $T_\rightarrow$ are in normal form and built in all but one casefrom B, B' and W only. As a tool in the proof ordered term rewriting systems are introduced. Based on the main theorem I define $FIT_\rightarrow$ - a Fitch-style calculus for the (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations