4.4 基于归结法的问答系统

　　通过前面的介绍，我们已经知道，当一个结论成立时，归结法可以证明该结论成立。对于一个类似于这样的结论：(x)W(x)，证明(x)W(x)成立固然重要，但有时我们可能更关心的是使得W(x)成立的那个x是什么，也就是说，我们希望得到问题的答案。基于归结的问答就是利用归结方法获得问题答案的方法。其基本方法是先用归结法证明问题的正确性，给出归结树。然后再根据该归结树构造一个修改证明树。构造的方法是：将结论的否定对应的子句S1，再次求反得到一个新子句S2，用S1与S2构造一个重言式S1∨S2，用该重言式代替归结树中的子句S1，并参予有关的置换。最后在归结树得到空子句的地方得到的子句就是问题的回答。