"快乐学生"问题：
假设任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有的考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。
解：
先将问题用谓词表示如下：
R1:"任何通过计算机考试并获奖的人都是快乐的"
(
x)((Pass(x,
computer)∧Win(x, prize))→Happy(x))R2:"任何肯学习或幸运的人都可以通过所有考试"
(
x)(y)(Study(x)∨Lucky(x)→Pass(x,
y))R3:"张不肯学习但他是幸运的"
～Study(zhang)∧Lucky(zhang)
R4:"任何幸运的人都能获奖"
(
x)(Luck(x)→Win(x,prize))结论"张是快乐的"的否定
～Happy(zhang)
将上述谓词公式转化为子句集并进行归结如下：
首先将每一个表示逻辑条件的谓词子句转换为子句集可以接受的Skolem标准形。
由R1及逻辑转换公式:P∧W→H = ～（P∧W）∨ H ，可得
(1) ～Pass(x, computer)∨～Win(x, prize)∨Happy(x)
由R2可得
(2) ～Study(y)∨Pass(y,z)
(3) ～Lucky(u)∨Pass(u,v)
由R3可得
(4) ～Study(zhang)
(5) Lucky(zhang)
由R4可得
(6) ～Lucky(w)∨Win(w，prize)
由结论可得
(7) ～Happy(zhang) 结论的否定
根据以上7条子句，归结如下：
(8) ～Pass(w, computer)∨Happy(w)∨～Luck(w) (1)，(6)归结，{w/x}
(9) ～Pass(zhang, computer)∨～Lucky(zhang) (8)，(7)归结，{zhang/w}
(10) ～Pass(zhang, computer) (9)，(5)归结
(11) ～Lucky(zhang) (10),(3)归结,{zhang/u, computer/v}
(12) (11),(5)归结
结论
1．归结法的实质：
・归结法是仅有一条推理规则的推理方法。
・归结的过程是一个语义树倒塌的过程。
2．归结法的问题
・对于传统归结法，子句中有等号或不等号时，完备性不成立。即，传统的归结法不能处理相等的关系。
Herbrand定理式归结原理的理论基础；而正是由于Herbrand定理的不实用性引出了可实用的归结法。