問題タブ [theorem-proving]

解決定理証明にKowalskiグラフアルゴリズムを使用しようとしています。http://www.doc.ic.ac.uk/~rak/でのアルゴリズムの説明は、 生成される多数の重複句について何をすべきかについては言及していません。それらに対処するためのよく知られたテクニックがあるかどうか疑問に思いますか？

特に、重複する句の生成を単純に抑制することはできません。これは、それらに付随するリンクが関連しているためです。

これまでに生成されたすべての句のセットを追跡する必要があるように思われます。複製が生成されたら、代わりに既存のインスタンスに新しいリンクを追加します。これは、句が名目上削除された場合でも、再生成された場合のために、おそらく維持する必要があります。

異なる句のリテラルは、同一であっても別個のオブジェクトであるため、重複は、オブジェクトの同等性ではなく、テキスト表現の観点から定義する必要があります。

私がここで正しい方向に進んでいるかどうかを誰かが確認できますか？また、このアルゴリズムについて私が見つけた唯一の重要なオンラインリファレンスは上記のリンクでした。他の誰か、またはそれを実装している既存のコードを知っている人はいますか？

のセットAと のセットがありB、それぞれに数値の優先度が関連付けられており、それぞれAが一部またはすべてBの と一致する場合があり、その逆もあり、私のメインループは基本的に次のもので構成されています。

最良の優先順位を取り、AとBを使用して処理をA行いBます。

これを行う最も明白な方法は、ペアの 1 つの優先キューを使用することですが、100,000と 100,000(A,B)がある場合、ペアのセットはメモリに収まりません (そしてディスクが遅すぎます)。ABO(N^2)

別の可能性は、 for each A、 every をループすることBです。ただし、これは、グローバルな優先順位が単独であることを意味しA、両方のコンポーネントの優先順位を考慮する必要があります。

(適用は定理証明であり、上記のオプションはそれぞれペア アルゴリズムと与えられた節アルゴリズムと呼ばれます。それぞれの欠点はわかっていますが、適切な解決策への参照は見つかりませんでした。)

ある種の 2 層優先キューが示されているように見えますが、最悪の場合にO(N^2)メモリや時間を使用せずにこれを行う方法は明確ではありません。O(N^2)

これを行う既知の方法はありますか？

明確化: それぞれは、1 つだけでなく、A対応するすべての で処理する必要がありますB。

数式を入力して操作を実行できるが、数学的に有効な操作のみに制限するツール (GUI が推奨されますが、CLI が機能します) を探しています。また、ツールはセッションを保存し、保存された特定の一連の操作が有効であることを後で証明できる必要があります。

注:証明を生成するシステムを探しているのではなく、手動で指定した手順が有効であることを確認するだけです。

同様の操作にACL2を使用したことがありますが、一部のケースではうまく機能しますが、それ以外の場合は非常に使いにくいです。

この小さなプロジェクトが私のモチベーションです。方程式を解くことができる D テンプレート タイプです。この方程式を考えると：

シンボルのいずれかを不明として設定でき、その式を評価すると、その変数に割り当てられます。これは、式ツリーを型に組み込み、書き換え規則を使用してそれを未知の型に対応できるものに変換することによって機能します。

必要なのは、書き換えルールを検証する方法です。それらは、ある関係が真であり、別の関係も真であるというアサーションをテストすることによって検証できます。

私はコンビネータ論理で定理を証明するいくつかの実験を行っていますが、これは有望に見えますが、つまずきのブロックが 1 つあります。コンビネータ論理では、たとえば I = SKK が真であることが指摘されていますが、これは定理ではありません。を公​​理として追加する必要があります。追加する必要がある公理の完全なリストを知っている人はいますか?

編集: もちろん、I = SKK を手で証明することはできますが、何かが欠けていない限り、それはコンビネータ ロジックと同等のシステム内の定理ではありません。そうは言っても、I を SKK にマクロ展開することはできますが、まだ何か重要なものが欠けています。通常の 1 階論理では矛盾を解決しやすい節 p(X) と ~p(X) の集合を SK に変換し、代入を実行して S と K のすべての呼び出しを評価すると、私のプログラムは以下（Unlambdaのバックティックに ' を使用しています）：

