時相論理（Temporal Logic）とは、時間との関連で問題を理解し表現するための規則と表記法の体系である。時相論理では、「私はいつも腹ペコだ」、「私はそのうち腹ペコになる」、「私は何かを食べるまで腹ペコだろう」といった文を表現できる。1950年代末にが提唱した様相論理に基づいた時相論理を特に時制論理（Tense Logic）と呼ぶことがある。が重要な業績を残した。その後、そこから発展し、アミール・プヌーリら計算機科学者や論理学者が研究を進めた。時相論理はシステムのハードウェアやソフトウェアの要求仕様を記述する方法として形式的検証で利用される。例えば、「要求が発生したら常にリソースへのアクセスがそのうちに承認される。ただし、決して2つの要求を同時に承認してはならない」といった文章は時相論理で表せる。「私は腹ペコだ」という文を考えてみよう。この文の意味は時間経過に関わらず一定であるが、その真偽は時間経過によって変化する。あるときは真だし、またあるときは偽である。しかし、同時に真でもあり偽でもあるということはありえない。時相論理では、時と共に真理値の変化する文を扱う。非時相論理では、時間経過によって真理値が変化しない文しか扱えない。時相論理は常に時系列について判断する能力を有する。線形時間論理（Linear Time Logic）と呼ばれるものはこの種の推論に限定されている。分岐論理（Branching Logic）は複数の時系列を判断できる。これは予測不能な挙動を示す環境を前提とする。さらに言えば、分岐論理では「私が永遠に腹ペコのままでいる可能性がある」といった文が表現可能である。他にも「私がもう腹ペコではなくなる可能性がある」という文も表現可能である。「私」が食べ物にありつけるかどうか不明ならば、これらの文はどちらも真である。アリストテレスは主に三段論法を研究したが、現代の時相論理のような研究もしており、一階時相二値論理のような形式を部分的に検討したことがある。特に不確定な未来の事象を扱う際、アリストテレスは二値の意味論を適用できないと考え、例えば「明日、海戦が勃発するだろう」といった文の真偽を現時点で決定できないとした。その後数千年間、ほとんど発展は見られなかった。19世紀、チャールズ・サンダース・パースは次のように記している。は自由意志や予定説といった哲学的問題を検討した。彼の妻によれば、彼が最初に時相論理を定式化したのは1953年のことだという。1955年から56年にかけてオックスフォード大学でそれについて講義をし、1957年には "Time and Modality" を出版。その中で2つの時相接続子（）F（「未来のいずれかの時点で」の意）とP（「過去のいずれかの時点で」の意）を備えた命題様相論理を説明している。この先駆的取り組みで、プライアーは時間を線型なものとみなしている。しかし1958年、ソール・クリプキはプライアーへの手紙で、その仮定は不当だと指摘した。計算機科学での同様な考え方を予示しつつ、プライアーは熟慮の上それを採用し2つの分岐時間の理論を考案、"Ockhamist" と "Peircean" と名付けた。1958年から1965年にかけて、プライアーは と共同で時相論理について研究した。1967年、時相論理に関する研究の集大成として "Past, Present, and Future" を出版。その2年後に亡くなった。は1968年の博士論文で二値の時相作用素 "Since" と "Until" を導入し、その論文で時相論理と一階述語論理を関連付ける重要な考察も行い、それが「カンプの定理」と呼ばれるようになった。形式的検証では、線形時相論理（アミール・プヌーリによる線形時間論理の一種）と計算木論理（エドムンド・クラークとアレン・エマーソンによる分岐時間論理の一種）が競っている。後者のほうが分岐を扱えるぶんだけ前者よりも効果的であると指摘されることがある。エマーソンと Lei は、いかなる線形論理も複雑性を変えずに分岐論理に拡張可能であることを示した。時相論理では2種類の作用素を使用する。論理作用素とである。論理作用素は一般的な真理関数作用素である(formula_1)。線形時相論理や計算木論理で使用される様相作用素を以下に示す。他の表現:B(formula_4) が整論理式(wff)であれば、単項作用素は全て整論理式である。B(formula_4) と C(formula_4) が整論理式であれば、二項作用素は全て整論理式である。論理体系によっては一部の作用素は表現できない。例えば、 では N 作用素は表現できない。時相論理と密接に関連する論理として、トポロジーや場所や空間的位置を扱う様相論理がある。

出典:wikipedia