FindEquationalProof

FindEquationalProof[thm,axms]

公理 axms を使って記号定理 thm を方程式によって証明しようとする．

FindEquationalProof[thm,"theory"]

指定の名前の公理理論を使って thm の証明を求めようとする．

詳細とオプション

  • FindEquationalProof[thm,axms]が，公理 axms から定理をTrueに導くことに成功した場合はProofObject式が返される．公理から定理が導けないことが明らかにできた場合はFailureオブジェクトが返される．それ以外の場合は，時間に制約がない限り終了しない場合かもしれない．
  • 公理と定理は，方程式の形で，あるいは一階論理の式の形で与えることができる．一階論理の式は方程式の形に変換される．
  • thm 文と axms 文は以下の任意の論理結合でよい．
  • expr1expr2等価のアサーション
    p[expr1,…]任意の記号述語
    ForAll[vars,stmt]stmt が vars のすべての値について真であるというアサーション
    Exists[vars,stmt]vars の値が stmt が真であるものについて存在するというアサーション
  • expriは，頭部が形式演算子や関数等を表す任意の記号式でよい．
  • 文 stmt は述語の任意の論理結合からなっていてよい．
  • FindEquationalProof[expr1&&expr2&&…,axm1&&axm2&&…]は expr1,expr2,…のそれぞれを別々の仮説として，axm1,axm2,…のそれぞれを別々の公理として扱う．
  • FindEquationalProof[{expr1,expr2,…},{axm1,axm2,…}]はFindEquationalProof[expr1&&expr2&&…,axm1&&axm2&&…]に等しい．
  • FindEquationalProof[thm,"theory"]はFindEquationalProof[thm,AxiomaticTheory["theory"]]に等しい．
  • FindEquationalProof["name","theory"]はAxiomaticTheory["theory","NotableTheorems"]からの名前付き理論の証明を求めようとする．
  • FindEquationalProofには次のオプションがある．
  • TimeConstraint Infinity使用可能な時間
  • FindEquationalProofは，指定された制限時間を超えた場合はFailureオブジェクトを返す．
  • FindEquationalProof[thm,axms]は，クヌース・ベンディックス(Knuth-Bendix)完備化アルゴリズムを使って，定理 thm が公理 axms から得られることを証明する．

例題

すべて開くすべて閉じる

例  (3)

命題論理の基本定理を証明する：

抽象的な証明ネットワークを，ツールチップで中間式を示して表示する：

証明過程の各段階の完全リストをDatasetオブジェクトとして表示する：

全称記号を含む定理を一階論理で証明する：

自然言語の引数をタイプセットする：

簡単な三段論法を証明する：

スコープ  (3)

公理のリストからの初等定理を証明する：

定理を論理積として表現する：

方程式の定理は他からは導出できないことを示す：

存在記号を使った述語論理における三段論法の証明：

オプション  (1)

TimeConstraint  (1)

TimeConstraintt を使って計算時間を t 秒に制限する：

デフォルトで，FindEquationalProofはいつまでも証明を探し続ける：

アプリケーション  (19)

基本論理  (6)

ブール論理で選択した公理を指定する：

ブール論理の定理を証明する：

抽象的な証明ネットワークを表示する：

ブール論理の別の定理を証明する：

同伴証明関数を構築して実行する：

シェファー(Sheffer)論理の公理を指定する：

シェファー論理の定理を証明する：

証明データ集合を表示する：

シェファー論理の別の定理を証明する：

同伴証明関数を構築（し，実行）する：

シェファー論理の第3定理を証明する：

抽象的な証明ネットワークを表示する：

シェファー論理の最終定理を証明する：

抽象的な証明ネットワークを表示する：

ブール論理，ハンティントン(Huntington)論理，ロビンス論理の公理を定義する：

ハンティントン論理の公理がブール論理の公理から得られることを証明する：

ロビンス論理の公理がブール論理の公理から得られることを証明する：

ロビンス論理の公理がハンティントン論理の公理から得られることを証明する：

ブール代数についてのWolframの可能な限り最も短い定理を定義する：

