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

Question

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

的公式有一定的限制相比，“全”一阶公式：

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

我可以改变这些公式在子句中的正常形式，我有文字统一的例程。但是我不确定如何继续，如果这个问题是可以确定的。

Answer 1

如所提到的，以证明˚F< =“G其中两个闭合（普遍量化）式中，你需要证明F =”G并且还G =>˚F。为了证明这两个公式的每一个，你可以使用各种结石。我将描述[分辨率演算]：

• 否定猜想，所以F =“G变得˚F& -G。
• 转换为CNF。
• 运行解决程序。
• 如果你得到一个空子句，你已经证明了原始猜想F => G。如果搜索饱和并且不能得出更多的新条款，则猜想不成立。

在你的条件下，所有原子公式从˚F未来将是摹只适用于变量和所有原子公式将是谓语符号谓词符号只适用TOTO斯科伦常量。所以解析过程只会产生替换，或者将变量映射到其他变量，或者将变量映射到这些skolem常量。这意味着它只能导出有限数量的不同文字，因此解决程序将始终停止 - 这将是可确定的。

---

您也可以使用自动化工具来达到这个目的，它将为您完成所有工作。我使用The E Theorem Prover来解决这些问题。作为输入语言，我使用The TPTP Problem Library的语言，这对人类来说很容易读/写。

举个例子：输入文件：

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