''eq''s''s''s'ks''s''s'ks''s'kk'keq'''s'ks'kk'kk''s'kk'k false 'k true 'k true

私が必要としているのは、部分呼び出し「k」と「」を処理するための適切な一連のルールのようです。これらのルールがどうあるべきかわかりません。この分野で見つけることができるすべての文献は、プログラマーではなく、数学者を対象としています。理解すれば、答えはおそらく非常に簡単だと思います。

ヒルベルト流の体系でステートメント〜（a->〜b）=>aを証明しようとしています。残念ながら、証拠を見つけるための一般的なアルゴリズムを思い付くのは不可能のようですが、私はブルートフォースタイプの戦略を探しています。これを攻撃する方法についてのアイデアは大歓迎です。

私は Agda で単純な補題を証明しようとしていますが、これは正しいと思います。

ベクトルに 2 つ以上の要素がある場合、head次の要素を取得することは、すぐにinit取得することと同じです。head

以下のように定式化しました。

それは私に与えます。

応答として。

(init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs))コンポーネントの読み方がよくわかりません。私の質問は次のとおりだと思います。それは可能ですか、その用語はどのように、そして何を意味しますか。

どうもありがとう。

セキュリティの脆弱性がソフトウェア システムに存在しないことを示すために、自動化された定理証明機能を使用するという話を少し聞いたことがあります。一般に、これを行うのは非常に困難です。

私の質問は、既存または提案されたシステムの脆弱性を見つけるために、同様のツールを使用する作業を行った人はいますか?

Eidt:ソフトウェア システムが安全であることを証明することについて質問しているわけではありません。私は、(理想的には以前は知られていない) 脆弱性 (またはそれらのクラス) を見つけることについて質問しています。ここではブラック ハットのように (しかしそうではありません) 考えています。システムの正式なセマンティクスを説明し、攻撃したいものを説明してから、システムを乗っ取るために使用する必要がある一連のアクションをコンピューターに判断させます。

私はCoqで遊んでいて、ソートされたリストを作成しようとしています。リスト[1,2,3,2,4]を取得して、次のような関数を返す関数が必要Sorted [1,2,3,4]でした。つまり、不良部分を削除しますが、実際にはリスト全体を並べ替えることはありません。

lesseqタイプの関数を定義することから始めようと思ったのですが(m n : nat) -> option (m <= n)、それからパターンマッチングをかなり簡単に行うことができました。多分それは悪い考えです。

私が今抱えている問題の核心はそれです（スニペット、下部の関数全体）

タイプチェックではありません。を期待していると書いてありますoption (m <= n)が、Some (le_n 0)タイプはoption (0 <= 0)です。mその文脈では明らかに両方とnがゼロであるため、私にはわかりませんが、 Coqにそのことを伝える方法がわかりません。

全体の機能は次のとおりです。

おそらく私は自分より進んでいて、これに取り組む前に読み続ける必要があります。

既成のSMTソルバーを使用して、Cコードのシンボリック実行でいくつかの実験を計画しており、どのソルバーを使用するかを考えています。たとえば、SMTコンテストの参加者を見て、オープンソースシステムのみを取り上げ、ビーバー、ブーレクター、CVC3、OpenSMT、サテン、ソノラー、STP、ベリットに絞り込みます。これはまだ長いリストです。

もう少し絞り込んでみると、一部のシステムはビットベクトル演算を処理する機能をアドバタイズしているのに対し、他のシステムは一般的な整数演算を処理する機能のみをアドバタイズしていることに気付きました。原則として、前者はCに対して正しいです。ここで、変数はマシンワードであり、無制限の整数ではありません。実際にはどのくらいの違いがありますか？この種の仕事に一般的な整数システムを使おうとするとどうなりますか？次のシナリオのいずれかが当てはまりますか？

1. ビットベクトルシステムの方が少し効率的ですが、どちらでも問題ありません。

2. 少し調整を加えた一般的な整数システムを使用できます。

3. 一般的な整数システムはsignedintには問題ありませんが（オーバーフローの結果が未定義であるため）、unsignedには間違った答えが返されます。

4. 一般的な整数システムは、マシンワード演算には正しくありません。短いリストを、ビットベクトル演算を提供するシステムのみに減らすことができます。

5. 他に…？

私はできるだけ具体的な質問をしようとしましたが、誰かがリストを絞り込むための他の基準を提案できるなら、それは素晴らしいことです！

リスト内のオブジェクトを検索しようとしていますが、見つかった場合はtrueを返します。それ以外の場合はfalse。

しかし、私が思いついたのは間違っています。いくつかのガイダンスを本当にいただければ幸いです。リストの先頭を関連する要素と比較して要素のリストを検索する関数が必要です。一致しない場合は、リストの残りの部分を関数に再帰的に配置し、リストの先頭を照合して繰り返します。

あなたの指導と援助は大歓迎です。

前もって感謝します