构造逻辑中Skolem定理的构造性证明
摘要：如果在一阶构造性自然演绎中可推导得出的序列(Gamma entails forall x exists y A)，则理论(Gamma, forall x (f (x)/y)A)，其中f是一个新的函数符号，是Gamma的一个保守扩展。
作者：Gilles Dowek (DEDUCTEAM), Benjamin Werner (PARTOUT)
论文ID：2305.10016
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-18