我有这个格式规则"如果A&B然后C"：如果b是_man，并且s是b的姐妹，则b是s的兄弟
我添加了一个事实，即is_man(luc(，并且我请求妹夫_of(b，leia(是否有任何"b">
我希望答案是否定的，因为没有说leia是luc的姐妹，所以在我的规则中"如果A&B然后C">B部分不是真的，但ResolutionProvert出人意料地回答了"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？只有在我声明姐妹(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)
我对这个问题发表了评论：https://github.com/nltk/nltk/issues/3046
问题是nltk.sem.logic中ResolutionProverCommand类中的函数find_answers()检查ANSWER((，但不检查空子句是否派生。