2

私は Prover9/Mace4 を通していくつかの格子証明を実行しています。私は格子結合操作の非標準の公理化を使用していますが、結合が交換可能、結合的、冪等であることはすぐにはわかりません。(私は Prover9 にそれが正しいことを証明してもらうことができます -- 最終的に。)

Prover9 がこれらのプロパティを探して、検索を高速化することを知っています。これらのプロパティを追加入力セクションに入れてみました (GUI バージョン 0.5 を実行しています)。

formulas(hints).
x v y = y v x.
% etc
end_of_list.

Q1: ヒントを見てもらう方法はこれですか？

Q2: 証明/ヒントとコツを高速化するためのヘルプを探すのに適した場所はありますか? (これを機能させることができれば、ヒントを提供したい演算子が他にもあります。)

参考までに、私の公理は次のとおりです（プリミティブ操作が1つだけの双格子）：

x ^ y = y ^ x.                % lattice meet
x ^ x = x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.              % standard absorption for join
x ^ z = x & y ^ z = y <-> z ^ (x v y) = (x v y).
                              % non-standard absorption

（DougSの回答が投稿された後に編集してください。）

わお！ありがとうございました。桁違いのスピードアップ。

もしよろしければ、いくつかの後続のqがあります...

Q3: 生成されたヒントには、最初の公理と目標がすべて含まれているように見えます。（おそらく、すべてのヒントを必要としないというあなたのコメントです。公理を削除すると証明が速くなることを確かに経験しました。）

Q4: (結果として) 公理によって正当化されないヒントを追加するとどうなりますか? それらは無視されますか？

Q5: 公理に反するヒントを追加するとどうなりますか? (いくつかの試行から、これにより Prover9 が誤って推論することはありません。)

Q6: 証明 (試行) がタイムアウトした場合、これまでに推論された数式を取得し、次の試行を高速化するためのヒントとして再利用する方法はありますか? (Q3 と Q4 に関して私が見たものにもかかわらず、これはある種の誤謬を引きずり込むだろうと私は感じています。)

4

2 に答える 2

2

Q1: はい、ヒントとして機能するはずです。しかし、それをよりよくテストするために、あなたが持っている証拠を取り、「再フォーマット」オプションを使用して「ヒント」部分をチェックしてください。次に、それらのヒントをすべてコピーして、「式 (ヒント)」に貼り付けます。リスト。（まあ、必ずしもすべてが必要というわけではありません...そして、それらのいくつかだけを使用すると、存在する場合はより短い証明になる可能性がありますが、余談です）。それからもう一度証明を実行し、ヒント付きの命題計算での私の証明のように実行されれば、「瞬時に」証明が得られます。

念のため...「追加入力」タブをクリックして、そこにヒントリストを配置する必要があります。

Q2: 戦略については、Prover9 のマニュアルに、重み付け、ヒント、セマンティック ガイダンスに関する有用な情報があります (セマンティック ガイダンスは試していません)。Bob Veroff のページも参照してください(彼の作業の一部は OTTER で行われていますが、プログラムは似ています)。ラリー・ウォスのノートブックやウォス博士の出版物などの有用な情報も存在しますが、ウォスの最近の作業はすべて OTTER を使用して行われています (繰り返しますが、プログラムは似ています)。

于 2014-06-13T03:30:06.677 に答える
2

Q3: はい、公理と目標がヒントとして含まれていることを期待する必要があります。どちらも有用な役割を果たすことができます。ヒントとして「$F」のようなものが表示される可能性があり、私にはあまり追加されないようであり、ヒントも最初に特定のパスに誘導され、短い証明を見つけるのがより困難または容易になる可能性があることを意味しました. ただし、より迅速な証明が必要な場合は、提案されたヒントをすべて使用することをお勧めします。

Q4: ヒントは、公理から演繹できるものである必要はありません。

Q5: 確かに、ヒントは公理と矛盾する可能性があります。

マニュアルには、「派生句がヒントを包含する場合、派生句はヒントに一致します。

...

つまり、hints_part パラメーターのデフォルト値は、ヒントが利用可能な場合はいつでも、ヒントに一致する (最も軽いものを最初に) 句を選択するように指示します。"

「C の変数が D の副次節になるような方法でインスタンス化できる場合、C 節は D を包含します。C が D を包含する場合、D は C よりも弱いか同等であるため、破棄できます。包含条項の保持を必要とするいくつかの証明手順。)」

だから、あなたが入れたとしましょう

 1. x ^((y^z) V v)=x V y as a hint.

次に、Prover9が生成した場合

 2. x ^ ((x^x) V v)=x V x

x ^ ((x^x) V v)=x V x は、ヒントと一致するため、使用可能な場合は常に選択されます。

「副節」がどのように定義されるのか正確にはわからないため、この説明は完全ではありません。

それでも、元の公理と Prover9 が式を生成するために使用する手順を使用して式を生成する代わりに、ヒントに一致する式が式を生成するためのリストの先頭に置かれます。これはプログラムの速度を上げることができますが、他のいくつかの問題について読んだことから、ヒント、重み付け、およびその他の戦略がなければ、多くの難しい問題は基本的に自動的に証明されなかったようです. .

Q6: どの数式を参照しているのかわかりません。もちろん、Prover9 では、[出力を表示] をクリックして、生成された多数の数式を確認できます。また、追加の目標として役立つと思われる補題を設定し、Prooftrans を使用してこれらの補題からヒントを生成し、次の実行でヒントとして使用することもできます。または、これらの補題の証明の手順を次の実行のヒントとして使用することもできます。これらの証明のステップをヒントとして使用する場合、または Prooftrans によって提案されたヒントを使用する場合、推論に関して誤りはありません。ヒントは実際には初期セットに仮定を追加しないためです。ヒント メカニズムは、少なくとも私の大雑把な理解によれば、ヒントに 1 回一致する句を使用するように検索手順を変更することによって機能します。ヒントに一致するものがあります (つまり、プログラムはヒントに一致するものを推測する必要があり、それからヒントに一致するものを使用することができます)。

于 2014-06-16T01:57:57.240 に答える