ブラウザよりも高速アクセス！
84 関係: 原始再帰関数、型理論、健全性、妥当性、定理、完全性、導出原理、帰納的可算集合、一階述語論理、人工知能、二分決定図、形式的検証、ミュンヘン工科大学、マンチェスター大学、マックス・プランク研究所、マサチューセッツ工科大学出版局、チャルマース工科大学、ハーバート・サイモン、バートランド・ラッセル、モーダスポネンス、モデル検査、ユニフィケーション、レーヴェンハイム–スコーレムの定理、トアルフ・スコーレム、プリンキピア・マテマティカ、プリンストン高等研究所、プログラム (コンピュータ)、ヒューリスティクス、フランス国立科学研究センター、命題論理、アラン・チューリング、アリストテレス、アルフレッド・ノース・ホワイトヘッド、アルゴンヌ国立研究所、アレン・ニューウェル、アロンゾ・チャーチ、アドバンスト・マイクロ・デバイセズ、インテル、ウプサラ大学、エルブランの定理、エルゼビア、エディンバラ大学、カールスルーエ工科大学、ギルモアのアルゴリズム、クリフ・ショー、クルト・ゲーデル、ケンブリッジ大学、ゲーデルの完全性定理、ゲーデルの不完全性定理、ゴットロープ・フレーゲ、...、シュプリンガー・サイエンス・アンド・ビジネス・メディア、ジャック・エルブラン、スタンフォード大学、タブローの方法、充足可能性問題、四目並べ、四色定理、Co-NP、Cycプロジェクト、第二次世界大戦、算術の基礎、DPLLアルゴリズム、選言標準形、項書き換え、証明、高階述語論理、論理学、論理プログラミング、自動推論、自然数、集積回路設計、FPU、General Problem Solver、GNU General Public License、Java Web Start、Logic Theorist、Pentium FDIV バグ、S&P グローバル、SRIインターナショナル、概念記法、決定可能性、数学的帰納法、数式処理システム、数理論理学。 インデックスを展開 (34 もっと) »
原始再帰関数
原始再帰関数（げんしさいきかんすう、）とは、原始再帰と合成で定義される関数であり、再帰関数（計算可能関数）の部分集合である。原始帰納的関数とも。 再帰理論において原始再帰関数は、計算可能性の完全形式化のための重要な要素となる関数のクラスの1つである。このような関数は証明論においても重要である。 数論が扱う関数の多くや、実数を値とする関数の近似は原始再帰的であり、加法、除法、階乗、指数、n 番目の素数を求める関数などがある (Brainerd and Landweber, 1974年)。実際、原始再帰的でない関数を考案するのは難しいが、いくつかの例が知られている（限界の節を参照）。 計算複雑性理論では、原始再帰関数の集合をPRと呼ぶ。 原始再帰関数のクラスはwhileプログラムでwhileループを使用せずに計算できる（すなわちloopプログラムで計算可能な）関数のクラスと一致する。原始再帰関数のクラスはグジェゴルチク階層と呼ばれる階層に分類される。.
新しい！!: 自動定理証明と原始再帰関数 · 続きを見る »
型理論
型理論（かたりろん、Type theory）は、数理論理学の一分野であり、「型」の階層を構築し、それぞれの型に数学的（あるいはそれ以外の）実体を割り当てるものである。階型理論（かいけいりろん、Theory of Types）とも。ある型のオブジェクトはその前提となる型のオブジェクトから構築される。この場合の「型」とは形而上的な意味での「型」である。バートランド・ラッセルは、彼が発見したラッセルのパラドックスにより素朴集合論の問題が明らかにされたことを受けて、型理論を構築した。型理論の詳細はホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』にある。 型理論は、プログラミング言語の理論における型システムのベースにもなっている。「型システム」と「型理論」の語はほぼ同義として扱われることもあるが、ここでは、この記事では数理論理学の範囲を説明し、プログラミング言語の理論については型システムの記事で説明する。.
新しい！!: 自動定理証明と型理論 · 続きを見る »
健全性
健全性（けんぜんせい、Soundness）は、論証が次の属性を持つことと同値である。.
新しい！!: 自動定理証明と健全性 · 続きを見る »
妥当性
妥当性（Validity）は、演繹的論証が持つ論理的特性であるが、一般に任意の文に対して使われる（ここでいう文とは、真か偽かという真理値を持つものをいう）。ここでは、論証を文の集まりとし、そのうちの1つの文が結論で残りは前提であるとする。前提とは、結論が（おそらく）真であると示す根拠である。 論証の結論が「確かに」真であるとされている場合、その論証は演繹的である。結論が「おそらく」真であるとされている論証は帰納的であると言われる。ある論証が妥当であるとは、結論が正しく前提から導き出されることを意味する。すなわち、妥当な演繹的論証であれば、真の前提から偽の結論が導き出されることはあり得ない。（一方、前提に偽がある場合には、真・偽どちらの結論も導き出されうる。） 次のような定義が一般的である。.
新しい！!: 自動定理証明と妥当性 · 続きを見る »
定理
定理（ていり、theorem）とは、数理論理学および数学において、証明された真なる命題をいう。 文脈によっては公理も定理に含む。また、数学においては論説における役割等から、補題（ほだい、lemma）あるいは補助定理（ほじょていり、helping theorem）、系（けい、corollary）、命題（めいだい、proposition）などとも呼ばれることがある。ここでの「命題」と冒頭文に言う命題とは意味が異なることに注意。 一般的に定理は、まずいくつかの条件を列挙し、次にその下で成り立つ結論を述べるという形をしている。例えば、次は代数学の基本定理の述べ方の1つである。 ある一定の条件（公理系）下で定理を述べそれを証明すること、というのが数学という分野の中心的な研究の形態である。 数学の多くの分野には、各々「基本定理」という名で呼ばれる中心的な定理が存在している。なお定理という名称と証明という手続きは、数学のみならず、物理や工学においても使用される。.
完全性
数理論理学における完全性（かんぜんせい、completeness）には二つの意味がある。.
新しい！!: 自動定理証明と完全性 · 続きを見る »
導出原理
導出原理（どうしゅつげんり、resolution principle）とは、により1965年に提案されたJ.
新しい！!: 自動定理証明と導出原理 · 続きを見る »
帰納的可算集合
帰納的可算集合（きのうてきかさんしゅうごう、Recursively enumerable set）は、計算理論または再帰理論におけるある種の集合に付与された名前。自然数の集合 S について以下が成り立つ場合、その集合を指して帰納的可算、計算可枚挙、半決定可能、証明可能、チューリング-認識可能などと称する。.
新しい！!: 自動定理証明と帰納的可算集合 · 続きを見る »
一階述語論理
一階述語論理（いっかいじゅつごろんり、first-order predicate logic）とは、個体の量化のみを許す述語論理 (predicate logic) である。述語論理とは、数理論理学における論理の数学的モデルの一つであり、命題論理を拡張したものである。個体の量化に加えて述語や関数の量化を許す述語論理を二階述語論理（にかいじゅつごろんり、second-order predicate logic）と呼ぶ。それにさらなる一般化を加えた述語論理を高階述語論理（こうかいじゅつごろんり、higher-order predicate logic）という。本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細は「二階述語論理」「高階述語論理」を参照。.
新しい！!: 自動定理証明と一階述語論理 · 続きを見る »
人工知能
250px 人工知能（じんこうちのう、artificial intelligence、AI）とは、「計算機（コンピュータ）による知的な情報処理システムの設計や実現に関する研究分野」を指す。.
新しい！!: 自動定理証明と人工知能 · 続きを見る »
二分決定図
二分決定図（にぶんけっていず、Binary Decision Diagram、BDD）とは、ブール関数を表現するのに使われるデータ構造である。二分決定グラフあるいは（基本的には二分木のような構造であることから）二分決定木と呼ぶこともある。.
新しい！!: 自動定理証明と二分決定図 · 続きを見る »
形式的検証
形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。.
新しい！!: 自動定理証明と形式的検証 · 続きを見る »
ミュンヘン工科大学
ミュンヘン工科大学メインキャンパス 上空から見たミュンヘン工科大学（こげ茶色の建物のあるエリアがキャンパス） ミュンヘンキャンパス内にあるすり鉢状の巨大円形講義室。あだ名はアウディマックス。 数学ならびにコンピュータサイエンス学科の校舎内にある巨大滑り台 ガーヒングキャンパス内にある機械工学部 1900年に印刷された同大学のリトグラフ版画 ミュンヘン工科大学（ミュンヘンこうかだいがく、Technische Universität München, 略称：TUM）は、ドイツのミュンヘンにある大学の一つ。.
新しい！!: 自動定理証明とミュンヘン工科大学 · 続きを見る »
マンチェスター大学
マンチェスター大学（The University of Manchester）は、イギリス、マンチェスターにある国立大学で、イングランドで最初の都市大学の一つである。2004年10月、一般にマンチェスター大学と呼ばれたマンチェスター・ビクトリア大学（Victoria University of Manchester）にマンチェスター工科大学（UMIST：University of Manchester Institute of Science and Technology）が再統合され、現在のマンチェスター大学（The University of Manchester）が誕生した。ラッセル・グループ（イギリスの大規模研究型大学群）に加盟している。 20世紀の発明に数多く貢献し、現在までに25人もの卒業生、研究者、教授らがノーベル賞を受賞している、英国が誇る名門国立大学である。受賞者数はケンブリッジ大学、オックスフォード大学に次いで英国第3位である。4名の受賞者が現役で教鞭をとっており、その数は英国最多である。 世界初のコンピューターは、1948年にマンチェスター大学で生まれた。 全国就職誌レポート（2012年）によると、英国ベスト100優良企業がイギリスで最も採用ターゲットとする名門大学となっている。また、英国GTI media社が全国7000以上の高等学校の受験生（2010年～2013年）に実施したアンケートでは、イギリスで最も行きたい大学として、ケンブリッジ大学、オックスフォード大学に次いで英国第３位であった。 エレクトロニクスの分野で世界を牽引する働きをしており、特にウェアラブル端末やスマートテキスタイルズ等の新領域での研究が盛んである。また、これらを応用した産業界との提携も幅広く、多数の日本企業も含む多国籍企業との産業共同研究を推進している。.
新しい！!: 自動定理証明とマンチェスター大学 · 続きを見る »
マックス・プランク研究所
マックス・プランク研究所（マックス・プランクけんきゅうしょ）は、マックス・プランク学術振興協会（e.（マックス‐プランク‐ゲゼルシャフト・ツア・フェルデルング・デア・ヴィッセンシャフテン・エーファオ）、略称：MPG（エムペーゲー））が運営する、ドイツを代表する学術研究機関の日本語における総称である。MPGが運営する各研究機関は、ドイツ語では「Max-Planck-Institut für ○○」（○○は研究分野）のように名づけられており、日本語では「マックス・プランク○○研究所」と訳している。MPGが運営する研究機関は、2006年5月現在で78に上る。.
新しい！!: 自動定理証明とマックス・プランク研究所 · 続きを見る »
マサチューセッツ工科大学出版局
マサチューセッツ工科大学出版局（MIT Press）は、マサチューセッツ工科大学 (MIT) 系列の大学出版局である。.
新しい！!: 自動定理証明とマサチューセッツ工科大学出版局 · 続きを見る »
チャルマース工科大学
ヨーロッパ指折りのエリート名門工科大学の1つとされ、スウェーデンに於ける大学ランキングではほぼ1位を独占し続けている。特に材料工学と建築工学に関しては世界屈指の研究を誇っている。.
新しい！!: 自動定理証明とチャルマース工科大学 · 続きを見る »
ハーバート・サイモン
ハーバート・アレクサンダー・サイモン（Herbert Alexander Simon、1916年6月15日 - 2001年2月9日）は、アメリカ合衆国の政治学者・認知心理学者・経営学者・情報科学者である。心理学、人工知能、経営学、組織論、言語学、社会学、政治学、経済学、システム科学などに影響を与えた。大組織の経営行動と意思決定に関する生涯にわたる研究で、1978年にノーベル経済学賞を受賞した。.
新しい！!: 自動定理証明とハーバート・サイモン · 続きを見る »
バートランド・ラッセル
3代ラッセル伯爵、バートランド・アーサー・ウィリアム・ラッセル（Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS、1872年5月18日 - 1970年2月2日）は、イギリスの哲学者、論理学者、数学者であり、社会批評家、政治活動家である。ラッセル伯爵家の貴族であり、イギリスの首相を2度務めた初代ラッセル伯ジョン・ラッセルは祖父にあたる。名付け親は同じくイギリスの哲学者ジョン・スチュアート・ミル。ミルはラッセル誕生の翌年に死去したが、その著作はラッセルの生涯に大きな影響を与えた。生涯に4度結婚し、最後の結婚は80歳のときであった。1950年にノーベル文学賞を受賞している。.
新しい！!: 自動定理証明とバートランド・ラッセル · 続きを見る »
モーダスポネンス
モーダスポネンス（ラテン語: 、MP）とは、論理学における妥当で単純な「論証」である。ラテン語で「肯定によって肯定する様式」の意。前件肯定 または分離規則 とも呼ぶ。.
新しい！!: 自動定理証明とモーダスポネンス · 続きを見る »
モデル検査
モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。.
新しい！!: 自動定理証明とモデル検査 · 続きを見る »
ユニフィケーション
ユニフィケーション（unification）は数理論理学や計算機科学の用語であり、問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つのが同一または同等であることを示すを求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。 なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。 主なユニフィケーションは数種類ある。等号を持たない論理（理論）において、2つの項が同一であることを示すためのユニフィケーションは統語論的ユニフィケーションと呼ばれる。空でない等号を持つ論理（理論）で2つの項の同等性を示す場合、それを意味論的ユニフィケーションと呼ぶ。置換は順序集合として順序付けられるので、ユニフィケーションは束における結びを求める手続きとして解釈できる。 ユニフィケーションを初めて形式的に研究したのはで、一階述語論理の導出手続きを構築する際に一階のユニフィケーションを基盤として使い、組合せ爆発の原因の1つ（項を例化したものの探索）を排除することで自動推論技術への大きな一歩とした。.
新しい！!: 自動定理証明とユニフィケーション · 続きを見る »
レーヴェンハイム–スコーレムの定理
レーヴェンハイム–スコーレムの定理（Löwenheim–Skolem theorem）とは、可算な一階の理論が無限モデルを持つとき、全ての無限濃度 κ について大きさ κ のモデルを持つ、という数理論理学の定理である。そこから、一階の理論はその無限モデルの濃度を制御できない、そして無限モデルを持つ一階の理論は同型の違いを除いてちょうど1つのモデルを持つようなことはない、という結論が得られる。.
新しい！!: 自動定理証明とレーヴェンハイム–スコーレムの定理 · 続きを見る »
トアルフ・スコーレム
トアルフ・スコーレム（Albert Thoralf Skolem、1887年5月23日 - 1963年3月23日）は、ノルウェーの数学者。オスロ大学で代数学や自然数論を講義した。 数理論理学、数学基礎論で重要な発見をしている。また、不定方程式論においても、いくつかの定理を発見している。主な業績として、数理論理学では.
新しい！!: 自動定理証明とトアルフ・スコーレム · 続きを見る »
プリンキピア・マテマティカ
短縮版『プリンキピア・マテマティカ 56節まで』の表紙 『プリンキピア・マテマティカ』(Principia Mathematica:数学原理)は、アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルによって書かれ、1910年から1913年に出版された、数学の基礎に関する全3巻からなる著作である。それは、記号論理学において、明示された公理の一組と推論規則から数学的真理すべてを得る試みである。『プリンキピア』のための主なインスピレーションと動機の1つは論理学に関するフレーゲの初期の仕事で、それがパラドックスをもたらすことをラッセルが発見したのである。 プリンキピアは、数学論理と哲学においてアリストテレスの『オルガノン』以来もっとも重要で独創的な仕事の一つと、広く専門家に考えられている。 モダン・ライブラリーは、この本を20世紀のノンフィクション書籍上位100のリスト(Modern Library 100 Best Nonfiction)の23位に位置づけた。.
新しい！!: 自動定理証明とプリンキピア・マテマティカ · 続きを見る »
プリンストン高等研究所
プリンストン高等研究所（プリンストンこうとうけんきゅうじょ、Institute for Advanced Study）は、アメリカ合衆国ニュージャージー州プリンストン市にある研究所。自然科学、数学、社会科学、歴史学の四部門を持ち、世界でももっとも優れた学術研究機関の一つとされる。 中核となるのは27名の教授陣。いずれも最高レベルの研究者であるが、特に物理学と数学の研究が有名である。なお「教授」とはいうものの、原則として授業負担はなく、各自の研究を進めることに加え、毎年世界各地から招聘される約190名の研究者を選抜することが主な職務である。 正式名称は「高等研究所」(Institute for Advanced Study)だが、類似の名称の研究所は内外に数多くあるため、日本では「プリンストン高等研究所」と呼ばれることが多い。プリンストン大学とは直接の関係はないが、同大学など近隣の大学とは密接な協力関係にあり、特にプリンストン大学は高等研究所の草創期に、研究者に対しオフィスを提供するなどしていた。.
新しい！!: 自動定理証明とプリンストン高等研究所 · 続きを見る »
プログラム (コンピュータ)
ンピュータプログラム（英：computer programs）とは、コンピュータに対する命令（処理）を記述したものである。コンピュータが機能を実現するためには、CPUで実行するプログラムの命令が必要である。 コンピュータが、高度な処理を人間の手によらず遂行できているように見える場合でも、コンピュータは設計者の意図であるプログラムに従い、忠実に処理を行っている。実際には、外部からの割り込み、ノイズなどにより、設計者の意図しない動作をすることがある。また設計者が、外部からの割り込みの種類を網羅的に確認していない場合もある。.
新しい！!: 自動定理証明とプログラム (コンピュータ) · 続きを見る »
ヒューリスティクス
ヒューリスティック（heuristic, Heuristik）とは、必ず正しい答えを導けるわけではないが、ある程度のレベルで正解に近い解を得ることができる方法である。ヒューリスティックスでは、答えの精度が保証されない代わりに、回答に至るまでの時間が少ないという特徴がある。主に計算機科学と心理学の分野で使用される言葉であり、どちらの分野での用法も根本的な意味は同じであるが、指示対象が異なる。すなわち、計算機科学ではプログラミングの方法を指すが、心理学では人間の思考方法を指すものとして使われる。なお、論理学では仮説形成法と呼ばれている。.
新しい！!: 自動定理証明とヒューリスティクス · 続きを見る »
フランス国立科学研究センター
フランス国立科学研究センター（フランスこくりつかがくけんきゅうセンター、仏：Centre national de la recherche scientifique 、略してCNRS）は、1939年10月19日設立のフランス最大の政府基礎研究機関である。常勤スタッフ26,080人（うち研究者11,664人、技術者14,416人、その他事務局員）と非常勤スタッフ4,000人を擁する。2006年の予算は27億3,800万ユーロであった。.
新しい！!: 自動定理証明とフランス国立科学研究センター · 続きを見る »
命題論理
命題論理（propositional logic）とは、数理論理学（記号論理学）の基礎的な一部門であり、命題全体を1つの記号に置き換えて単純化し、論理演算を表す記号（論理記号・論理演算子）を用いて、その命題（記号）間の結合パターンを表現・研究・把握することを目的とした分野のこと。ブール論理はブール代数で形式化され2値の意味論を与えられた命題論理とみることができる。 命題を1つの記号で大まかに置き換える命題論理に対して、命題の述語（P）と主語（S）を、関数のF(x)のように別記号で表現し、更に量化子で主語（S）の数・量・範囲もいくらか表現し分けることを可能にした、すなわちより詳細に命題の内部構造を表現できるようにしたものを、述語論理と呼ぶ。.
新しい！!: 自動定理証明と命題論理 · 続きを見る »
アラン・チューリング
アラン・マシスン・チューリング（Alan Mathieson Turing、〔テュァリング〕, 1912年6月23日 - 1954年6月7日）はイギリスの数学者、論理学者、暗号解読者、コンピュータ科学者。.
新しい！!: 自動定理証明とアラン・チューリング · 続きを見る »
アリストテレス
アリストテレス（アリストテレース、Ἀριστοτέλης - 、Aristotelēs、前384年 - 前322年3月7日）は、古代ギリシアの哲学者である。 プラトンの弟子であり、ソクラテス、プラトンとともに、しばしば「西洋」最大の哲学者の一人とされ、その多岐にわたる自然研究の業績から「万学の祖」とも呼ばれる。特に動物に関する体系的な研究は古代世界では東西に類を見ない。イスラーム哲学や中世スコラ学、さらには近代哲学・論理学に多大な影響を与えた。また、マケドニア王アレクサンドロス3世（通称アレクサンドロス大王）の家庭教師であったことでも知られる。 アリストテレスは、人間の本性が「知を愛する」ことにあると考えた。ギリシャ語ではこれをフィロソフィア（）と呼ぶ。フィロは「愛する」、ソフィアは「知」を意味する。この言葉がヨーロッパの各国の言語で「哲学」を意味する言葉の語源となった。著作集は日本語版で17巻に及ぶが、内訳は形而上学、倫理学、論理学といった哲学関係のほか、政治学、宇宙論、天体学、自然学（物理学）、気象学、博物誌学的なものから分析的なもの、その他、生物学、詩学、演劇学、および現在でいう心理学なども含まれており多岐にわたる。アリストテレスはこれらをすべてフィロソフィアと呼んでいた。アリストテレスのいう「哲学」とは知的欲求を満たす知的行為そのものと、その行為の結果全体であり、現在の学問のほとんどが彼の「哲学」の範疇に含まれている立花隆『脳を究める』（2001年3月1日 朝日文庫）。 名前の由来はギリシア語の aristos （最高の）と telos （目的）から 。.
新しい！!: 自動定理証明とアリストテレス · 続きを見る »
アルフレッド・ノース・ホワイトヘッド
アルフレッド・ノース・ホワイトヘッド （Alfred North Whitehead、1861年2月15日 - 1947年12月30日）は、イギリスの数学者、哲学者である。論理学、科学哲学、数学、高等教育論、宗教哲学などに功績を残す。ケンブリッジ大学、ユニバーシティ・カレッジ・ロンドン、インペリアル・カレッジ・ロンドン、ハーバード大学の各大学において、教鞭をとる。哲学者としての彼の業績は、ハーバード大学に招聘されてからが主体であり、その時既に63歳であった。.
新しい！!: 自動定理証明とアルフレッド・ノース・ホワイトヘッド · 続きを見る »
アルゴンヌ国立研究所
アルゴンヌ国立研究所 アルゴンヌ国立研究所（Argonne National Laboratory）は、アメリカ合衆国の国立研究所である。.
新しい！!: 自動定理証明とアルゴンヌ国立研究所 · 続きを見る »
アレン・ニューウェル
アレン・ニューウェル（Allen Newell, 1927年3月19日 - 1992年7月19日）は、初期の人工知能研究の研究者。計算機科学および認知心理学の研究者であり、ランド研究所やカーネギーメロン大学の計算機科学科、テッパー・スクール・オブ・ビジネスに勤務した。ハーバート・サイモンと共に開発した Information Processing Language (1956) や2つの初期のAIプログラムである Logic Theory Machine (1956) と General Problem Solver (1957) で知られている。1975年、人工知能と認知心理学への基礎的貢献が認められ、ハーバート・サイモンと共にACMチューリング賞を受賞。.
新しい！!: 自動定理証明とアレン・ニューウェル · 続きを見る »
アロンゾ・チャーチ
アロンゾ・チャーチ（Alonzo Church, 1903年6月14日 - 1995年8月11日）はアメリカの論理学者、数学者。ラムダ計算の創案者、「チャーチ＝チューリングのテーゼ」の提唱者として知られる。.
新しい！!: 自動定理証明とアロンゾ・チャーチ · 続きを見る »
アドバンスト・マイクロ・デバイセズ
アドバンスト・マイクロ・デバイセズ（Advanced Micro Devices, Inc.
新しい！!: 自動定理証明とアドバンスト・マイクロ・デバイセズ · 続きを見る »
インテル
インテル（英:Intel Corporation）は、アメリカ合衆国カリフォルニア州に本社を置く半導体素子メーカーである。 社名の由来はIntegrated Electronics（集積されたエレクトロニクス）の意味である。.
新しい！!: 自動定理証明とインテル · 続きを見る »
ウプサラ大学
ウプサラ大学（Uppsala universitet、Uppsala University）は、スウェーデンのウプサラにある、1477年に創設された北欧最古の大学。ヨーロッパの最も権威ある高等教育・研究機関の一つであり、15人の大学関係者（卒業生・教員等）がノーベル賞を受賞している。 大学間及び産学協力に積極的であり、ヨーロッパやアメリカ、アジアなど、世界の1,000以上の大学と約3,000にのぼる共同研究を行なっており、毎年、約5,000の学術出版物が発行されている。 数多くの分野で世界最先端の研究を実施しており、ウプサラ生物医学センター（BMC：The Uppsala Biomedical Centre）は、生命科学に関するヨーロッパ最大の拠点の一つであり、オングストローム研究所(Ångström Laboratory)は、材料科学に関するヨーロッパ最先端研究所の一つである。また、卒業生でもある第二代国連事務総長ダグ・ハマーショルドの名を冠した図書館を設置し、平和と紛争研究において世界的拠点の一つである研究所を擁している。.
新しい！!: 自動定理証明とウプサラ大学 · 続きを見る »
エルブランの定理
ルブランの定理（Herbrand's theorem）は1930年にジャック・エルブランが発表した数理論理学上の基本定理である 。 エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。 エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。 なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだがBuss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp.
新しい！!: 自動定理証明とエルブランの定理 · 続きを見る »
エルゼビア
thumb エルゼビア (Elsevier B.V.、エルゼビア・ベーフェー) は、オランダ・アムステルダムを本拠とする国際的な出版社。医学・科学技術関係を中心とする世界最大規模の出版社で、学術雑誌も多数発行している。現在はレレックス・グループの100%子会社である。日本法人はエルゼビア・ジャパン株式会社。.
新しい！!: 自動定理証明とエルゼビア · 続きを見る »
エディンバラ大学
ンバラ大学（University of Edinburgh）は、1583年に設立された、英国で6番目に長い歴史を有する大学である（「Ancient University」の1つ）。キャンパスはスコットランドの首都エジンバラにあり、ユネスコの世界遺産に登録されている旧市街の多くの建物がエジンバラ大学の所有物である。スコットランドで4番目に古い大学であり、スコットランドにある最高学府のうち最高峰とされている。QS世界大学ランキング2019では世界18位、英国5位、スコットランド1位であり、世界トップクラスの研究大学とされている。スコットランドの大学としてラッセルグループに所属しているのは当大学とグラスゴー大学のみであり、ヨーロッパの大学の提携組織であるコインブラ・グループ、ヨーロッパ研究大学連盟 (LERU) に加盟していることも特徴である。また、アイビーリーグやU15など米国やカナダの高等教育機関とも歴史的に深いつながりがあり、現在まで学術交流を盛んに行っている。 エジンバラ大学は啓蒙時代に優れた人材が輩出し、エジンバラは北のアテネと呼ばれるまでになった。主な卒業生として、物理学者ジェームズ・クラーク・マクスウェル、哲学者デイヴィッド・ヒューム、数学者トーマス・ベイズ、第74代英国首相ゴードン・ブラウン、医学者ジョゼフ・リスター、小説家アーサー・コナン・ドイル、小説家ウォルター・スコット、発明家アレクサンダー・グラハム・ベル、タンザニア初代首相ジュリウス・ニエレレなどがいる。また、中退ではあるが自然科学者チャールズ・ダーウィンも通っていた。エディンバラ大学はこれまで21名のノーベル賞受賞者とアーベル賞受賞者を1名を出している。英国王室とのつながりも深く、これまでにエディンバラ公爵フィリップや アン王女が総長についている。また、2003年にはスコットランドの大学として初めてフェアトレード賞を受賞した。.
新しい！!: 自動定理証明とエディンバラ大学 · 続きを見る »
カールスルーエ工科大学
ールスルーエ工科大学（独：KIT / Karlsruher Institut für Technologie）は、1825年、ルートヴィヒ1世 (バーデン大公) によって創立されたドイツでは最古の工業大学。ドイツのバーデン＝ヴュルテンベルク州に位置する。 ドイツ9大工科大学によるコンソーシアム（TU9）に参加している。世界100大学に常に入り、工学系は現在ドイツで最も評価が高い。.
新しい！!: 自動定理証明とカールスルーエ工科大学 · 続きを見る »
ギルモアのアルゴリズム
ルモアのアルゴリズム（Gilmore's algorithm）は、エルブランの定理にもとづき一階述語論理式が充足不能（unsatisfiable）かどうかを調べる半アルゴリズム（semi-algorithm）である。ギルモアのアルゴリズムは1960年に発表された。 P. Gilmore.
新しい！!: 自動定理証明とギルモアのアルゴリズム · 続きを見る »
クリフ・ショー
J・C・ショー (J.C.Shaw)、クリフ・ショー (Cliff Shaw) として知られた、ジョン・クリフォード・ショー（John Clifford Shaw、1922年 – 1991年）は、ランド研究所に所属したアメリカ合衆国のシステム・プログラマ。世界初の人工知能プログラムとされる Logic Theorist の共同開発者のひとりであり、1950年代のプログラミング言語であるInformation Processing Language (IPL)の開発者のひとりである。IPLは、JOSS言語の真の「父」であると考えられている。プログラミングの歴史における最も重要な出来事のひとつは、IPL-V言語の開発過程における、アレン・ニューウェル、ハーバート・A・サイモンとクリフ・ショーの3人による「リスト処理」という概念の開発であった。.
新しい！!: 自動定理証明とクリフ・ショー · 続きを見る »
クルト・ゲーデル
ルト・ゲーデル（Kurt Gödel, 1906年4月28日 - 1978年1月14日）は、オーストリア・ハンガリー二重帝国（現チェコ）のブルノ生まれの数学者・論理学者である。業績には、完全性定理及び不完全性定理、連続体仮説に関する研究が知られる。.
新しい！!: 自動定理証明とクルト・ゲーデル · 続きを見る »
ケンブリッジ大学
ンブリッジ大学（University of Cambridge）は、イギリスの大学都市ケンブリッジに所在する総合大学であり、イギリス伝統のカレッジ制を特徴とする世界屈指の名門大学である。中世に創設されて以来、英語圏ではオックスフォード大学に次ぐ古い歴史をもっており、アンシャン・ユニヴァシティーに属する。 ハーバード大学、シカゴ大学、オックスフォード大学等と並び、各種の世界大学ランキングで常にトップレベルの優秀な大学として評価されており、公式のノーベル賞受賞者は96人（2016年12月現在）と、世界の大学・研究機関で最多（内、卒業生の受賞者は65人）。総長はで、副総長は。 公式サイトでは国公立大学（Public University）と紹介している。法的根拠が国王の勅許状により設立された自治団体であること、大学財政審議会（UFC)を通じて国家から国庫補助金の配分を受けており、大学規模や文科・理科の配分比率がUFCにより決定されていること、法的性質が明らかに違うバッキンガム大学等の私立大学が近年新設されたことによる。ただし、自然発生的な創立の歴史や高度な大学自治、独自の財産と安定収入のあるカレッジの存在、日本でいう国公立大学とは解釈が異なる。 アメリカ、ヨーロッパ、アジア、アフリカ各国からの留学生も多い。2005年現在、EU外からの学生は3,000人を超え、日本からの留学生も毎年十数人～数十人規模となっている。研究者の交流も盛んで、日本からの在外訪問研究者も多い。.
新しい！!: 自動定理証明とケンブリッジ大学 · 続きを見る »
ゲーデルの完全性定理
数理論理学においてゲーデルの完全性定理（ゲーデルのかんぜんせいていり、Gödel's completeness theorem、Gödelscher Vollständigkeitssatz）とは、第一階述語論理の恒真な論理式はその公理系からすべて導出可能であることを示した定理を言う。1929年にクルト・ゲーデルが証明した。.
新しい！!: 自動定理証明とゲーデルの完全性定理 · 続きを見る »
ゲーデルの不完全性定理
ーデルの不完全性定理（ゲーデルのふかんぜんせいていり、）又は単に不完全性定理とは、数学基礎論における重要な定理で、クルト・ゲーデルが1930年に証明したものである。;第1不完全性定理: 自然数論を含む帰納的公理化可能な理論が、ω無矛盾であれば、証明も反証もできない命題が存在する。;第2不完全性定理: 自然数論を含む帰納的公理化可能な理論が、無矛盾であれば、自身の無矛盾性を証明できない。.
新しい！!: 自動定理証明とゲーデルの不完全性定理 · 続きを見る »
ゴットロープ・フレーゲ
フリードリヒ・ルートヴィヒ・ゴットロープ・フレーゲ（Friedrich Ludwig Gottlob Frege, 1848年11月8日 - 1925年7月26日）は、ドイツの哲学者、論理学者、数学者であり、現代の数理論理学、分析哲学の祖にあたる。 フレーゲはバルト海に面したドイツの港町ヴィスマールの生まれである。母のアウグステ・ビアロブロツキーはポーランド系である。彼ははじめイェーナ大学で学び、その後ゲッティンゲン大学に移り1873年に博士号を取得した。その後イェーナに戻り、1896年から数学教授。1925年に死去した。.
新しい！!: 自動定理証明とゴットロープ・フレーゲ · 続きを見る »
シュプリンガー・サイエンス・アンド・ビジネス・メディア
ュプリンガー・サイエンス・アンド・ビジネス・メディア（Springer Science+Business Media, Springer）は、科学（Science）、技術（Technology、工学など）、医学（Medicine）、すなわちSTM関連の書籍、電子書籍、査読済みジャーナルを出版するグローバル企業である。シュプリンガーはまた、"SpringerLink"（「シュプリンガー・リンク」） 、"SpringerProtocols"（「」） 、"SpringerImages"（「シュプリンガー・イメージ」） 、"SpringerMaterials"（「シュプリンガー・マテリアル」） などいくつかの科学データベース・サービスのホスティングも行っている。 出版物には、参考図書（Reference works、レ（リ）ファレンス・ワークス）、教科書、モノグラフ（Monograph）、（Proceedings）、叢書など多数が含まれる。また、シュプリンガー・リンクには45,000以上のタイトルが自然科学など13の主題・テーマで集められており、それらは電子書籍として利用可能である。シュプリンガーはSTM分野の書籍に関しては世界最大の出版規模を持ち、ジャーナルでは世界第2位である（第1位はエルゼビア）。 多数のインプリントや、20ヶ国に約55の発行所（パブリッシング・ハウス）、5,000人以上の従業員を抱え、毎年約2,000のジャーナル、7,000以上の新書（これにはSTM分野だけではなく、B2B分野のものも含まれる）を発刊している。シュプリンガーはベルリン、ハイデルベルク、ドルトレヒト、ニューヨークに主要オフィスを構える。近年成長著しいアジア市場のために、アジア地域本部を香港に置いており、2005年8月からは北京に代表部を設置している 。 2015年5月、シュプリンガー・サイエンス+ビジネスメディアとマクミラン・サイエンス・アンド・エデュケーションの大半の事業の合併が、欧州連合や米国司法省などの主要な公正競争監視機関により承認された。新会社の名称は「シュプリンガー・ネイチャー（Springer Nature）」。.
新しい！!: 自動定理証明とシュプリンガー・サイエンス・アンド・ビジネス・メディア · 続きを見る »
ジャック・エルブラン
ャック・エルブラン (Jacques Herbrand、1908年2月12日 - 1931年7月27日)はパリ生まれのフランスの数学者である。数理論理学と類体論に業績がある。再帰関数を導入した。エルブランの定理と呼ばれているものは、まったく別の２つの定理を指していう。ひとつは彼が博士論文として書いた証明論についてのものであり、もうひとつはエルブラン・リベットの定理と呼ばれているものである。エルブラン商とはホモロジー代数におけるオイラー標数の一種。彼はまたヒルベルトプログラムにも貢献した（弱い算術系における無矛盾性の証明）。.
新しい！!: 自動定理証明とジャック・エルブラン · 続きを見る »
スタンフォード大学
タンフォード大学（Stanford University）とは、アメリカ合衆国カリフォルニア州スタンフォードに本部を置く私立大学。正式名称はリーランド・スタンフォード・ジュニア大学（）。 校訓は「Die Luft der Freiheit weht（独：自由の風が吹く）」。サンフランシスコから約60 km南東に位置し、地理上も、歴史的にもシリコンバレーの中心に位置している。.
新しい！!: 自動定理証明とスタンフォード大学 · 続きを見る »
タブローの方法
タブローの方法(英 tableau method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。.
新しい！!: 自動定理証明とタブローの方法 · 続きを見る »
充足可能性問題
充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。.
新しい！!: 自動定理証明と充足可能性問題 · 続きを見る »
四目並べ
四目並べ（よんもくならべ）は、卓上で遊ぶゲームである。交互にコマを下から積み重ねて、先に縦・横・斜めいずれかに直線状に4つ並べた方が勝ちになる。.
新しい！!: 自動定理証明と四目並べ · 続きを見る »
四色定理
四色定理（よんしょくていり／ししょくていり、）とは、厳密ではないが日常的な直感で説明すると「平面上のいかなる地図も、隣接する領域が異なる色になるように塗り分けるには4色あれば十分だ」という定理である。.
新しい！!: 自動定理証明と四色定理 · 続きを見る »
Co-NP
co-NPとは計算量理論における問題クラスの一つである。.
新しい！!: 自動定理証明とCo-NP · 続きを見る »
Cycプロジェクト
Cyc（サイク）は、人工知能へのアプローチのひとつ。一般常識をデータベース化し（知識ベース）、人間と同等の推論システムを構築することを目的とするプロジェクトである。「Cyc」の名は「encyclopedia」に由来する。 1984年に MCC 社のダグラス・レナートによって開始。人手による入力作業が続けられており、1995年には Cycorp 社が設立され、2001年からは知識ベースの一部が OpenCyc として公開されている。 2010年代に流行し始めたニューラルネットワークによる統計処理とは異なる、人間の常識に根ざした推論を可能にするとしている。.
新しい！!: 自動定理証明とCycプロジェクト · 続きを見る »
第二次世界大戦
二次世界大戦（だいにじせかいたいせん、Zweiter Weltkrieg、World War II）は、1939年から1945年までの6年間、ドイツ、日本、イタリアの日独伊三国同盟を中心とする枢軸国陣営と、イギリス、ソビエト連邦、アメリカ 、などの連合国陣営との間で戦われた全世界的規模の巨大戦争。1939年9月のドイツ軍によるポーランド侵攻と続くソ連軍による侵攻、そして英仏からドイツへの宣戦布告はいずれもヨーロッパを戦場とした。その後1941年12月の日本とイギリス、アメリカ、オランダとの開戦によって、戦火は文字通り全世界に拡大し、人類史上最大の大戦争となった。.
新しい！!: 自動定理証明と第二次世界大戦 · 続きを見る »
算術の基礎
『算術の基礎』（さんじゅつのきそ、Die Grundlagen der Arithmetik）とは1884年に出版されたゴットロープ・フレーゲの本のことである。この本の中でフレーゲは算術の哲学の基礎を研究している。文学的・哲学的価値をもつ傑作の中で、フレーゲは他の数の理論を破壊し、彼自身の数の理論を開発した。 『算術の基礎』はまた、フレーゲの後の論理主義の仕事を動機づける助けとなった。この本は出版されたとき、評判がよくなく、広く読まれなかった。 この本はしかし、バートランド・ラッセルとルートヴィヒ・ウィトゲンシュタインの注意を引き、2人ともフレーゲの哲学から重い影響をうけた。.
新しい！!: 自動定理証明と算術の基礎 · 続きを見る »
DPLLアルゴリズム
Davis-Putnam-Logemann-Lovelandアルゴリズム（DPLLアルゴリズム、Davis-Putnam-Logemann-Loveland algorithm）とは、数理論理学および計算機科学において、論理式の充足可能性を調べるアルゴリズムである。連言標準形で表現された命題論理式を対象とし、論理式を真（True）にできるかどうかを判定する。この判定問題はCNF-SATと呼ばれる。 このアルゴリズムは、1960年に発表されたデービス・パトナムのアルゴリズム（Davis–Putnam algorithm）の改良版として、1962年に、、が発表した 。 なお、文献によってはDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。.
新しい！!: 自動定理証明とDPLLアルゴリズム · 続きを見る »
選言標準形
選言標準形（せんげんひょうじゅんけい、Disjunctive normal form, DNF）は、数理論理学においてブール論理での論理式の標準化（正規化）の一種であり、連言節(AND)の選言(OR)の形式で論理式を表す。加法標準形、主加法標準形、積和標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。.
新しい！!: 自動定理証明と選言標準形 · 続きを見る »
項書き換え
項書き換え（こうかきかえ、term rewriting）とは、数学・計算機科学・論理学において、式（数式、論理式）の項を別の項に置換する手法を総称する用語である。項書き換え系（term rewriting system、TRS）とは、項の集合とその置換規則から構成される。 項書き換えは非決定論的になることがありうる。ある規則で書き換え可能な項が他の規則でも書き換え可能な場合がありえて、その場合は複数の規則が適用可能と言うことになる。項書き換え系では、項書き換えのためのアルゴリズムは提供されず、書き換え規則の集合のみが提供される。しかし、適当なアルゴリズムと組み合わせれば、項書き換え系はプログラムのような働きをし、実際いくつかの宣言型プログラミング言語は項書き換えに基づいている。.
新しい！!: 自動定理証明と項書き換え · 続きを見る »
証明
証明（しょうめい）とは、ある事柄が真理もしくは事実であることを明らかにすること。また、その内容。.
高階述語論理
階述語論理（こうかいじゅつごろんり、Higher-order logic）は、一階述語論理と様々な意味で対比される用語である。 例えば、その違いは量化される変項の種類にも現われている。一階述語論理では、大まかに言えば述語に対する量化ができない。述語を量化できる論理体系については二階述語論理に詳しい。 その他の違いとして、基盤となる型理論で許されている型構築の違いがある。高階述語（higher-order predicate）とは、引数として1つ以上の別の述語をとることができる述語である。一般に n 階の高階述語の引数は1つ以上の (n − 1) 階の述語である（ここで n > 1）。同じことは高階関数（higher-order function）にも言える。 高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理は（帰納的に公理化された）健全で完全な証明計算が認められないとされた。しかし、Henkin model によれば、健全で完全な証明計算は存在する。 高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。.
新しい！!: 自動定理証明と高階述語論理 · 続きを見る »
論理学
論理学（ろんりがく、）とは、「論理」を成り立たせる論証の構成やその体系を研究する学問である。.
新しい！!: 自動定理証明と論理学 · 続きを見る »
論理プログラミング
論理プログラミング（Logic Programming）とは、広い意味では、コンピュータプログラミングでの数理論理学の使用である。この観点での論理プログラミングは、ジョン・マッカーシーのadvice takerの提案にまでさかのぼることができる。 より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。 論理をベースにしたプログラミング言語として1971年に Planner のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった。Plannerと独立してより論理を重視した Prolog が開発され、コワルスキーにより述語論理式(ホーン節)のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した。 Planner からの派生で、プログラミング言語 Poplerが開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、Oz、Fril などがある。バックトラッキングを使用しない並行論理プログラミング言語としてProlog からの派生したConcurrent Prolog、PARLOG、GHC、KL1などの各種言語（Shapiro に調査結果がある）がある。.
新しい！!: 自動定理証明と論理プログラミング · 続きを見る »
自動推論
自動推論（じどうすいろん、Automated Reasoning）は計算機科学と数理論理学の一分野であり、推論の様々な側面を理解することでコンピュータによる完全（あるいはほぼ完全）自動な推論を行うソフトウェアを開発することを目的とする。人工知能研究の一部と考えられるが、理論計算機科学や哲学とも深い関係がある。 自動推論のなかでも最も研究が進んでいるのは、自動定理証明（および完全自動ではないがより現実的な）と（固定の前提条件下での推論と見なすことができる）であるが、他にも類推、帰納、アブダクションによる推論の研究も盛んである。他の重要なトピックとしては、不確かさのある状況での推論と非単調推論である。不確かさに関する研究では論証（argumentation）が重要である。それはすなわち、標準的な自動推論へのさらなる極小性と一貫性の適用である。John Pollock の Oscar システムは単なる自動定理証明機よりも自動論証システムといえるものである。 自動推論のツールや手法としては、古典的論理学や代数学があるが、他にもファジィ論理、ベイズ推定、最大エントロピー原理に基づく推論、その他のあまり形式的でない技法などがある。.
新しい！!: 自動定理証明と自動推論 · 続きを見る »
自然数
自然数（しぜんすう、natural number）とは、個数、もしくは順番を表す一群の数のことである。集合論においては、自然数は物の個数を数える基数のうちで有限のものであると考えることもできるし、物の並べ方を示す順序数のうちで有限のものであると考えることもできる。 自然数を 1, 2, 3, … とする流儀と、0, 1, 2, 3, … とする流儀があり、前者は数論などでよく使われ、後者は集合論、論理学などでよく使われる（詳しくは自然数の歴史と零の地位の節を参照）。いずれにしても、0 を自然数に含めるかどうかが問題になるときは、その旨を明記する必要がある。自然数の代わりに非負整数または正整数と言い換えることによりこの問題を避けることもある。 数学の基礎付けにおいては、自然数の間の加法についての形式的な逆元を考えることによって整数を定義する。正の整数ないしは負でない整数を自然数と同一視し、自然数を整数の一部として取扱うことができる。自然数と同様に整数の全体も可算無限集合である。 なお、文脈によっては、その一群に属する個々の数（例えば 3 や 18）を指して自然数ということもある。.
新しい！!: 自動定理証明と自然数 · 続きを見る »
集積回路設計
集積回路設計（しゅうせきかいろせっけい）の記事では、集積回路の設計について解説する。主な領域を占める電子工学の他、半導体物性等から論理設計など応用分野に応じた各種の知識と技術も必要である。集積回路そのものについては集積回路の記事を参照のこと。.
新しい！!: 自動定理証明と集積回路設計 · 続きを見る »
FPU
FPU（Floating Point Unit、浮動小数点（演算処理）装置）とは、浮動小数点演算を専門に行う処理装置のこと。コンピュータの周辺機器のようなアーキテクチャのものもあれば、主プロセッサと一体化したコプロセッサのようなアーキテクチャのものもある。 AMDではAm9511をAPU (Arithmetic Processing Unit) と呼んでおり（2011年以降はAPUをAccelerated Processing Unitの略称として使用）、インテルではx87をNDP（Numeric data processor, 数値演算コプロセッサ）、またその命令についてNPX（Numeric Processor eXtension）とも呼んでいる。 マイクロプロセッサにおいては、Apple IIの頃は完全に周辺機器のようなアーキテクチャだったが、8087の頃には命令の一体化など、CPUの拡張装置のようなアーキテクチャになった。 インテルのx86系CPUでは387（386用）が最後となり、486からは同一のチップ内に内蔵された（486の初期には、FPUを内蔵しない廉価版と、事実上はオーバードライブプロセッサであった487もあった）。同様に、モトローラの68000系でもMC68040以降のMPUではチップ内に内蔵している。 1990年代中盤以降の高性能プロセッサではFPUはプロセッサ内部のサブユニットとなっている。プロセッサに内蔵されたFPUは、スーパースカラーで他ユニットと並列動作させることができるなど様々なメリットがあるため、現在ではFPUを単体で用いることは珍しくなっている。.
新しい！!: 自動定理証明とFPU · 続きを見る »
General Problem Solver
General Problem Solver（GPS）とは、1957年、ハーバート・サイモンとアレン・ニューウェルが開発した、汎用の問題解決のためのプログラムである。GPS は任意の形式化された記号問題を解くことができる。例えば、定理証明、幾何学問題、チェスのプレイなどである。これは、サイモンとニューウェルの論理機械に関する理論研究に基づいていた。GPSは、正しく形式化されていさえすればハノイの塔も解くことが可能だったが、実世界の問題を解くことはできなかった。 ユーザーはオブジェクトとそのオブジェクトに関する操作を定義し、GPSは手段目標分析によって問題解決のためのヒューリスティックスを生成する。それは使用可能な操作に注目し、受容される入力と、その結果生成される出力を見つけ出す。次に目標に近づくためのサブゴールを生成していく。 GPSの方法論は後に Soar へと発展した。.
新しい！!: 自動定理証明とGeneral Problem Solver · 続きを見る »
GNU General Public License
GNU General Public License(GNU GPLもしくは単にGPLとも)とは、GNUプロジェクトのためにリチャード・ストールマンにより作成されたフリーソフトウェアライセンスである。八田真行の日本語訳ではGNU 一般公衆利用許諾書と呼んでいる。.
新しい！!: 自動定理証明とGNU General Public License · 続きを見る »
Java Web Start
Java Web Start（ジャバウェブスタート）はJava製アプリケーションをウェブサーバなどから自動ダウンロード、自動インストール、自動アップデートして、サンドボックス上にて実行可能な仕組み。Java 5にて搭載され、Java 9にて廃止予定（deprecated）となった。Swing APIなどで記述されたGUIアプリケーションを実行できる。問題点が多いためにFlashよりも劣ると言われるJavaアプレットの代替リッチクライアントと言われている。 たとえば、ウェブブラウザでJava Web Startに対応したJavaアプリケーションへのリンクをクリックすると、Javaアプレットのようなブラウザ埋め込み型ではなくメディアプレーヤーなどの外部アプリケーションのようにJava Web Startが起動する。Java Web Startがインストールされていないときは、Java Web Startソフトウェア（Java Web Startの管理・実行ソフトウェア）が自動ダウンロード、自動インストールされる。JREがインストールされていないときは、それも自動的にインストールされる。さらに、JRE、Java Web Startそれぞれのバージョンが古いときは自動的にアップデートされる。また、Java Web Start対応Javaアプリケーションが古く、最新バージョンがサーバにアップロードされている場合は、実行前の事前確認により自動的にアップデートされる。 なお、Java Web Start対応Javaアプリケーションはローカルマシンに保存される。よって、二回目以降の起動は、ダウンロードなどが不要となり高速に起動できる。 現在のJava Web Start はOSとの協調動作も行なわれる。たとえば、Windowsにおいて「プログラムの追加と削除」を利用したJava Web Startアプリケーションのアンインストールが可能である。また、プログラムメニューやデスクトップへのショートカットアイコンの作成なども行なわれる。.
新しい！!: 自動定理証明とJava Web Start · 続きを見る »
Logic Theorist
Logic Theorist は、1955年から1956年にかけてアレン・ニューウェル、ハーバート・サイモン、J・C・ショーが開発したコンピュータプログラム。人間の問題解決能力を真似するよう意図的に設計された世界初のプログラムであり、「世界初の人工知能プログラム」と称された。ホワイトヘッドとラッセルの『プリンキピア・マテマティカ』の冒頭の52の定理のうち38を証明してみせ、一部については新たなもっと洗練された証明方法を発見している。.
新しい！!: 自動定理証明とLogic Theorist · 続きを見る »
Pentium FDIV バグ
Pentium FDIV バグは、インテルのPentiumプロセッサに含まれていた、特定の値の除算の結果が誤ったものになる、というバグである。.
新しい！!: 自動定理証明とPentium FDIV バグ · 続きを見る »
S&P グローバル
S&P グローバル（S&P Global Inc.）は、アメリカ合衆国・ニューヨーク市に本拠を置く金融サービス企業。S&P グローバル・レーティングやS&P ダウ・ジョーンズ・インデックスなど、4つの事業体の親会社にあたる。旧社名はマグロウヒルファイナンシャル。ニューヨーク証券取引所上場企業（）。.
新しい！!: 自動定理証明とS&P グローバル · 続きを見る »
SRIインターナショナル
SRIインターナショナル（SRI International）は、世界で最も大きな研究機関のひとつである。1946年、スタンフォード大学により、スタンフォード研究所（Stanford Research Institute）の名で地域の経済発展を支援する目的で設置されたものである。 1970年に完全に大学から独立し、アメリカ合衆国の非営利組織として独自の法人となった。1975年に SRIインターナショナルへと改称。科学技術の発見・応用を通して、知識・経済・繁栄・平和へ貢献することを目的としている。政府機関、企業、私立財団などの顧客から研究開発を請け負っている。テクノロジーのライセンス提供、戦略的提携、スピンオフ企業の創業なども行っている。 スタンフォード大学からそう遠くないカリフォルニア州のメンローパーク市に本拠地を持つ。1998年から、物理学者が所長 (CEO) を務めている。2012年の年間収入は約5億8500万ドルで、従業員は2,200名である。 主な研究分野は、生命医学、化学物質と材料、情報処理、地球および宇宙、経済、教育と学習、エネルギーと環境技術、セキュリティと国防、センサーなどである。千件以上の特許を所有している。.
新しい！!: 自動定理証明とSRIインターナショナル · 続きを見る »
概念記法
The title page of the original 1879 edition 『概念記法』（がいねんきほう、Begriffsschrift）はゴットロープ・フレーゲによって1879年に出版された論理学に関する短い本の題名であり,またその本で創始された形式体系の名称である。 この本の完全な書名は「算術の式言語を模した、純粋な思考のための一つの式言語 eine der arithmetischen nachgebildete Formelsprache des reinen Denkens」である。『概念記法』は,アリストテレスが論理学という主題を創設して以来,論理学に関するおそらく最も重要な出版物であった。フレーゲが自分の式を開発して論理に到達しようとした動機は,ライプニッツが彼の推論計算機に対して持った動機と似ている。続いてフレーゲは,数学の基礎の研究に彼の論理計算を用い,それは次の四半世紀にわたって遂行された。.
新しい！!: 自動定理証明と概念記法 · 続きを見る »
決定可能性
決定可能（けっていかのう、decidable）は、論理学において、論理式の集合のメンバーシップの決定をする実効的（effectiveな）方法が存在することを指す。決定可能性（けっていかのうせい、decidability）は、そのような属性を指す。命題論理のような形式体系は、論理的に妥当な論理式（または定理）の集合のメンバーシップを実効的に決定できるなら、決定可能である。ある決まった論理体系における理論（論理的帰結で閉じている論理式の集合）は、任意の論理式がその理論に含まれるか否かを決定する実効的方法があれば、決定可能である。.
新しい！!: 自動定理証明と決定可能性 · 続きを見る »
数学的帰納法
数学的帰納法（すうがくてききのうほう、mathematical induction）は自然数に関する命題 が全ての自然数 に対して成り立っている事を証明するための、次のような証明手法である自然数の定義は を含む流儀とそうでない流儀があるが、ここでは後者を採用した。。.
新しい！!: 自動定理証明と数学的帰納法 · 続きを見る »
数式処理システム
数式処理システム（すうしきしょりシステム、Computer algebra system、CAS，Formula Manipulation System，広義にはSymbolic Computation System）は、コンピュータを用いて数式を記号的に処理するソフトウェアである。コンピュータによる通常の数値計算処理では実数を有限精度の数値（浮動小数点数）で近似し、数値と演算に対して丸め誤差を許容して計算を行なうので数学的に厳密な結果を得ることが困難もしくは不可能であるのに対して、数式処理システムでは主に抽象度の高い記号列を取り扱い，可能な範囲で代数的な規則に基づきながら厳密な記号処理を行う。ただし最近では応用性と実用性の観点から、数値とその演算に対して浮動小数点数も扱える（数値・数式の）融合計算システムとでも呼べるような数式処理システムも増えて来た。 また，数式処理システムに向けた計算アルゴリズムを研究する分野も数式処理（あるいは computer algebra の直訳として計算機代数）と呼ぶ。.
新しい！!: 自動定理証明と数式処理システム · 続きを見る »
数理論理学
数理論理学（mathematische Logik、mathematical logic）は、論理学（形式論理学）の数学への応用の探求ないしは論理学の数学的な解析を主たる目的とする、数学の関連分野である。局所的には数理論理学は超数学、数学基礎論、理論計算機科学などと密接に関係している。数理論理学の共通な課題としては形式体系の表現力や形式証明系の演繹の能力の研究が含まれる。 数理論理学はしばしば集合論、モデル理論、再帰理論、証明論の4つの領域に分類される。これらの領域はロジックのとくに一階述語論理や定義可能性に関する結果を共有している。計算機科学（とくに）における数理論理学の役割の詳細はこの記事には含まれていない。詳細はを参照。 この分野が始まって以来、数理論理学は数学基礎論の研究に貢献し、また逆に動機付けられてきた。数学基礎論は幾何学、算術、解析学に対する公理的な枠組みの開発とともに19世紀末に始まった。20世紀初頭、数学基礎論は、ヒルベルトのプログラムによって、数学の基礎理論の無矛盾性を証明するものとして形成された。クルト・ゲーデルとゲルハルト・ゲンツェンによる結果やその他は、プログラムの部分的な解決を提供しつつ、無矛盾性の証明に伴う問題点を明らかにした。集合論における仕事は殆ど全ての通常の数学を集合の言葉で形式化できることを示した。しかしながら、集合論に共通の公理からは証明することができない幾つかの命題が存在することも知られた。むしろ現代の数学基礎論では、全ての数学を展開できる公理系を見つけるよりも、数学の一部がどのような特定の形式的体系で形式化することが可能であるか（逆数学のように）ということに焦点を当てている。.
新しい！!: 自動定理証明と数理論理学 · 続きを見る »
