埃尔布朗定理

在逻辑学中,赫尔不兰特定理(Herbrand's theorem)建立了命题逻辑计算和谓词逻辑计算之间的关系,因此赫尔不兰特定理可能是一种确定的手段来判断一个命题的命题逻辑计算是否是有限的,对于一个含有复杂谓词的公式,它的谓词逻辑计算也起到同样的作用。通过对赫尔不兰特定理的应用,部分回答了上述问题。虽然有Gödel, Tarski, Church, Turing和其他科学家在逻辑学领域的研究成果,但是目前不存在这样一个已经被证明了的算法,也就是能够决定对于一个普遍的公式的谓词逻辑计算。