|
===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。 ・ 定理 ： [ていり] 【名詞】 1. theorem 2. proposition ・ 理 ： [り] 【名詞】 1. reason ・ 自動 ： [じどう] 1. (adj-na,n) automatic 2. self-motion ・ 動 ： [どう] 【名詞】 1. motion 2. change 3. confusion ・ 証 ： [あかし, しょう] (n) 1. proof 2. evidence ・ 証明 ： [しょうめい] 1. (n,vs) proof 2. verification
自動定理証明（、ATP）とは、自動推論(AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。 == 歴史 == === 論理学的背景 === 論理学の起源はアリストテレスまで遡るが、現代的数理論理学は19世紀末から20世紀初頭に発展した。フレーゲの『概念記法』(1879) が完全な命題論理と一階述語論理の基本的なものを導入。同じくフレーゲの『算術の基礎』(1884)でも、形式論理の数学（の一部）を説明している。この流れを受け継いだのがラッセルとホワイトヘッドの『プリンキピア・マテマティカ』で、初版は1910年から1913年に出版され、1927年に第2版が出ている。ラッセルとホワイトヘッドは、公理と形式論理の推論規則からあらゆる数学的真理が導き出せると考え、証明自動化への道を拓いた。1920年、トアルフ・スコーレムはの成果を単純化したレーヴェンハイム-スコーレムの定理をもたらし、1930年にはエルブラン領域とエルブラン解釈により、一階の論理式の充足（不）可能性（および定理の妥当性）を命題論理の充足可能性問題に還元できることが示された。 1929年、Mojżesz Presburger は（加法と等号のある自然数の理論）が決定可能であり、その言語内の任意の文の真偽を判定できるアルゴリズムを示した〔)〕。しかしその直後、クルト・ゲーデルが ''Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I'' (1931) を発表し、十分に強力な公理系はその体系内で証明も反証もできない文を含みうることを示した。1930年代にこの課題を研究したのがアロンゾ・チャーチとアラン・チューリングで、それぞれ独自に等価な計算可能性の定義を与え、決定不能な具体例も示した。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「自動定理証明」の詳細全文を読む 英語版ウィキペディアに対照対訳語「 Automated theorem proving 」があります。 スポンサード リンク
|