如何自动证明两个一阶公式是等价的

Question

自动证明两个一阶公式F和G等价的最佳方法是什么？

与"完整"一阶公式相比，这些公式有一些限制：

1. 无量词
2. 无功能
3. 隐含普遍量化

我可以将这些公式转换为子句范式，并且我有用于统一文本的例程。然而，我不确定如何继续，以及这个问题是否可以决定。

Answer 1

如前所述，证明F<=>G如果两者都是封闭的（普遍量化的）公式，则需要证明F=>G=>F。为了证明这两个公式中的每一个，你可以使用各种各样的结石。我将描述[分辨率演算]：

• 否定猜想，所以F=>G变成F&amp-G
• 转换为CNF
• 运行解析过程
• 如果你推导出一个空子句，你就证明了最初的猜想F=>G。如果搜索饱和，再也不能派生出新的子句，那么这个猜想就不成立了

在您的条件下，来自F的所有原子公式都将是仅应用于变量的谓词符号，而来自G所有原子公式将是仅适用于skolem常量的谓词符号。因此，解析过程只会产生将变量映射到其他变量或将变量映射为这些skolem常量的替换。这意味着它只能导出有限数量的不同文字，因此解析过程将始终停止——它将是可判定的。

---

您也可以为此目的使用自动化工具，它将为您完成所有工作。我用E定理的证明来解决这些问题。作为输入语言，我使用TPTP问题库的语言，它对人类来说很容易读/写。

举个例子：输入文件：

fof(my_formula_name, conjecture, (![X]: p(X)) <=> (![Y]: p(Y)) ).

然后我运行

eprover --tstp-format -xAuto -tAuto myfile

（-tAuto和-xAuto进行一些自动配置，在您的情况下很可能不需要），结果是

# Garbage collection reclaimed 59 unused term cells.
# Auto-Ordering is analysing problem.
# Problem is type GHNFGFFSF00SS
# Auto-mode selected ordering type KBO6
# Auto-mode selected ordering precedence scheme <invfreq>
# Auto-mode selected weight ordering scheme <precrank20>
#
# Auto-Heuristic is analysing problem.
# Problem is type GHNFGFFSF00SS
# Auto-Mode selected heuristic G_E___107_C41_F1_PI_AE_Q4_CS_SP_PS_S0Y
# and selection function SelectMaxLComplexAvoidPosPred.
#
# No equality, disabling AC handling.
#
# Initializing proof state
#
#cnf(i_0_2,negated_conjecture,(~p(esk1_0)|~p(esk2_0))).
#
#cnf(i_0_1,negated_conjecture,(p(X1)|p(X2))).
# Presaturation interreduction done
#
#cnf(i_0_2,negated_conjecture,(~p(esk1_0)|~p(esk2_0))).
#
#cnf(i_0_1,negated_conjecture,(p(X2)|p(X1))).
#
#cnf(i_0_3,negated_conjecture,(p(X3))).
# Proof found!
# SZS status Theorem
# Parsed axioms                        : 1
# Removed by relevancy pruning         : 0
# Initial clauses                      : 2
# Removed in clause preprocessing      : 0
# Initial clauses in saturation        : 2
# Processed clauses                    : 5
# ...of these trivial                  : 0
# ...subsumed                          : 0
# ...remaining for further processing  : 5
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 1
# Backward-rewritten                   : 1
# Generated clauses                    : 4
# ...of the previous two non-trivial   : 4
# Contextual simplify-reflections      : 0
# Paramodulations                      : 2
# Factorizations                       : 2
# Equation resolutions                 : 0
# Current number of processed clauses  : 1
#    Positive orientable unit clauses  : 1
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 0
#    Non-unit-clauses                  : 0
# Current number of unprocessed clauses: 0
# ...number of literals in the above   : 0
# Clause-clause subsumption calls (NU) : 0
# Rec. Clause-clause subsumption calls : 0
# Unit Clause-clause subsumption calls : 1
# Rewrite failures with RHS unbound    : 0
# Indexed BW rewrite attempts          : 4
# Indexed BW rewrite successes         : 4
# Unification attempts                 : 12
# Unification successes                : 9
# Backwards rewriting index :     2 leaves,   1.00+/-0.000 terms/leaf
# Paramod-from index        :     1 leaves,   1.00+/-0.000 terms/leaf
# Paramod-into index        :     1 leaves,   1.00+/-0.000 terms/leaf

其中最重要的线路是

# Proof found!
# SZS status Theorem