自動定理証明 - ATPとCASのこと
現在の定理証明プログラムは ・論理式を入力すれば，自動的に証明してくれる（ものによっては証明も出力する），いわゆる，prover． 例）otter/prover9 http://www.mcs.anl.gov/research/projects/AR/otter/index.html http://www.cs.unm.edu/~mccune/mace4/ SPASS http://www.spass-prover.org/ そして，Theorema http://www.risc.jku.at/research/theorema/description/ ・証明に用いる定理や規則を対話的に入力する，いわゆる，proof assistant． 例）LCF http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng
不可能性定理：Prologによる２×３のケースの自動証明
Prologによる２×３のケースの不可能性定理の自動証明： Gibbard-Satterthwaiteの定理とArrowの定理 2006.3.8 last revision:2007.11.22 犬童健良 関東学園大学経済学部 はじめに ギッバード＝サタスウェイトの定理（Gibbard(1973), Satterthwaite(1975)）は、 経済学・政策科学・倫理学などの分野における基本定理として知られています。 Kenneth J. Arrow やAmartya Sen によって開拓された社会的選択理論 (Arrow, 1963; Sen, 1982; Arrow et al., 2002)における不可能性定理のひとつです。 ２人以上のメンバーからなる社会に、 ３つ以上の代替案があるとして、人々の選好モデルと社会的選択のルール （社会的選択関数；SCF）が 所定の条件（定義域の非限定
導出原理 - Wikipedia
導出原理（どうしゅつげんり、英: resolution principle）とは、ジョン・アラン・ロビンソン（英語版）により1965年に提案された[1]原理または手法を言う。 導出原理を元とする導出の手法は、その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。 背景[編集] 述語論理式 P が恒真であるかを証明する一般的な手続きは存在しないが、1930年に発表されたエルブランの定理はエルブラン領域の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、¬P が充足不能（恒偽）であれば有限のステップで証明できることを保証している。また、エルブランの論文には単一化アルゴリズムなど他の様々なものが含まれていた[2]。 1950年代以降、計算機上での定理証明の研究が活発になり、ギルモアのアルゴリズム(1960)やデービス・パトナ
エルブランの定理 - Wikipedia
エルブランの定理（英: Herbrand's theorem）は1930年にジャック・エルブランが発表した数理論理学上の基本定理である [1]。 エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。 を節の有限集合とするとき、以下の2つは同値である。 が充足不能 から得られる基礎例（エルブラン基底）の有限集合で充足不能なものが存在 エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。 なお、エルブランの本来の証明は任意の一階述語論理式を
自動定理証明 - Wikipedia
アルゴンヌ国立研究所は1960年代以降2000年代まで、自動定理証明のリーダーだった。 自動定理証明（英: automated theorem proving, ATP）とは、自動推論 (AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。 歴史[編集] 論理学的背景[編集] 論理学の起源はアリストテレスまで遡るが、現代的数理論理学は19世紀末から20世紀初頭に発展した。フレーゲの『概念記法』(1879) が完全な命題論理と一階述語論理の基本的なものを導入[1]。同じくフレーゲの『算術の基礎』(1884)[2]でも、形式論理の数学（の一部）を説明している。この流れを受け継いだのがラッセルとホワイトヘッドの『プリンキピア・マテマティカ』で
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
