向大家请教一个关于谓词公式的自动证明问题

Question

具体的题目是这样的：
由于各个子句之间是与的关系，所以只要归结产生空子句就可以证明结论是假的
应用归结原理证明
P,Q,R等大写字母代表谓词公式名称
x,y,z等代表变量
a,b,c代表常量输入子句：
（1）!P(a)∨Q(x,b)
（2）p(y)
（3）!Q(x,z)输出归结过程：
 (4)Q(x,a)      （1）与（2），置换式：a/y
 (5)nill        （3）与（4），置换式：b/z
 归结出空子句成功！以上是一个简单的归结过程，但是我知道用java语言怎么实现，请知道的告诉小弟一下