我们现在希望演示自动证明器与上述证明器E [Sch02]的应用。E是一种专门的平等证明者，通过优化的平等处理极大地缩小了搜索空间。
我们想要证明半群中的左中性元素和右中性元素是相等的。
首先，我们逐步将索赔正式化。
1 CADE是年度“自动演绎会议”[CAD]，ATP代表“自动定理证明器”。
定义3.10 结构（M，・） 由具有两个位置的集合 M 组成
1.
数学例子49
内部操作“ ・ ”如果是相关性定律则称为半群
∀ X ∀ Ý ∀ Z（X ・ Y） ・ Ž = X ・ （Y ・ Z）
成立。元素 Ë ∈中号被称为左中性（右中性）如果∀ XE ・ X = X
（ ∀
XX ・ Ë = X ）。
它仍有待证明
定理3.7如果一个半群有一个左中性元素el和一个右中性元素er，那么el = er。
显然，这适用于所有 X ∈中号说
和
el ・ x = x （3.8）
x ・ er = x。（3.9）
如果我们设置 X = ER 在（3.8 ）和 X =报在（3.9 ），我们得到两个方程埃尔・ ER = ER
和 el ・ er = el 。加入这两个方程得到
el = el ・ er = er，
我们要证明这一点。顺便说一下，在最后一步中，我们使用了等式是对称和传递的事实。
在我们应用自动化证明器之前，我们手动执行分辨率证明。首先，我们将否定查询和知识库KB形式化，由公理作为连接法线形式的子句组成：
（¬ EL = ER）1否定的查询
（m（m（x，y），z）= m（x，m（y，z）））2（m（el，x）= x）3
（m（x，er）= x）4
平等公理：
（x = x）5（反身性）
（¬ X = Ŷ ∨ Ŷ = x）的6（对称）
（¬ X = Ŷ ∨¬ Ŷ = ž ∨ X = Z）7（传递）
（¬ X = ý ∨米（X，Z）= M（Y，Z））在8取代米（¬ X = ý ∨米（Z，X）= M（Z，Y））在9取代米，
乘法由两位函数符号m表示。所述equal-两者均公理类似地配制成（ 3.1 ）页上的 36 和（ 3.2 页） 36 。一个简单的分辨率证明具有形式
RES（3，6，X 6 /米（EL，X 3）中，y 6 / X 3）：（X = M（EL，X））10
RES（7，10，X 7 / X 10，Y 7 /米（EL，X 10））
：（
¬米（EL，X）= Ž ∨ X = Z）11
RES（4，11中，x 4 / EL，X 11 / ER，Z 11 / EL） ：（ER = EL）12
RES（1，12，∅）：（）。
在此，例如，RES （ 3 ， 6 ，X 6 /米（EL，X 3 ）中，y 6 /
X 3 ）是指在第3条的分辨率与第6，可变X从第6被替换为米（el，x 3 ）与第3条中的变量x类似地，第6条中的y由第3条中的x代替。
现在我们要将证明者E应用于问题。通过映射将子句转换为子句正规形式语言LOP
（¬阿1 ∨…∨¬上午∨乙1 ∨…∨ BN）→ B1 ; …… ; Bn < – A1，…，Am。
LOP的语法表示非Horn子句的PROLOG语法的扩展（参见第5节）。因此，我们获得了E的输入文件
< – el =呃。
m（m（X，Y），Z）= m（X，m（Y，Z））。m（el，X）= X.
m（X，er）= X.
％查询
m的相关性％
％的左中性元素
m的右中性元素％
其中相等性由谓词符号gl建模。打电话给证明者
unixprompt> eproof halbgr1a.lop
＃确定问题状态，构建证明对象
＃问题状态的证据开始
1.
：[–equal（el，er）]：initial
2.
：[++
equal（m（el，X1），X1）]：initial
3.
：[++
equal（m（X1，er），X1）]：initial 3：[++ equal（el，er）]：pm（2,1）
4：[–equal（el，el）]：rw（0,3）5：[]：cn（4）
6：[]：5：{证明}
＃问题状态的证据结束
正面文字由++和负面文字识别–。在第0行到第4行中，标记为initial，再次列出输入数据中的子句。pm（a，b）代表a和b之间的解决步骤。我们看到了证明
E发现的非常类似于手动创建的证明。因为我们通过谓词gl明确地模拟了相等性，所以E的特定优势没有发挥作用。现在我们省略了等式公理并得到了
< – el =呃。
m（m（X，Y），Z）= m（X，m（Y，Z））。m（el，X）= X.
m（X，er）= X.
％查询
％Assoziativit “{a} t v.m
％linksneutrales El。v.m.
％rechtsneutrales El。v.m.
作为证明者的输入。
证明也变得更紧凑。我们在证明者的以下输出中看到证据基本上由两个相关条款1和2的单个推理步骤组成。
unixprompt> eproof halbgr1a.lop
＃确定问题状态，构建证明对象
＃问题状态的证据开始
4.
：[–equal（el，er）]：initial
5.
：[++
equal（m（el，X1），X1）]：initial
6.
：[++
equal（m（X1，er），X1）]：initial 3：[++ equal（el，er）]：pm（2,1）
4：[–equal（el，el）]：rw（0,3）5：[]：cn（4）
6：[]：5：{证明}
＃问题状态的证据结束
读者现在可以仔细研究E的功能（第 55 页的练习 3.9 ）。
