这是一个非常基础的问题。我试图表达两个二元谓词（父与子）之间的对称关系。但是，使用以下语句，我的解析证明器允许我证明任何事情。转换后的CNF形式对我来说是有意义的，解析证明也是如此，但这显然应该是一个假的情况。我错过了什么？
forall x,y (is-parent-of(x,y) <-> is-child-of(y,x)) 我使用的是nltk Python库和ResolutionProver证明器。以下是nltk代码：
from nltk.sem import Expression as expfrom nltk.inference import ResolutionProver as provers = exp.fromstring('all x.(all y.(parentof(y, x) <-> childof(x, y)))')q = exp.fromstring('foo(Bar)')print prover().prove(q, [s], verbose=True)输出：
[1] {-foo(Bar)} A [2] {-parentof(z9,z10), childof(z10,z9)} A [3] {parentof(z11,z12), -childof(z12,z11)} A [4] {} (2, 3) True回答：
这里是ResolutionProver的一个快速修复方案。
导致证明器不健全的问题在于，当存在多个互补文字时，它没有正确实现解析规则。例如，给定子句{A B C}和{-A -B D}，二元解析将产生子句{A -A C D}和{B -B C D}。这两个都会被作为重言式丢弃。当前的NLTK实现反而会产生{C D}。
这可能是因为在NLTK中，子句被表示为列表，因此相同的文字可能在一个子句中出现多次。这个规则在应用于子句{A A}和{-A -A}时确实能产生空子句，但总的来说，这个规则是不正确的。
看起来，如果我们保持子句不重复相同的文字，我们可以通过一些修改来恢复健全性。
首先定义一个移除相同文字的函数。
以下是这种函数的一个简单实现
现在我们可以将这个函数插入到nltk.inference.resolution模块的一些函数中。
def _iterate_first_fix(first, second, bindings, used, skipped, finalize_method, debug): """ 此方法有助于遍历'self'的条目 """ debug.line('unify(%s,%s) %s'%(first, second, bindings)) if not len(first) or not len(second): #如果无法继续递归 return finalize_method(first, second, bindings, used, skipped, debug) else: #探索这个'self'原子 result = res._iterate_second(first, second, bindings, used, skipped, finalize_method, debug+1) #跳过这个可能的'self'原子 newskipped = (skipped[0]+[first[0]], skipped[1]) result += res._iterate_first(first[1:], second, bindings, used, newskipped, finalize_method, debug+1) try: newbindings, newused, unused = res._unify_terms(first[0], second[0], bindings, used) #找到了统一，所以继续这条统一线 #将跳过的和未使用的条目重新投入到后续的统一中。 newfirst = first[1:] + skipped[0] + unused[0] newsecond = second[1:] + skipped[1] + unused[1] #当`_unify_term()`成功时，我们立即返回 result += _simplify(finalize_method(newfirst,newsecond,newbindings,newused,([],[]),debug)) except res.BindingException: pass return resultres._iterate_first=_iterate_first_fix类似地更新res._iterate_second
def _iterate_second_fix(first, second, bindings, used, skipped, finalize_method, debug): """ 此方法有助于遍历'other'的条目 """ debug.line('unify(%s,%s) %s'%(first, second, bindings)) if not len(first) or not len(second): #如果无法继续递归 return finalize_method(first, second, bindings, used, skipped, debug) else: #跳过这个可能的配对并移动到下一个 newskipped = (skipped[0], skipped[1]+[second[0]]) result = res._iterate_second(first, second[1:], bindings, used, newskipped, finalize_method, debug+1) try: newbindings, newused, unused = res._unify_terms(first[0], second[0], bindings, used) #找到了统一，所以继续这条统一线 #将跳过的和未使用的条目重新投入到后续的统一中。 newfirst = first[1:] + skipped[0] + unused[0] newsecond = second[1:] + skipped[1] + unused[1] #当`_unify_term()`成功时，我们立即返回 result += _simplify(finalize_method(newfirst,newsecond,newbindings,newused,([],[]),debug)) except res.BindingException: #原子无法统一， pass return resultres._iterate_second=_iterate_second_fix最后，将我们的函数插入到clausify()中，以确保输入没有重复。
def clausify_simplify(expression): """ 斯柯伦化、子句化，并标准化变量分离。 """ clause_list = [] for clause in res._clausify(res.skolemize(expression)): for free in clause.free(): if res.is_indvar(free.name): newvar = res.VariableExpression(res.unique_variable()) clause = clause.replace(free, newvar) clause_list.append(_simplify(clause)) return clause_listres.clausify=clausify_simplify应用这些更改后，证明器应该能够运行标准测试，并且正确处理parentof/childof关系。
print res.ResolutionProver().prove(q, [s], verbose=True)输出：
[1] {-foo(Bar)} A [2] {-parentof(z144,z143), childof(z143,z144)} A [3] {parentof(z146,z145), -childof(z145,z146)} A [4] {childof(z145,z146), -childof(z145,z146)} (2, 3) 重言式[5] {-parentof(z146,z145), parentof(z146,z145)} (2, 3) 重言式[6] {childof(z145,z146), -childof(z145,z146)} (2, 3) 重言式False更新：实现正确性并不是故事的结局。一个更有效的解决方案是用基于Python内置哈希集的容器替换Clause类中存储文字的容器，但这似乎需要对证明器实现进行更彻底的重新设计，并引入一些性能测试基础设施。
