Prover9测试失败：将假设设为目标验证出现报错求助

我来帮你捋清楚这个问题——你遇到的"denials share constants"警告和"search failed"其实是用Prover9测试时的典型小坑，尤其是当你直接把假设里的具体事实当成目标来证明的时候。

先搞懂警告的本质 #

Prover9是靠反证法工作的：它会先否定你的目标，把否定后的语句加入到假设集合里，然后尝试推导出矛盾。当你把一个已经在假设里存在的带具体常量的事实（比如parent(adam, jill)）设为目标时，它会生成否定语句-parent(adam, jill)，这就和原假设里的事实直接矛盾了。但"denials share constants"警告是在提醒你：否定后的目标和现有假设共享所有的常量（比如adam、jill这些），这会让Prover9的搜索策略陷入低效循环，甚至直接终止搜索，因为它找不到有意义的推导路径。

具体的解决步骤 #

1. 调整假设与目标的划分

如果你就是要验证某条已知事实，正确的做法是把这条事实从assumptions里移到goals里，剩下的作为前提。比如修改你的输入文件：

formulas(assumptions).
parent(eve, jill).
parent(adam, bill).
parent(eve, bill).
parent(ed, mary).
% 把要证明的那条从假设中移除
end_of_list.

formulas(goals).
parent(adam, jill). % 这是你要验证的目标
end_of_list.

这样Prover9就会用剩下的假设（如果有逻辑关联的话）来推导目标，而不是带着矛盾的前提去做无意义的搜索。

2. 修复输入文件的语法问题

你提供的输入最后有pare...，这明显是内容截断了。一定要确保所有公式完整，每个公式块（assumptions和goals）都以end_of_list.结尾，语法错误也会直接导致Prover9搜索失败。

3. 换个更适合测试的场景

如果只是想测试Prover9是否正常工作，建议用需要推导的目标，而不是直接验证已知事实。比如：

formulas(assumptions).
parent(adam, jill).
parent(eve, jill).
female(eve).
mother(X,Y) <-> parent(X,Y) & female(X).
end_of_list.

formulas(goals).
mother(eve, jill).
end_of_list.

这个场景下Prover9需要通过组合前提来推导目标，能更直观地看到它的工作效果。

内容的提问来源于stack exchange，提问作者callum perks