Paper Info
Title
Terminiation of permutative conversions in intuitionistic Gentzen calculi
Abstract
It is shown that permutative conversions terminate for the cut-free intuitionistic Gentzen (i.e. sequent) calculus; this proves a conjecture by Dyckhoff and Pinto. The main technical tool is a term notation for derivations in Gentzen calculi. These terms may be seen as λ-terms with explicit substitution, where the latter corresponds to the left introduction rules.
Year
DOI
Venue
1999
10.1016/S0304-3975(98)00143-1
Theor. Comput. Sci.
Keywords
DocType
Volume
Natural deduction,Termination of permutative conversions,Explicit substitution,permutative conversion,intuitionistic Gentzen calculus,Sequent term
Journal
212
Issue
ISSN
Citations 
1-2
Theoretical Computer Science
15
PageRank 
References 
Authors
4.24
2
1
Name
Order
Citations
PageRank
Helmut Schwichtenberg137344.83