子句包含算法

自动定理证明的一个重要部分是通过找出一个子句何时包含另一个子句来减少冗余。

有一些索引技术可以大大减少必须进行的包含尝试的次数,但是即使如此,包含也会消耗大量的CPU时间,因此优化它非常重要。显然,在一般情况下,这是NP难的,但仍然有可能和必要使大多数特殊情况快速运行。

下面的伪代码是正确的,但效率低下。(在实践中,负的和正的文字必须分开处理,然后还有一些问题,比如尝试用两种方法都指向方程,但这里我只考虑匹配两包文字的核心算法。)

def match_clauses(c, d, map):
    if c == {}:
        return true
    for ci in c:
        for di in d:
            if match_terms(ci, di, map):
                if match_clauses(c - ci, d - di, map):
                    return true
    return false

为什么效率低?考虑这两个条款 p(x) | q(y) | r(42) p(x) | q(y) | r(54) . 上述算法将首先成功匹配 p(x) q(y) ,然后注意 r(42) 不匹配 r(54) . 好吧,但它会反过来尝试:首先成功匹配 ,则成功匹配 p(x) ,然后再次通知 r(42) 不匹配 r(54)

如果给我足够的时间,我无疑能找到更好的算法,但其他人肯定在我之前就已经做了这件事,所以似乎值得问:最著名的算法是什么?