对称二进制谓词的基本一阶逻辑推理失败

Question

超级基本的问题。我试图表达两个二进制谓词(父谓词和子谓词)之间的对称关系。但是，有了下面的陈述，我的决议证明器允许我证明任何事情。转换后的CNF表格对我来说是有意义的，通过决议证明也是有意义的，但这应该是一个明显的错误案例。我遗漏了什么？

forall x,y (is-parent-of(x,y) <-> is-child-of(y,x)) 

我正在使用nltk库和ResolutionProver验证程序。以下是nltk代码：

from nltk.sem import Expression as exp
from nltk.inference import ResolutionProver as prover

s = 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

Answer 1

以下是ResolutionProver的快速修复。

导致验证程序不健全的问题是，当有多个互补文本时，它没有正确地实现解析规则。例如，给定子句，{A B C}和{-A -B D}，二进制解析将产生子句{A -A C D}和{B -B C D}。这两者都会作为重言之词被抛弃。相反，当前的NLTK实现将生成{C D}。

这可能是因为子句在NLTK中表示为列表，因此相同的文本可能在一个子句中出现不止一次。当应用于子句{A A}和{-A -A}时，此规则确实会正确地生成空子句，但通常情况下，此规则是不正确的。

看来，如果我们使从句不重复相同的文字，我们可以恢复健全，只要稍加修改。

首先，定义一个删除相同文字的函数。

下面是这样一个函数的简单实现

import nltk.inference.resolution as res

def _simplify(clause):
    """
    Remove duplicate literals from a clause
    """
    duplicates=[]
    for i,c in enumerate(clause):
       if i in duplicates:
          continue
       for j,d in enumerate(clause[i+1:],start=i+1):
          if j in duplicates:
             continue
          if c == d:
               duplicates.append(j)
    result=[]
    for i,c in enumerate(clause):
        if not i in duplicates:
           result.append(clause[i])
    return res.Clause(result)

现在，我们可以将这个函数插入到nltk.inference.resolution模块的一些功能中。

def _iterate_first_fix(first, second, bindings, used, skipped, finalize_method, debug):
    """
    This method facilitates movement through the terms of 'self'
    """
    debug.line('unify(%s,%s) %s'%(first, second, bindings))

    if not len(first) or not len(second): #if no more recursions can be performed
        return finalize_method(first, second, bindings, used, skipped, debug)
    else:
        #explore this 'self' atom
        result = res._iterate_second(first, second, bindings, used, skipped, finalize_method, debug+1)

        #skip this possible 'self' atom
        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)
            #Unification found, so progress with this line of unification
            #put skipped and unused terms back into play for later unification.
            newfirst = first[1:] + skipped[0] + unused[0]
            newsecond = second[1:] + skipped[1] + unused[1]

            # We return immediately when `_unify_term()` is successful
            result += _simplify(finalize_method(newfirst,newsecond,newbindings,newused,([],[]),debug))
        except res.BindingException:
            pass
    return result
res._iterate_first=_iterate_first_fix

类似地更新res._iterate_second

def _iterate_second_fix(first, second, bindings, used, skipped, finalize_method, debug):
    """
    This method facilitates movement through the terms of 'other'
    """
    debug.line('unify(%s,%s) %s'%(first, second, bindings))

    if not len(first) or not len(second): #if no more recursions can be performed
        return finalize_method(first, second, bindings, used, skipped, debug)
    else:
        #skip this possible pairing and move to the next
        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)
            #Unification found, so progress with this line of unification
            #put skipped and unused terms back into play for later unification.
            newfirst = first[1:] + skipped[0] + unused[0]
            newsecond = second[1:] + skipped[1] + unused[1]

            # We return immediately when `_unify_term()` is successful
            result += _simplify(finalize_method(newfirst,newsecond,newbindings,newused,([],[]),debug))
        except res.BindingException:
            #the atoms could not be unified,
            pass

    return result
res._iterate_second=_iterate_second_fix

最后，将我们的函数插入到clausify()中，以确保输入不重复。

def clausify_simplify(expression):
    """
    Skolemize, clausify, and standardize the variables apart.
    """
    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_list
res.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) Tautology
[5] {-parentof(z146,z145), parentof(z146,z145)}  (2, 3) Tautology
[6] {childof(z145,z146), -childof(z145,z146)}    (2, 3) Tautology

False

更新:实现正确性的并不是故事的结尾。一个更有效的解决方案是将用于在Clause类中存储文本的容器替换为基于内置Python哈希集的容器，但是这似乎需要对验证程序实现进行更彻底的重新工作，并引入一些性能测试基础设施。