Herbrand公式的无Skolemization判定方法
A Decision Procedure for Herbrand Formulae without Skolemization
摘要：
本文描述了一个判断量词范围内不含$\vee$的纯一阶逻辑反前束范式（FOLDNF）合取词的析取的过程。这些FOLDNF的析取等价于前束范式，其无量词部分是原子公式和否定原子公式（= Herbrand公式）的合取。与Herbrand公式的通常算法不同，该算法既不使用Skolemization算法，也不使用带函数符号的统一算法。相反，一个过程中描述的是依赖于纯粹的一阶逻辑（FOL）内的等价变换。这个过程涉及到负范式演算（NNF演算）的应用，其中$A \dashv\vdash A \wedge A$（= $\wedge$ I）作为增加给定FOLDNF复杂性的唯一规则。所描述的算法说明了如何在Herbrand公式的情况下，决策问题可以通过系统搜索证明来解决，该证明将规则$\wedge$ I的应用数量减少到最小，在NNF演算中。在Herbrand公式的情况下，甚至可以完全放弃应用$\wedge$ I。最后，它示出了如何描述的程序可以使用在一个优化的一般搜索矛盾的证据和什么样的问题出现的情况下，一般搜索矛盾的证据的$\wedge$ I-最小的证明策略。
英文摘要：
This paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain $\vee$ within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described that rests on nothing but equivalence transformations within pure first-order logic (FOL). This procedure involves the application of a calculus for negative normal forms (the NNF-calculus) with $A \dashv\vdash A \wedge A$ (= $\wedge$I) as the sole rule that increases the complexity of given FOLDNFs. The described algorithm illustrates how, in the case of Herbrand formulae, decision problems can be solved through a systematic search for proofs that reduce the number of applications of the rule $\wedge$I to a minimum in the NNF-calculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying $\wedge$I. Finally, it is shown how the described procedure can be used within an optimized general search for proofs of contradiction and what kind of questions arise for a $\wedge$I-minimal proof strategy in the case of a general search for proofs of contradiction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
