从归结反演中提取问题解答　

    在定理证明系统中有这样一类问题，在目标公式中含有存在量词量化的变量。如果目标公式成立的话，我们希望知道这个变量的一个例。对于更一般的问题，如果已经证明了一个问题存在解，我们希望得到这个解，问题在于从证明过程中提取问题的解答。本节介绍从归结反演中提取解答的问题。

    1、提取解答的基本过程

       将通过几个具体例子来说明

    2、目标公式含有全称量词的情况

       将通过几个具体例子来说明

    3、解答提取过程的一般步骤