ブラウザよりも高速アクセス！
19 関係: 型理論、並行性、人工知能と法、形式的検証、モナド (プログラミング)、モデル検査、レスリー・ランポート、デイナ・スコット、アミール・プヌーリ、エキスパートシステム、ジョン・レモン、ストア派、知識表現、線形時相論理、非古典論理、計算木論理、論理学の歴史、自然演繹、様相論理。
型理論
型理論（かたりろん、Type theory）は、数理論理学の一分野であり、「型」の階層を構築し、それぞれの型に数学的（あるいはそれ以外の）実体を割り当てるものである。階型理論（かいけいりろん、Theory of Types）とも。ある型のオブジェクトはその前提となる型のオブジェクトから構築される。この場合の「型」とは形而上的な意味での「型」である。バートランド・ラッセルは、彼が発見したラッセルのパラドックスにより素朴集合論の問題が明らかにされたことを受けて、型理論を構築した。型理論の詳細はホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』にある。 型理論は、プログラミング言語の理論における型システムのベースにもなっている。「型システム」と「型理論」の語はほぼ同義として扱われることもあるが、ここでは、この記事では数理論理学の範囲を説明し、プログラミング言語の理論については型システムの記事で説明する。.
並行性
並行性(へいこうせい、concurrency)とは、計算機科学において、時間的にオーバーラップして実行される計算を伴うシステムの属性であり、そのような計算ではリソースを共有することがある。並行計算は、同一チップ上の複数のコア、単一プロセッサ上のプリエンプションを伴うマルチスレッド、物理的に分離した複数プロセッサ上などで行われる。並行計算のための数学的モデルとして、ペトリネット、プロセス計算、並列ランダムアクセス機械モデル、アクターモデル、 などが開発された。.
人工知能と法
人工知能と法(Artificial Intelligence and Law, AI and Law) とは、人工知能研究の一部門であり、主として人工知能技術を法情報学の問題へと応用し、あるいはこれらの問題について独自の研究をする領域である。 それは他の問題の解決にも資する。すなわち、法的問題の文脈で開発されてきた技術および道具立てを人工知能一般へと還元するのである。例えば、法的意思決定の理論、特に議論のモデルは、知識表現と推論の研究に貢献してきた。また、規範に基づく社会の組織化のモデルは、マルチエージェントシステムの研究に貢献してきた。あるいは、法的事例についての推論は事例ベース推論の研究に貢献してきた。そして、大規模な文章データの保存および検索の必要は、概念情報検索と知識データベースの研究へと結実した。.
新しい！!: 時相論理と人工知能と法 · 続きを見る »
形式的検証
形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。.
新しい！!: 時相論理と形式的検証 · 続きを見る »
モナド (プログラミング)
関数型プログラミングにおいて、モナド(monad)は計算を表現する構造であり、計算ステップの列からなる。つまり、型がモナド構造をもつというのは、命令を繋げるやり方、言い換えるとその型をもつ関数をネストさせる規則が定まっていることをいう。これはプログラマがパイプラインを作ることを可能にする。パイプラインでは入力データを１ステップずつ処理するが、モナドは各アクションに追加の処理規則を上乗せすることができるO'Sullivan, Bryan; Goerzen, John; Stewart, Don.
新しい！!: 時相論理とモナド (プログラミング) · 続きを見る »
モデル検査
モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。.
新しい！!: 時相論理とモデル検査 · 続きを見る »
レスリー・ランポート
レスリー・ランポート（Leslie Lamport、1941年2月7日 - ）は、数学者であり、コンピュータ科学者である。博士。ニューヨーク市生まれ。 TeX の上にマクロパッケージを組み込んで構築した組版処理システムである LaTeX の開発者として有名である。 また、コンピュータ科学では、時相論理・フォールトトレランス・分散コンピューティングの研究者として有名である。 マサチューセッツ工科大学にて1960年に学士号、ブランダイス大学にて1963年に修士号、1972年に博士号を授与されている。 現在は、マイクロソフト社の基礎研究所であるマイクロソフトリサーチで研究を行っている。2013年チューリング賞受賞。.
新しい！!: 時相論理とレスリー・ランポート · 続きを見る »
デイナ・スコット
デイナ・スチュアート・スコット (Dana Stewart Scott, 1932年-) はアメリカの計算機科学者、数学者、論理学者。数学的に難しい問題についての素養に基づき、非形式的だが厳格な方法で計算機科学・論理学・哲学にまたがる領域の根本的概念を明確化させてきた。オートマトン理論についての業績により1976年にチューリング賞を受賞。1970年代にはクリストファー・ストレイチーと共同でプログラム意味論への新たなアプローチを基礎付けた。様相論理、位相幾何学、圏論などでも業績を残している。 2012年現在は、カーネギーメロン大学で計算機科学と哲学と数理論理学の名誉教授を務めている。事実上引退しており、カリフォルニア州バークレー在住。2005年に創刊した学術誌 Logical Methods in Computer Science の編集長を務めている。.
新しい！!: 時相論理とデイナ・スコット · 続きを見る »
アミール・プヌーリ
アミール・プヌーリ、ア（ー）ミール・ペヌーエーリー、アミル・ペヌエリ（אַמִיר(אָמִיר) פְּנוּאֵלִי a(ā)mīr pənū’ēlī; Amir Pnueli、1941年4月22日 - 2009年11月2日）は、イスラエル人の計算機科学者。.
新しい！!: 時相論理とアミール・プヌーリ · 続きを見る »
エキスパートシステム
パートシステム（）は人工知能研究から生まれたコンピュータシステムで、人間の専門家（エキスパート）の意思決定能力をエミュレートするものである。専門家のように知識についての推論によって複雑な問題を解くよう設計されており、通常のプログラミングのようにソフトウェア開発者が設定した手続きに従うわけではない。1970年代に人工知能の研究者によって開発され、1980年代にわたって商業的に適用され、AIソフトウェアとして最初に成功を収めた形態である。日本語訳では専門家システムと言う場合もある。 エキスパートシステムは基本的に、特定の分野の問題についての情報を解析するルール群から構成されるプログラムであり、その情報はシステムの利用者が提供する。 問題の分析結果を提供するだけでなく、設計によっては利用者の行動を正しく導く指針を与えることもできる。通常のプログラムとは異なった独特の構造をしている。2つの部分で構成されており、1つはそのエキスパートシステムから独立している推論エンジンであり固定である。もう1つは知識ベースで、可変である。推論エンジンが知識ベースを使って推論を行う。80年代になると、利用者とやりとりするための対話インタフェースが第3の部分として登場した。利用者との会話によって知識ベースを構築することから、後に会話型 (en:Conversational Programming System) と呼ばれるようになった。 関連用語としてウィザードがある。エキスパートシステムのように、ウィザードもユーザが問題を解決するのを手助けする対話型コンピュータプログラムである。普通、ウィザードという用語は、ユーザにより入力された指針に従ってデータベースで検索するプログラムを指す。あいにく、これらの2つの定義の区別は確定したものではなくルールベースのプログラムの中にはウィザードと呼ばれるものもある。.
新しい！!: 時相論理とエキスパートシステム · 続きを見る »
ジョン・レモン
ドワード・ジョン・レモン (Edward John Lemmon、1930年6月1日 – 1966年7月29日) はイギリスの論理学者 、哲学者。シェフィールド生まれ。レモンは様相論理学において知られている。死後、出版されたデイナ・スコットとの共著（An introduction to modal logic, 1977）が有名。 レモンはシェフィールドにある高校（King Edward VII School）に通い、その後オックスフォード大学のマグダレン・カレッジにて学ぶ。 1957年には同大学のトリニティ・カレッジのフェローに任命された。1963年アメリカに移住しクレアモント大学院大学に勤めた。彼は登山中に心臓病で亡くなった。.
新しい！!: 時相論理とジョン・レモン · 続きを見る »
ストア派
トア派(Στωικισμός)はヘレニズム哲学の一学派で、紀元前3世紀初めにキティオンのゼノンによって始められた。破壊的な衝動は判断の誤りから生まれるが、知者すなわち「道徳的・知的に完全」な人はこの種の衝動に苛まされることはない、と説いた, Stanford Encyclopedia of Philosophy.
知識表現
知識表現（ちしきひょうげん）、KR（Knowledge Representation）は、推論を導けるような知識の表現、およびその方法を開発する人工知能研究の領域である。 思考を形式的に分析し、議論領域を記述する。一般に、議論領域の記述から推論するための形式意味論を与え、解釈可能な意味を各文が生じるように演算子を与える。それによって自動推論が可能となる。 知識表現は、表現力が高いほど、事柄が簡潔に記述されるが、一貫性が保障されず、自動推論が困難となる。例として、命題論理は自己認識的時相論理よりも表現力が低い。用途・必要性・資源との適合性がKR推論システムの開発において大切となる。 最近の主な知識表現の研究としてセマンティック・ウェブがある。XML型言語の知識表現と標準の開発に随伴することが多い。.
線形時相論理
線形時相論理（せんけいじそうろんり、Linear Temporal Logic、LTL）とは、時間に関する様相を持つ様相時相論理である。LTLでは、ある条件が最終的に真となるとか、別の事実が真になるまでその条件は真であるとかいった将来の出来事について論理式で表すことができる。.
新しい！!: 時相論理と線形時相論理 · 続きを見る »
非古典論理
非古典論理（ひこてんろんり、non-classical logic(s)）は、古典論理におけるいくつかの仮定を否定、もしくは置き換えることによって構築された論理、あるいは、古典論理における仮定をすべて認めた上で新たな仮定を付け加えることによって構築された論理の総称である。.
新しい！!: 時相論理と非古典論理 · 続きを見る »
計算木論理
計算木論理（けいさんきろんり、Computational Tree Logic、CTL）は、分岐時相論理の一種である。その時間モデルでは未来は決定されておらず木構造のように分岐している。未来の複数の経路のうちの1つが実際に現実の経路となる。.
新しい！!: 時相論理と計算木論理 · 続きを見る »
論理学の歴史
論理学の歴史では妥当な推論を探求する学問の発展を取り扱う。形式論理学は古代の中国、インド、ギリシアで発展した。ギリシア論理学、中でもアリストテレス論理学は科学・数学に広く受容・応用されている。 アリストテレス論理学は中世のイスラーム圏およびキリスト教西方世界にさらに発展し、14世紀半ばに頂点をむかえた。14世紀から19世紀初めまでの時期は概して論理学が衰退し、軽視された時期であり、少なくとも一人の論理学史家によって論理学の不毛期とみなされているOxford Companion p. 498; Bochenski, Part I Introduction, passim。 19世紀半ばになると論理学が復興し、革命期が始まって、数学において用いられる厳密な証明を手本とする厳格かつ形式的な規則へと主題が発展した。近現代におけるこの時期の発展、いわゆる「記号」あるいは「数理」論理学は二千年にわたる論理学の歴史において最も顕著なものであり、人類の知性の歴史において最も重要・顕著な事件の一つだと言えるOxford Companion p. 500。 数理論理学の発展は20世紀の最初の数十年に、特にゲーデルおよびタルスキの著作によって起こり、分析哲学や哲学的論理学に、特に1950年代以降に様相論理や時相論理、義務論理、適切さの論理といった分野に影響を与えた。.
新しい！!: 時相論理と論理学の歴史 · 続きを見る »
自然演繹
自然演繹（しぜんえんえき、Natural deduction）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。.
様相論理
様相論理（ようそうろんり、modal logic）は、いわゆる古典論理の対象でない、様相（modal）と呼ばれる「〜は必然的に真」や「〜は可能である」といった必然性や可能性などを扱う論理である（様相論理は、部分の真理値からは全体の真理値が決定されない内包論理の一種と見ることができる）。 その歴史は古くアリストテレスまで遡ることができるが、形式的な扱いは数理論理学以降、非古典論理としてである。 様相論理では一般に、標準的な論理体系に「～は必然的である」ことを意味する必然性演算子 \Box と、「～は可能である」ことを意味する可能性演算子 \Diamond のふたつの演算子が追加される。.
ここにリダイレクトされます：
時制論理。
