問題タブ [theorem]

プログラムで、定義から二項定理を数えなければならない解決策（エラーの修正）を見つけようとしています。まず、" factorial " - "silnia" の定義を作成しました。

1) アルゴリズムは、定義の SN1 (n,k) の値を決定します。(ニュートン関数)

2) アルゴリズムは、式によって再帰的に SN3 (n,k) の値を決定します。( newton_rek関数)。

入力: ファイル名: In0101.txt

OUTPUT: ファイル名: Out0101.txt このファイルには、数式から計算された値を保存したいと思います。

例: In0101.txt

Out0101.txt

そして、私が修正できないエラーがあります。誰でもこれで私を助けることができますか?

私のコード:

Coqで定理を証明しようとしていますが、発生した問題を解決できません。私は解決しようとしています：

私はCoqを初めて使用するので、それが実際に何を意味するのかわかりません。私はインターネットでいくつかの調査をしましたが、解決策を見つけることができませんでした。この問題が何から来ているのか誰かが知っていますか？

私は非常に単純なOTTERの入力ファイルを書いています：

私は検索のためにこの出力を取得します：

なぜOTTERは推測しないのCauses($c2,$c1)ですか？

編集：角かっこをから削除しましたが、[Nipah(x) & Encephalitis(x)]機能しました。なぜこれが重要なのですか？

誰かがいくつかの質問で私を助けてくれたら本当にありがたいです.

次の再帰関数定義のそれぞれについて、マスター定理を使用して漸近的な成長順序 (つまり、Big-Tetha) を決定します。マスター定理が特定のケースに当てはまらないと思われる場合は、その理由を適切に説明してください。そのような場合でも、実行時間のある程度妥当な上限 (つまり Big-O) を提供できますか? 基本ケースはすべて定数であると想定されることに注意してください。

(a) T (n) = T(n/2) + 2^n

(b) T (n) = 4T(n/2) +(n^1.5) − 1

(c) T (n) = T (n/3) + 100

(d) T(n) = 125T(n/5) + n^3/logn

(e) T (n) = 2T(n/7) + log n + √n

これに関してオンラインでいくつかのことを読んだだけで、この質問に答えるのに十分な理解を得ることができません. テストのために勉強しようとしていますが、何も得られません!

どうもありがとう！

ソフトウェア検証モジュールでは、真理値表から自然推論に移行しました。真理値表は非常に基本的なものに見えましたが、現在は coq の定理証明器を使用して、より複雑なステートメントを証明しています。私を混乱させているのは、「証明されているか証明されていない」タイプの答えになる方法です。真理値表を使用すると、入力に基づいて真または偽のタイプの結果が得られる場合、これは自然な演繹を使用して調べることを意味しますか?トートロジーの場合、または完全に何かが欠けていますか?

Eclipse IDE 内でZ3 ( http://z3.codeplex.com/ ) を使用しようとしています。PyDev をインストールし、Z3 のコンパイル済み Windows バイナリをダウンロードしました。また、「bin」サブディレクトリを環境変数 PYTHONPATH および PATH に追加しました。

この非常に単純な例では、

Eclipse によると、Real e Solver は未​​定義の変数です。このコードを実行すると、次のエラー メッセージが表示されました。

「ImportError: ...\bin\z3.pyc の不正なマジック ナンバー」

これは、インタープリターとは異なるバージョンの python (通常はそれ以降) の問題のようです (参照: What's the bad magic number error? )。

何か助けはありますか？コンパイル済みの Windows バイナリを使用するのではなく、Z3Py をコンパイルしてインストールする必要がありますか?

ありがとう。

私はこのレマを証明しようとしています

しかし、別の関数である reverse-helper が目標に到達し続けており、それを取り除く方法がわかりません。ガイダンスや提案はありますか？

この講義の「演習として残した」補題に行き詰まっています。こんなふうになります：

even次のように定義された帰納的述語はどこにありますか。

助けてください？私はいつも(S (S p) = 2または似たようなものになります。

編集

私が使用したいくつかの補題と戦術 (完全な証明ではありません):