Paper Info
Title
Existential Instantiation and Strong Normalization
Abstract
We present a new manageable formulation of natural deduction with a rule of existential instantiation xA[x]/A[b]. It simplifies skolemizing devices of earlier formulations, includes a new rule for disjunction and admits a proof of strong normalization. This opens way to the treatment of new systems for which only normal form theorems are known.
Year
DOI
Venue
1997
10.1007/3-540-63045-7_26
LFCS
Keywords
Field
DocType
existential instantiation,strong normalization,normal form,natural deduction
Existential instantiation,Discrete mathematics,Normalization (statistics),Algebra,Computer science,Natural deduction
Conference
ISBN
Citations 
PageRank 
3-540-63045-7
3
0.58
References 
Authors
2
1
Name
Order
Citations
PageRank
Grigori Mints123572.76