问题：设 A，B，C 三些人从不说实话，有些人从不说谎。有人问这三个人同样的问题:谁是谎者？A 答：“ B 和 C 都是说谎者；B 答：“ A 和 C 都是说谎者；C答：“ A 和 B 至少有一个是说谎者。谁是老实人，谁是说谎者？

答案：C 是老实人，A、B 是说谎者。

• 鲁滨逊归结原理永真的证明转化为不满意的证明。
• 反证法：P ? Q ，当且仅当 P∧～Q ? F ，即 Q 为 P 逻辑结论，当，仅当 P∧～Q 不能满足。
• 海伯伦(Herbrand)定理为自动定理证明奠定了基础理论基础。
• 鲁滨逊(Robinson)归结原理使机器定理证成为现实。

定理证明应用归结原理的步骤如下：

• 可以用谓词公式来表示以下形式：A1∧A2∧…∧An ? B
  1. 首先否定结论 B ，并将否定公式~B 谓词公式与前提公式集成如下： G= A1∧A2∧…∧An∧～B。
  2. 求谓词公式 G的子句集 S。
  3. 应用归结原理，证明子句集 S 不满，这证明了谓词公式G的不满。这表明了结论 B 否定是错误的，推断定理的建立。

解决问题的步骤：

1. 先决条件已知用谓词公式表示，并化成相应的子句集，该子句集的名称为 S 1 S_{1} S1。
2. 把待求解的问题也以谓词公式表示，然后将其否定，并与一谓词ANSWER构成析取式。谓词 ANSWER 为解决问题而设置的谓词，其变量必须与问题公式的变量完全一致。
3. 问题公式和谓词 ANSWER 构成的分析式化为子句集，并将该子句集与 S1 合并构成子句集 S。
4. 对子句集 S 应用谓词归结原理归结，在归结过程中，通过合一替换进行改变ANSWER中的变元。
5. 若得到归结式 ANSWER，则问题的答案即在 ANSWER 谓词中。