Prover9/Mace4 的形式化语言简介（二）
语法示例
下面是一个简单的例子，尝试证明群论中的一条性质（左单位元也是右单位元）。注意，此性质不一定成立，取决于具体的公理定义，这里仅作语法演示：
formulas(assumptions). % 公理/假设部分
all x (x * e = x). % e 是左单位元
all x (e * x = x). % e 也是右单位元？ (这是我们想证明的目标，但这里作为假设列出仅用于演示语法，实际证明中它应放在goal部分)
all x all y all z ((x * y) * z = x * (y * z)). % 结合律
end_of_list.
formulas(goals). % 目标部分
all x (x * e = x) -> all x (e * x = x). % 如果左单位元存在，则它也是右单位元 (这个蕴含关系不一定成立！)
end_of_list.
说明：
- all x (...) 表示 $\forall x (...)$。
- * 是一个二元函数（群运算）。
- e 是一个常量（单位元）。
- -> 表示逻辑蕴含。
- formulas(assumptions). 和 formulas(goals). 分别标记假设和目标块的开始，end_of_list. 标记结束。
Mace4 的输入
Mace4 的输入语法与 Prover9 非常相似。用户同样提供一组公式（公理）。Mace4 的任务是寻找一个有限的数学结构（模型），使得这些公理在该结构中同时为真。如果公理集存在矛盾，Mace4 会报告找不到模型。如果猜想可能不成立，用户可以将猜想（或其否定）加入公理集，让 Mace4 寻找反例模型。
输出
- Prover9：如果证明成功，它会输出一个详细的、人类（经过训练）可读的证明过程。
- Mace4：如果找到模型，它会输出模型的详细描述，包括：
- 论域（Domain）的大小和元素（通常是整数 0, 1, 2, ..., n-1）。
- 常量的解释（映射到哪个域元素）。
- 函数的解释（对每个可能的输入组合，给出输出值）。
- 谓词的解释（列出所有满足该谓词的元素组合）。
总结
Prover9 和 Mace4 的形式化语言提供了一种相对简洁的方式来描述一阶逻辑（特别是涉及等式）中的数学问题。用户通过声明公理和目标，即可利用强大的自动化工具进行定理证明或反例查找。虽然学习这套语言需要一定的逻辑基础，但它为研究逻辑性质、验证猜想提供了非常实用的自动化手段。