Lower bounds on Herbrand’s theorem
Lower bounds on Herbrand’s theorem
复制标题
赫布兰德定理的下界
DOI：
10.1090/s0002-9939-1979-0529224-9
复制
发表时间：
1979
影响因子：
1.3
通讯作者：
R. Statman
中科院分区：
文献类型：
--
作者：
R. Statman
我们通过赫布兰德定理给出了消除量词推论的非卡尔玛基本下界。 I. 赫布兰德定理的一个特例如下：设 X 为方程组，VX 为 X 成员的通用闭包集，X* 为 X 成员的闭替换实例集；那么，对于所有闭方程 E，
We give non Kalmar-elementary lower bounds on the elimination of quantifier inferences via Herbrand's theorem. I. A special case of Herbrand's theorem says the following: Let X be a set of equations, VX the set of universal closures of members of X, and X* the set of closed substitution instances of members of X; then, for all closed equations E,