A note on the existence property for intuitionistic logic with function symbols
A note on the existence property for intuitionistic logic with function symbols
复制标题
关于带函数符号的直觉逻辑的存在性的注记
DOI：
10.1002/malq.19900360104
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
L. M. Doorman
中科院分区：
文献类型：
--
作者：
L. M. Doorman
The article focuses on the existence property (EP) for intuitionistic first-order logic with function symbols. It states that Kurt Gödel was the first one who proved the property in elementary number theory. It mentions the use of unification algorithm to minimize the arbitrarily complex terms caused by derivation. It says that the proof for the EP consists of Prawitz'argument and unification.
