对称二元谓词的基本一阶逻辑推理失败
Basic first order logic inference fails for symmetric binary predicate
超级基础的问题。我试图表达两个二元谓词(父项和子项)之间的对称关系。但是,通过以下陈述,我的决议证明者可以让我证明任何事情。转换后的 CNF 形式对我来说很有意义,通过解析证明也是如此,但这应该是一个明显的错误案例。我错过了什么?
forall x,y (is-parent-of(x,y) <-> is-child-of(y,x))
我正在使用 nltk python 库和 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
这是 ResolutionProver 的快速修复。
导致prover不健全的问题是当有多个互补字面量时,它没有正确执行解析规则。例如。给定子句 {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
class 中存储文字的容器替换为基于内置 Python 哈希集的容器,但这似乎需要一个对证明者实施进行更彻底的返工,并引入一些性能测试基础设施。
超级基础的问题。我试图表达两个二元谓词(父项和子项)之间的对称关系。但是,通过以下陈述,我的决议证明者可以让我证明任何事情。转换后的 CNF 形式对我来说很有意义,通过解析证明也是如此,但这应该是一个明显的错误案例。我错过了什么?
forall x,y (is-parent-of(x,y) <-> is-child-of(y,x))
我正在使用 nltk python 库和 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
这是 ResolutionProver 的快速修复。
导致prover不健全的问题是当有多个互补字面量时,它没有正确执行解析规则。例如。给定子句 {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
class 中存储文字的容器替换为基于内置 Python 哈希集的容器,但这似乎需要一个对证明者实施进行更彻底的返工,并引入一些性能测试基础设施。