論理演算子Nandの可換性を証明する：

Wolfram公理を使い，補助的な定義を介してAnd，Or，Notの各演算子を導入することで，ブール公理を証明する：

Wolfram公理を使い，補助的な定義を介してOr，Notの両演算子を導入することで，Or-Notブール公理を証明する：

抽象代数  (8)

群論の公理を指定する：

左単位元の存在を証明する：

自然言語の引数をタイプセットする：

群論におけるより高度な定理を証明する：

抽象的な証明ネットワークを表示する：

アーベル群論の公理を指定する：

アーベル群論の定理を証明する：

証明のデータ集合を表示する：

アーベル群論の別の定理を証明する：

抽象的な証明ネットワークを表示する：

半群論，モノイド論，群論の公理を定義する：

どの群も半群であることを証明する：

どの群もモノイドであることを証明する：

アーベル群論と環論の公理を定義する：

どの環もアーベル群であることを証明する：

p を積，e を単位元として使って群論の公理を取る：

四元群をその8つの元の2つから生成する関係を加える：

この群の他の関係を証明する：

場の理論の公理は乗法右逆元の存在を含む：

積は可換なので，上記は左逆元でもある：

積が可換であることを示すことで，左近環の公理から右近環の公理を示す：

LeftTriangleで示される自然に定義された半順序でベキ等半環の公理を構築する：

半順序が反対称であることを証明する：

算術  (1)

プレスバーガー(Presburger)算術の修正（方程式）版について，いくつかの公理を指定する：

プレスバーガー算術における二重否定の定理を証明する：

抽象的な証明ネットワークを表示する：

プレスバーガー算術における加算演算子について，定理を証明する：

証明のデータ集合を表示する：

実解析  (1)

次の公理は，微積分の基本定理，積の規則，微分の線形性を指定する：

この積分を部分公式で証明する：

自然言語による引数をタイプセットする：

ループ理論と普遍代数  (1)

次の公理は，内部自己同形群がアーベル群であるループを表している：

このループのベキ零性の等級が3以下であることを証明する：

証明のデータ集合を表示する：

論理パズル  (2)

ルイス キャロル(Lewis Carroll)に従って赤ん坊はワニを制御できないと結論付ける：

knights（正直者，常に本当のことを言う）とknaves（嘘つき，常に嘘を言う）のパズルの解をチェックする：

特性と関係  (2)

FindEquationalProofが特定の定理についての証明オブジェクエトを返すなら，FullSimplifyはその定理に対してTrueを返す：

FindEquationalProofは公理のリストと公理の論理積を同じものとして扱う：

仮説についても同じことが言える：

考えられる問題  (1)

FindEquationalProofは，デフォルトで，算術演算子を含む定理は証明できない：

乗算の特性を指定することで結果を証明する：

Wolfram Research (2018), FindEquationalProof, Wolfram言語関数， https://reference.wolfram.com/language/ref/FindEquationalProof.html （2020年に更新）.

テキスト

Wolfram Research (2018), FindEquationalProof, Wolfram言語関数， https://reference.wolfram.com/language/ref/FindEquationalProof.html （2020年に更新）.

CMS

Wolfram Language. 2018. "FindEquationalProof." Wolfram Language & System Documentation Center. Wolfram Research. Last Modified 2020. https://reference.wolfram.com/language/ref/FindEquationalProof.html.

APA

Wolfram Language. (2018). FindEquationalProof. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/FindEquationalProof.html

BibTeX

@misc{reference.wolfram_2024_findequationalproof, author="Wolfram Research", title="{FindEquationalProof}", year="2020", howpublished="\url{https://reference.wolfram.com/language/ref/FindEquationalProof.html}", note=[Accessed: 22-November-2024 ]}

BibLaTeX

@online{reference.wolfram_2024_findequationalproof, organization={Wolfram Research}, title={FindEquationalProof}, year={2020}, url={https://reference.wolfram.com/language/ref/FindEquationalProof.html}, note=[Accessed: 22-November-2024 ]}