ブラウザよりも高速アクセス！
32 関係: 単項演算、三段論法、一階述語論理、二項演算、予定説、形式的検証、作用素、チャールズ・サンダース・パース、チョムスキー階層、命題論理、アミール・プヌーリ、アリストテレス、アレン・エマーソン、アロンゾ・チャーチ、エドムンド・クラーク、オートマトン、オックスフォード大学、ソール・クリプキ、状態遷移系、線形時相論理、真理関数、複雑性、計算機科学、計算木論理、論理学、論理演算、自由意志、Property Specification Language、Well-formed formula、様相論理、時間、1950年代。
単項演算
単項演算とは、数学で、被作用子（オペランド）が一つだけであるような演算（つまり、入力が一つの演算）のこと。 たとえば、論理否定は真理値に対する単項演算であり、自乗は実数に対する単項演算である。階乗 n! も単項演算である。与えられた集合 S に対する単項演算は、関数 S→S に他ならない。 単項演算は、プログラミング言語においても使われる（APLではmonadicという）。たとえば、C言語の系統では、以下の単項演算子がある。.
三段論法
三段論法（さんだんろんぽう、συλλογισμός, シュロギスモス、syllogismus、syllogism）は、論理学における論理的推論の型式のひとつ。典型的には、大前提、小前提および結論という3個の命題を取り扱う。これを用いた結論が真であるためには、前提が真であること、および論理の法則（同一律、無矛盾律、排中律、および充足理由律）が守られることが必要とされる。 アリストテレスの『オルガノン』（『分析論前書』『分析論後書』）によって整備された。.
一階述語論理
一階述語論理（いっかいじゅつごろんり、first-order predicate logic）とは、個体の量化のみを許す述語論理 (predicate logic) である。述語論理とは、数理論理学における論理の数学的モデルの一つであり、命題論理を拡張したものである。個体の量化に加えて述語や関数の量化を許す述語論理を二階述語論理（にかいじゅつごろんり、second-order predicate logic）と呼ぶ。それにさらなる一般化を加えた述語論理を高階述語論理（こうかいじゅつごろんり、higher-order predicate logic）という。本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細は「二階述語論理」「高階述語論理」を参照。.
新しい！!: 時相論理と一階述語論理 · 続きを見る »
二項演算
数学において、二項演算（にこうえんざん、binary operation）は、数の四則演算（加減乗除）などの 「二つの数から新たな数を決定する規則」 を一般化した概念である。二項算法（にこうさんぽう）、結合などともいう。.
予定説
予定説（よていせつ）は、聖書からジャン・カルヴァンによって提唱されたキリスト教の神学思想。カルヴァンによれば、神の救済にあずかる者と滅びに至る者が予め決められているとする（二重予定説）。神学的にはより広い聖定論に含まれ、その中の個人の救済に関わる事柄を指す。全的堕落と共にカルヴァン主義の根幹を成す。 予定説を支持する立場からは、予定説は聖書の教えであり正統教理とされるが、全キリスト教諸教派が予定説を認めている訳ではなく、予定説を認める教派の方がむしろ少数派である（後述）。.
形式的検証
形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。.
新しい！!: 時相論理と形式的検証 · 続きを見る »
作用素
数学における作用素（さようそ、operator）は、しばしば写像、函数、変換などの同義語として用いられる。函数解析学においては主にヒルベルト空間やバナッハ空間上の（必ずしも写像でない部分写像の意味での）線型変換を単に作用素と呼ぶ。そのような空間として特に函数空間と呼ばれる函数の成す無限次元線型空間は典型的であり（同じものを物理学の分野、特に量子力学などでは演算子（えんざんし）と呼ぶ）、このとき、作用素を関数を別の関数にうつす写像として理解することができる。数（定数関数）の集合に値をとる作用素は汎函数（はんかんすう、functional）と呼ばれる。 また、群や環が空間に作用しているとき、群や環の各元が定める空間上の変換、あるいはその変換が引き起こす関数空間上の変換のことを作用素ということがある。.
チャールズ・サンダース・パース
チャールズ・サンダース・パース（Charles Sanders Peirce、1839年9月10日 - 1914年4月19日）は、アメリカ合衆国の哲学者、論理学者、数学者、科学者であり、プラグマティズムの創始者として知られる。マサチューセッツ州ケンブリッジ生まれ。パースは化学者としての教育を受け、米国沿岸測量局に約三十年間、科学者として雇われていた。「アメリカ合衆国の哲学者たちの中で最も独創的かつ多才であり、そしてアメリカのもっとも偉大な論理学者」ともいわれる。存命中はおおむね無視されつづけ、第二次世界大戦後まで二次文献はわずかしかなかった。莫大な遺稿の全ては今も公表されていない。パースは自分をまず論理学者とみなし、さらに論理学を記号論（semiotics）の一分野とみなした。.
新しい！!: 時相論理とチャールズ・サンダース・パース · 続きを見る »
チョムスキー階層
チョムスキー階層（チョムスキーかいそう、Chomsky Hierarchy）は、形式言語を生成する形式文法の包含階層（「形式言語の階層」）で、「句構造文法（Phrase Structure Grammars）の階層」などとも言う。1956年にノーム・チョムスキーが発表した。.
新しい！!: 時相論理とチョムスキー階層 · 続きを見る »
命題論理
命題論理（propositional logic）とは、数理論理学（記号論理学）の基礎的な一部門であり、命題全体を1つの記号に置き換えて単純化し、論理演算を表す記号（論理記号・論理演算子）を用いて、その命題（記号）間の結合パターンを表現・研究・把握することを目的とした分野のこと。ブール論理はブール代数で形式化され2値の意味論を与えられた命題論理とみることができる。 命題を1つの記号で大まかに置き換える命題論理に対して、命題の述語（P）と主語（S）を、関数のF(x)のように別記号で表現し、更に量化子で主語（S）の数・量・範囲もいくらか表現し分けることを可能にした、すなわちより詳細に命題の内部構造を表現できるようにしたものを、述語論理と呼ぶ。.
アミール・プヌーリ
アミール・プヌーリ、ア（ー）ミール・ペヌーエーリー、アミル・ペヌエリ（אַמִיר(אָמִיר) פְּנוּאֵלִי a(ā)mīr pənū’ēlī; Amir Pnueli、1941年4月22日 - 2009年11月2日）は、イスラエル人の計算機科学者。.
新しい！!: 時相論理とアミール・プヌーリ · 続きを見る »
アリストテレス
アリストテレス（アリストテレース、Ἀριστοτέλης - 、Aristotelēs、前384年 - 前322年3月7日）は、古代ギリシアの哲学者である。 プラトンの弟子であり、ソクラテス、プラトンとともに、しばしば「西洋」最大の哲学者の一人とされ、その多岐にわたる自然研究の業績から「万学の祖」とも呼ばれる。特に動物に関する体系的な研究は古代世界では東西に類を見ない。イスラーム哲学や中世スコラ学、さらには近代哲学・論理学に多大な影響を与えた。また、マケドニア王アレクサンドロス3世（通称アレクサンドロス大王）の家庭教師であったことでも知られる。 アリストテレスは、人間の本性が「知を愛する」ことにあると考えた。ギリシャ語ではこれをフィロソフィア（）と呼ぶ。フィロは「愛する」、ソフィアは「知」を意味する。この言葉がヨーロッパの各国の言語で「哲学」を意味する言葉の語源となった。著作集は日本語版で17巻に及ぶが、内訳は形而上学、倫理学、論理学といった哲学関係のほか、政治学、宇宙論、天体学、自然学（物理学）、気象学、博物誌学的なものから分析的なもの、その他、生物学、詩学、演劇学、および現在でいう心理学なども含まれており多岐にわたる。アリストテレスはこれらをすべてフィロソフィアと呼んでいた。アリストテレスのいう「哲学」とは知的欲求を満たす知的行為そのものと、その行為の結果全体であり、現在の学問のほとんどが彼の「哲学」の範疇に含まれている立花隆『脳を究める』（2001年3月1日 朝日文庫）。 名前の由来はギリシア語の aristos （最高の）と telos （目的）から 。.
新しい！!: 時相論理とアリストテレス · 続きを見る »
アレン・エマーソン
アーネスト・アレン・エマーソン（Ernest Allen Emerson、1954年6月2日 - ）は、アメリカ合衆国の計算機科学者であり、テキサス大学オースティン校の教授。 エドムンド・クラーク、ジョセフ・シファキスと共にモデル検査の先駆的研究で2007年のチューリング賞を受賞した。1998年には、記号的モデル検査 (Symbolic Model Cheking) の研究に対してACMのパリス・カネラキス実践的理論賞を受賞した。 1976年、テキサス大学オースティン校で数学の学士号を取得し、1981年、ハーバード大学で応用数学の博士号を取得した。 1980年代にエドムンド・クラークと共同研究し、計算木論理を考案した。 ACMの会員である。.
新しい！!: 時相論理とアレン・エマーソン · 続きを見る »
アロンゾ・チャーチ
アロンゾ・チャーチ（Alonzo Church, 1903年6月14日 - 1995年8月11日）はアメリカの論理学者、数学者。ラムダ計算の創案者、「チャーチ＝チューリングのテーゼ」の提唱者として知られる。.
新しい！!: 時相論理とアロンゾ・チャーチ · 続きを見る »
エドムンド・クラーク
ドムンド・クラーク エドムンド・メルソン・クラーク・ジュニア（Edmund Melson Clarke, Jr.、1945年7月27日 - ）は、ハードウェアやソフトウェアの設計を形式的に検証するモデル検査の開発で知られている計算機科学者。カーネギーメロン大学計算機科学科の教授。アレン・エマーソン、ジョセフ・シファキスと共に、2007年のACMチューリング賞を受賞。.
新しい！!: 時相論理とエドムンド・クラーク · 続きを見る »
オートマトン
ートマトン (単数形: automaton, 複数形: オートマタ（automata ）) とは、自動人形などとも呼ばれる「オートマタ」と同じ語であるが、計算理論において、計算モデルに関して有限オートマトンなどの総称として使われる。また特に「オートマトン理論」と呼ばれる分野では、計算機械のうち計算可能性の点でチューリングマシンよりも制限されているものを特に指して言うこともある。.
新しい！!: 時相論理とオートマトン · 続きを見る »
オックスフォード大学
ックスフォード大学 (University of Oxford) は、イギリスの大学都市、オックスフォードに所在する総合大学である。11世紀の末に大学の礎が築かれていることから、現存する大学としては世界で3番目に古く、英語圏では最古の大学である。また、ハーバード大学、ケンブリッジ大学、シカゴ大学等と並び、各種の世界大学ランキングで常にトップレベルの優秀な大学として評価される世界有数の名門大学である。2016年、2017年THE世界大学ランキングで世界1位の大学に2年連続で選ばれた。 イギリス伝統のカレッジ制を特徴とする大学である。貴族の大学としても有名である。 世界中の指導的政治家を輩出しており、テリーザ・メイ現首相、デーヴィッド・キャメロン前首相、トニー・ブレア元首相、マーガレット・サッチャー元首相など27人のイギリス首相、30人以上の各国元首らがオックスフォード大学出身である。さらに、50人以上のノーベル賞受賞者、6人のイギリス国王、150人以上のオリンピックメダリストなどを輩出している。また、皇太子徳仁親王、皇太子妃雅子、秋篠宮文仁親王ら、日本の皇族の留学先としても知られている。 ちなみに「オックスブリッジ」として並び称されるケンブリッジ大学の形成は、この大学に所属していた多くの教師と学生が1209年にケンブリッジに移住したことに端を発する。.
新しい！!: 時相論理とオックスフォード大学 · 続きを見る »
ソール・クリプキ
ール・アーロン・クリプキ （Saul Aaron Kripke, 1940年12月13日 - ）は、アメリカ合衆国の哲学者・論理学者である。プリンストン大学名誉教授。ネブラスカ州オマハ生まれ。ユダヤ系アメリカ人。.
新しい！!: 時相論理とソール・クリプキ · 続きを見る »
状態遷移系
態遷移系（じょうたいせんいけい、State Transition System）とは、理論計算機科学での計算の研究に使用される抽象機械の一種。状態遷移系は状態群と状態間の遷移から構成される。 状態と遷移が有限個の状態遷移系は有向グラフで表すことができる。 また、状態遷移系は「ラベル付き」と「ラベル無し」の2種類に分類することができる。.
新しい！!: 時相論理と状態遷移系 · 続きを見る »
線形時相論理
線形時相論理（せんけいじそうろんり、Linear Temporal Logic、LTL）とは、時間に関する様相を持つ様相時相論理である。LTLでは、ある条件が最終的に真となるとか、別の事実が真になるまでその条件は真であるとかいった将来の出来事について論理式で表すことができる。.
新しい！!: 時相論理と線形時相論理 · 続きを見る »
真理関数
真理関数 （ しんりかんすう、Truth Function ） とは、数理論理学において、各変数の変域と終集合とがそれぞれ真な命題と偽な命題とだけから成る集合に等しいような写像である。真理関数は命題関数でもある。.
複雑性
複雑性（ふくざつせい、complexity）という用語は、多数の部品が入り組んで配置された何らかのものを特徴付ける言葉として使われる。科学として複雑性を研究するアプローチはいくつか存在しており、本項目ではそれらを概説する。マサチューセッツ工科大学のセス・ロイドは、複雑性の定義を32種類集めてプレゼンテーションしたことがあるという。.
計算機科学
計算機科学（けいさんきかがく、computer science、コンピュータ科学）とは、情報と計算の理論的基礎、及びそのコンピュータ上への実装と応用に関する研究分野である。計算機科学には様々な下位領域がある。コンピュータグラフィックスのように特定の処理に集中する領域もあれば、計算理論のように数学的な理論に関する領域もある。またある領域は計算の実装を試みることに集中している。例えば、プログラミング言語理論は計算を記述する手法に関する学問領域であり、プログラミングは特定のプログラミング言語を使って問題を解決する領域である。.
新しい！!: 時相論理と計算機科学 · 続きを見る »
計算木論理
計算木論理（けいさんきろんり、Computational Tree Logic、CTL）は、分岐時相論理の一種である。その時間モデルでは未来は決定されておらず木構造のように分岐している。未来の複数の経路のうちの1つが実際に現実の経路となる。.
新しい！!: 時相論理と計算木論理 · 続きを見る »
論理学
論理学（ろんりがく、）とは、「論理」を成り立たせる論証の構成やその体系を研究する学問である。.
論理演算
論理演算（ろんりえんざん、logical operation）は、論理式において、論理演算子などで表現される論理関数（ブール関数）を評価し（正確には、関数適用を評価し）、変数（変項）さらには論理式全体の値を求める演算である。 非古典論理など他にも多くの論理の体系があるが、ここでは古典論理のうちの命題論理、特にそれを形式化したブール論理に話を絞る。従って対象がとる値は真理値の2値のみに限られる。また、その真理値の集合（真理値集合）と演算（演算子）はブール代数を構成する。 コンピュータのプロセッサやプログラミング言語で多用されるものに、ブーリアン型を対象とした通常の論理演算の他に、ワード等のビット毎に論理演算を行なう演算があり、ビット演算という。 なお、以上はモデル論的な議論であり、証明論的には、公理と推論規則に従って論理式を変形（書き換え）する演算がある（証明論#証明計算の種類）。.
自由意志
自由意志（じゆういし、free will、freier Wille、libre arbitre、liberum arbitrium）とは、他から束縛されず自らの責任において決定する意思。言い換えれば、行為者の自由な意志のこと。.
Property Specification Language
Property Specification Language（特性仕様言語、PSL と略記）とは、ハードウェア設計におけるプロパティ（特性）や表明を記述する言語として標準化団体 Accelleraが開発したものである。これにより、プロパティをシミュレートしたり形式的に検証したりできる。2004年9月から、IEEE 1850 ワーキンググループがこの標準化を行ってきた。2005年9月、IEEE 1850 Standard for Property Specification Language (PSL) が発表された。 Property Specification Language は以下のような複数のハードウェア記述言語で使われることを目指している.
新しい！!: 時相論理とProperty Specification Language · 続きを見る »
Well-formed formula
数理論理学において well-formed formula（wff、整式などとも）とは、形式言語といったような概念が広まる以前に、"formula" を単なる「記号を任意の順序に並べたもの」であるとして、それらのうち、数式などとして意味をなすような記号列を特に区別したものである。形式言語の考え方が広まるにつれ、そもそも意味のある数式などは何らかのルールに従って導出されるもので、それ以外の、任意の順序に並べたようなものは最初から議論の対象外として扱われるのが普通となった。.
新しい！!: 時相論理とWell-formed formula · 続きを見る »
様相論理
様相論理（ようそうろんり、modal logic）は、いわゆる古典論理の対象でない、様相（modal）と呼ばれる「〜は必然的に真」や「〜は可能である」といった必然性や可能性などを扱う論理である（様相論理は、部分の真理値からは全体の真理値が決定されない内包論理の一種と見ることができる）。 その歴史は古くアリストテレスまで遡ることができるが、形式的な扱いは数理論理学以降、非古典論理としてである。 様相論理では一般に、標準的な論理体系に「～は必然的である」ことを意味する必然性演算子 \Box と、「～は可能である」ことを意味する可能性演算子 \Diamond のふたつの演算子が追加される。.
時間
人類にとって、もともとは太陽や月の動きが時間そのものであった。 アイ・ハヌム（紀元前4世紀～紀元前1世紀の古代都市）で使われていた日時計。人々は日時計の時間で生きていた。 砂時計で砂の流れを利用して時間を計ることも行われるようになった。また砂時計は、現在というものが未来と過去の間にあることを象徴している。くびれた部分（現在）を見つめる。すると時間というのは上（未来）から流れてきて下（過去）へと流れてゆく流れ、と感じられることになる。 時間（じかん）は、出来事や変化を認識するための基礎的な概念である。芸術、哲学、自然科学、心理学などの重要なテーマとなっている。それぞれの分野で異なった定義がなされる。.
1950年代
1950年代（せんきゅうひゃくごじゅうねんだい）は、西暦（グレゴリオ暦）1950年から1959年までの10年間を指す十年紀。この項目では、国際的な視点に基づいた1950年代について記載する。.
新しい！!: 時相論理と1950年代 · 続きを見る »
ここにリダイレクトされます：
時制論理。
