theorem-proving

0熱

1答えて

(∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0)をz3で証明したい。否定は：∀i(0≤i<k→a[i]>0)∧a[k]>0∧∃i(0≤i≤k∧¬(a[i]>0))です。まず、私は5にkの値を設定し、一部a[k]>0を無視して、試してみてください。 from z3 import * i = Int('i')` a = Array('a',IntSort(),I

2熱

2答えて

関数の値にネストされた帰納法を使用したFixpointプルーフ

Coqの誘導原理を証明しようとしています。データ構造の定義のために、この原理を2つのネストされた誘導によって表示することが義務付けられています。外部誘導は、Fixpoint構築物を介して行われ、内部誘導は、原理list_indで行われる。問題が発生するのは、内部誘導の誘導引数が関数の結果である、つまりdfs tです。 Iは、dfs tの最初の要素を外側帰納法の仮定を適用できるようにする必要があり

-2熱

1答えて

Z3での「最小化」の仕組み

私はZ3のminimize関数をたくさん使っていますが、私はいくつかのスケーラビリティの問題（最小化する変数の数が増えると）について心配しています。 "最小化"の根底にあるアルゴリズムは何ですか？そして、物事をスピードアップする一般的な方法はありますか？

-4熱

2答えて

実装が不可能な機能を記述することは可能ですか？

私は理論コンピュータサイエンスを勉強していますし、私はこの質問に遭遇：入力と出力としてNを取る関数の例を与えるを（はい、いいえ）この機能を実装することができます何のJavaプログラムが存在しないようにします。どうすればこの問題を解決できますか？私はこれを正しく理解してはいけません。なぜなら、Javaプログラムは常に上記のステートメントから作成できるように思えるからです。

1熱

1答えて

Isabelle/HOLではどのように誘導をIsar/Isarと併用しますか？

以下の例のそれぞれがうまく動作しないのか、より抽象的な誘導が戦術対Isarと相互作用するのかを理解するのは苦労しています。私は最新のIsabelle/HOL（2016-1）で最新のIsabelle/HOL（2016年12月）のプログラミングと検証で4.3に取り組んでいます。 8つのケースがあります：補題は長い（矢印を使用）、証明は構造化（Isar）または非構造化（戦術的）のいずれかです。 theo

3熱

1答えて

Agda：スタックでインストールするときにstd-libを見つけることができません

Agdaファイルをコンパイルしようとしていますが、標準ライブラリを見つけることができません。私は文書hereを見ました。私はそれをインストールするために、スタックを使用しました： > which agda /home/joey/.local/bin/agda そして、私は私のAgdaディレクトリの環境変数を設定しました：正しいファイルが格納されている > echo $AGDA_DIR /

1熱

1答えて

難し私は次のように私の定義のデータ型の1つにプロパティを証明しようとしていますイドリス

で証明を適用する：：私はことを以前に証明事実を使用しようとしていますこれを証明しようとして reverseProof' : (inputBlock : Block iType iSize iInputs) -> (ind : Fin rSize) -> (rInputs : Vect rSize Ty) -> (receiveBlock : Block r

2熱

1答えて

Z3：線形代数を表現する

行列やベクトルを含む式の性質を証明したいと考えています（サイズは大きくなる可能性がありますが、サイズは固定されています）。 Iは、式の結果は、対角行列または三角行列である、またはそれは、正定であることを証明したい例えば ... そのために私は、エンコードよく知られた特性をたいと思いますし、以下のような線形代数からアイデンティティ、： ||x + y|| <= ||x|| + ||y|| (A *

2熱

1答えて

Z3で完全に評価された結果は？

Z3は、しばしば、中間関数の束として定義されたモデルを返します。たとえば、次のようなことがよくあります（私の不適切な構文を許してください）。 (define-const myArray (Array Bool Int) (_ as-array f)) (define-fun f (x Bool) Int (f!10 (k!26 x))) ...などです。私は私のプログラム（ライブラリバイン

1熱

1答えて

セット組み込みからリーンの等価設定へ

セット組み込みとその逆の証明が与えられていると、2つのセットが等しいことを示すことができます。は例えば、私はfollowing statement、およびits converseを証明する方法を知っている： open set universe u variable elem_type : Type u variable A : set elem_type variable B : se