問題タブ [isabelle]

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

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

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

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

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

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

という名前の理論で独自のリスト型を定義したいのですがList、その名前の理論は既に存在します。より軽量な理論はありMainますか？

Isabelle でケース分析を適用するにはどうすればよいですか? apply (induct x)（誘導に使用される）に似たものを探していました。

場合分けや帰納法で生成される変数に自分の名前を付けることはできますか?

Isabelle の一連の数値 (nat) で最大の要素を見つけるにはどうすればよいですか。max 関数は、最大 2 つの要素を取るように定義されているため、機能しません。reduce like 関数を使用して実装する方法については考えていますが、セットからランダムな要素を 1 つ選択する方法がわかりません。

質問

Isabelle / HOLベリファイアのコアアルゴリズムは何ですか？

スキームメタサーキュラーエバリュエーターのレベルで何かを探しています。

明確化

私は検証者にのみ興味があり、自動定理証明の戦略には興味がありません。

コンテクスト

簡単な証明検証ツールを最初から実装したい（本番環境ではなく、純粋に教育上の理由で）。

Isabelle/HOLのコアベリファイアアルゴリズムを理解したい。自動定理証明に使用される戦略/コードは気にしません。

コアのVerifierアルゴリズムは非常に単純（かつエレガント）であると思われます。しかし、私はそれを見つけることができません。

ありがとう！

Isabelleで補題を述べるとき、私はしばしば とタイプnitpickします。次にsledgehammer、証明を自動的に見つけようと入力します。

私は疑問に思います: NitpickとSledgehammerを呼び出して、同時に実行することは可能ですか? Sledgehammerはすでに私の補題を多数の自動証明者に送っているので、それらの証明者の 1 つは実際にNitpickのような反例発見者ではないでしょうか?

Isabelle 理論ファイルでは、次のような単純な 1 行の戦術を書くことができます。

しかし、証明を自動化し、ML オブジェクトを生成するために ML コードを書き始めるとtactic、これらのワンライナーはかなり冗長になります。

Isabelle/ML レベルで単純な 1 行の戦術を記述する簡単な方法はありますか?

たとえば、反引用のようなもの: @{tactic "clarsimp simp: split_def split: prod.splits"}type の関数を生成するcontext -> tacticことは理想的な解決策です。

AFPエントリDijkstra's Shortest Path Algorithmについては、証明の概要と証明文書の両方が存在しませんでした *。残念ながら、IsaMakefileこれらのドキュメントをローカルでビルドするためのいずれかが見つかりませんでした。それらの書類を入手する最良の方法は何ですか?

別の質問は、Dijkstra.thy他の多くの理論に依存しているため、すべてをより速くロードする方法はありますか?

*)現在は修正されています。

私fooはそのstring型で機能する関数を持っています。export_code foo in Scala file -非常に醜いScalaコードを入手したとき。

このように見える非常に長いリストが作成されます