python - Python NLTK ResolutionProver 在实际上没有解决方案时找到了解决方案

Question

我有这样的格式规则“如果 A&B 则 C”： 如果b 是_man并且s 是 b 的妹妹，那么b 是 s 的兄弟

我添加了is_man(luc)的事实，并且我请求Brother_of(b,leia)是否有任何“b”

我希望答案是否定的，因为没有说 leia 是 luc 的姐妹，所以在我的规则“如果 A&B 则 C”中，B 部分不正确，但是 ResolutionProver 出人意料地回答了“luc”？？！？

import nltk.inference
rexp = nltk.sem.Expression.fromstring
p1 = rexp('is_man(luc)')
p2 = rexp('(is_man(b) & sister_of(s,b)) -> brother_of(b,s)')
answer = rexp('brother_of(b,leia) -> ANSWER(b)')
tp = nltk.ResolutionProverCommand(None, [p1,p2,answer])
if list(tp.find_answers()): 
    for ans in list(tp.find_answers()): print(ans,end=' ')
else: print('No answer')

它不应该回答 Luc 而是 False，我怎样才能得到 False ？并且只有在我另外声明 Sister_of(leia,luc) 的情况下才获得“luc”。谢谢 ！

PS：有关信息，这是证明：

[1] {is_man(luc)}                                                  A  (that is p1)
[2] {-is_man(z368), -sister_of(z369,z368), brother_of(z368,z369)}  A  (that is p2)
[3] {-brother_of(z370,leia), ANSWER(z370)}                         A  (that is answer)
[4] {-sister_of(z369,luc), brother_of(luc,z369)}                   (1, 2)  (combination of 1 & 2)
[5] {ANSWER(z370), -is_man(z370), -sister_of(leia,z370)}           (2, 3) 
[6] {-sister_of(leia,luc), ANSWER(luc)}                            (1, 5) 
[7] {-sister_of(leia,luc), ANSWER(luc)}                            (3, 4) 

标签： pythonnltkresolutionsolverinference