3

2 つの 1 次式 F と G が等しいことを自動的に証明する最良の方法は何ですか?

式には、「完全な」一次式と比較していくつかの制限があります。

  1. 量指定子なし
  2. 機能フリー
  3. 暗黙的に普遍的に量化された

これらの式を句の標準形に変換でき、リテラルの統一のためのルーチンがあります。ただし、続行する方法と、この問題が決定可能かどうかはわかりません。

4

1 に答える 1

5

前述のように、F <=> Gが閉じた (普遍的に量化された) 式であることを証明するには、F => GとG => Fを証明する必要があります。これら 2 つの公式をそれぞれ証明するには、さまざまな計算を使用できます。[解像度計算] について説明します。

  • 予想を否定すると、F => GはF & -Gになります。
  • CNFに変換します。
  • 解決手順を実行します。
  • 空節を導出すると、元の予想F => Gが証明されたことになります。検索が飽和し、それ以上新しい句を導出できない場合、予想は成立しません。

あなたの条件下では、Fから来るすべての原子式は変数にのみ適用される述語記号になり、 Gからのすべての原子式はスコーレム定数にのみ適用される述語記号になります。したがって、解決手順は、変数を他の変数にマップするか、変数をそれらのスコーレム定数にマップする置換のみを生成します。これは、限定された量の異なるリテラルしか導出できないことを意味するため、解決手順は常に停止します-決定可能になります。

この目的のために自動化されたツールを使用して、すべての作業を行うこともできます。このような問題には、 The E Theorem Proverを使用します。入力言語として、人間が読み書きしやすい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
于 2012-08-11T20:34:21.620 に答える