2. 实验任务
编写程序，实现一阶逻辑归结算法，并用于求
解给出的三个逻辑推理问题，要求输出按照如
下格式：
16
1. (P(x),Q(g(x)))
2. (R(a),Q(z),¬P(a))
3. R[1a,2c]{X=a} (Q(g(a)),R(a),Q(z))
… …
“R” 表示归结步骤.
“1a” 表示第一个子句(1-th)中的第一个 (a-th)个原子公式，即P(x).
“2c”表示第二个子句(1-th)中的第三个 (c-th)个原子公式，即¬P(a).
“1a”和“2c”是冲突的，所以应用最小合一{X = a}.
评论0