参考答案：

给出一个公式集S和目标公式L，通过反证或反演来求证目标公式L，其证明步骤如下：

（1）否定L，得～L；

（2）把～L添加到S中去；

（3）把新产生的集合｛～L，S｝化成子句集；

（4）应用消解原理，力图推导出一个表示矛盾的空子句NIL。