問題タブ [theorem-proving]

したがって、サブゴールに誤った仮説があります。これは、異なるコンストラクター間の同等性です。サブゴールを終了するにはどうすればよいですか？

誰かがZ3とcoqの違いを教えてくれるかどうか疑問に思っていますか？coqは、ユーザーが証明手順を入力する必要があるという点で証明アシスタントであるように思われますが、Z3にはその要件がありません。しかし、coqにもZ3と同様の自動戦術があるようです。それとも、coqの証明検索機能はZ3ほど強力ではありませんか？

従来、計算ロジックでのほとんどの作業は、SAT（充足可能性）ソルバーを使用する命題論理、または1次定理証明器を使用する1次のいずれかでした。

近年、基本的に命題論理を算術などの理論で補強するSMT（満足度モジュロ理論）ソルバーで多くの進歩が見られました。SRIInternationalのJohnRushbyは、彼らを破壊的技術と呼んでいます。

一階述語論理で処理できるが、SMTでは処理できない問題の最も重要な実際的な例は何ですか？特に、ソフトウェア検証の領域でSMTが処理できない問題はどのようなものでしょうか。

Java（またはJavaバインディングを提供するもの）でのBDD（二分決定図）の実装に関する提案はありますか？このページをオンラインで見つけました：http：//www.mancoosi.org/~abate/avalaible-bdd-librariesですが、古くなっているかどうかはわかりません。それとも、Prologの実装を使用するだけで意味がありますか？

Coq には次の定理がありますTheorem T : exists x:A, P x.。この値を後続の証明で使用できるようにしたいです。IE私は次のようoなことを言いたいです:P ooT

どうすればいいですか？前もって感謝します！

私は修士号の最終試験の準備をしています。これは過去の試験の問題で、本当に混乱しています。どこから始めればよいかわかりません。

私の考えでは、許容できるヒューリスティックは解決ルールであり、解決ルールが許容できることを証明します。そうですか? もしそうなら、解決規則が許容できることを証明するには、どこから始めればよいですか? みんなを助けてくれてありがとう。

定理証明アプリケーションを考えてみましょう。A* アルゴリズムを使用して、最も単純な (最短の) 証明を検索できます。既知の公理と定理が命題論理のホーン節の知識ベースとして表され、証明者が後方連鎖を使用すると仮定します。

(a) 許容できるヒューリスティックを提案する。

(b) 提案されたヒューリスティックが許容できることを証明する

Z3定理証明者を使用して、満足のいく割り当てのセットから均一にサンプリングする方法はありますか? そうでない場合、この機能を備えた Z3 に最も近いシステムはどれですか?

私は COQ を学んでいて、本の演習の 1 つに行き詰まっています。この本には解決策が書かれていないので、どうすればよいかわかりません。最初はやったけど。これらのステートメントを述語ロジックに変換する必要があります。

コード：

.

助けていただけますか？どうもありがとう！

この問題をできるだけ切り分けるために、次のように Coq セッションを開始するとします。

ここからは、常に truef : A -> Bである一意の関数として関数を定義したいと思います。P a (f a)

これどうやってするの？これはできますか？明らかに、私は次のようなものから始めるべきです

...しかし、これらの仮説に関して実際に関数をどのように記述すればよいでしょうか?

私はこれを証明しなければなりません:

これまでのところ、私はやった：

次に、False を証明する必要があります。どうすればいいのかわかりません。これは証明不可能でしょうか？私を正しい方向に向けることができますか？それとも、ここで何か不足していますか?

編集: Ptival さん、大変お世話になりました...質問の間違いに気付き、質問を編集しようとしたときに、誤って削除ボタンを押してしまい、パニックになり、バックスペースを押してしまいました。:(