temporal logicとは? わかりやすく解説

Weblio 辞書 > 辞書・百科事典 > 百科事典 > temporal logicの意味・解説 

時相論理

(temporal logic から転送)

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2019/01/02 21:06 UTC 版)

ナビゲーションに移動 検索に移動

時相論理(Temporal Logic)とは、時間との関連で問題を理解し表現するための規則と表記法の体系である。時相論理では、「私はいつも腹ペコだ」、「私はそのうち腹ペコになる」、「私は何かを食べるまで腹ペコだろう」といった文を表現できる。1950年代末にアーサー・プライアー英語版が提唱した様相論理に基づいた時相論理を特に時制論理(Tense Logic)と呼ぶことがある。ハンス・カンプ英語版が重要な業績を残した。その後、そこから発展し、アミール・プヌーリ計算機科学者や論理学者が研究を進めた。

時相論理はシステムのハードウェアやソフトウェアの要求仕様を記述する方法として形式的検証で利用される。例えば、「要求が発生したら常にリソースへのアクセスがそのうちに承認される。ただし、決して2つの要求を同時に承認してはならない」といった文章は時相論理で表せる。

概要

「私は腹ペコだ」という文を考えてみよう。この文の意味は時間経過に関わらず一定であるが、その真偽は時間経過によって変化する。あるときは真だし、またあるときは偽である。しかし、同時に真でもあり偽でもあるということはありえない。時相論理では、時と共に真理値の変化する文を扱う。非時相論理では、時間経過によって真理値が変化しない文しか扱えない。

時相論理は常に時系列について判断する能力を有する。線形時間論理(Linear Time Logic)と呼ばれるものはこの種の推論に限定されている。分岐論理(Branching Logic)は複数の時系列を判断できる。これは予測不能な挙動を示す環境を前提とする。さらに言えば、分岐論理では「私が永遠に腹ペコのままでいる可能性がある」といった文が表現可能である。他にも「私がもう腹ペコではなくなる可能性がある」という文も表現可能である。「私」が食べ物にありつけるかどうか不明ならば、これらの文はどちらも真である。

歴史

アリストテレスは主に三段論法を研究したが、現代の時相論理のような研究もしており、一階時相二値論理のような形式を部分的に検討したことがある。特に不確定な未来の事象を扱う際、アリストテレスは二値の意味論を適用できないと考え、例えば「明日、海戦が勃発するだろう」といった文の真偽を現時点で決定できないとした[1]

その後数千年間、ほとんど発展は見られなかった。19世紀、チャールズ・サンダース・パースは次のように記している。

時間は、論理学者にとって論理外のものとみなされてきた。私は決してこの意見に与しない。しかし論理学はそこまでの状態に達しておらず、今の論理を時相を扱えるよう修正すれば大きな混乱を生じるであろう。私の思考もまだその段階に達していない。

アーサー・プライアー英語版自由意志予定説といった哲学的問題を検討した。彼の妻によれば、彼が最初に時相論理を定式化したのは1953年のことだという。1955年から56年にかけてオックスフォード大学でそれについて講義をし、1957年には Time and Modality を出版。その中で2つの時相接続子(様相作用素英語版)F(「未来のいずれかの時点で」の意)とP(「過去のいずれかの時点で」の意)を備えた命題様相論理を説明している。この先駆的取り組みで、プライアーは時間を線型なものとみなしている。しかし1958年、ソール・クリプキはプライアーへの手紙で、その仮定は不当だと指摘した。計算機科学での同様な考え方を予示しつつ、プライアーは熟慮の上それを採用し2つの分岐時間の理論を考案、"Ockhamist" と "Peircean" と名付けた[2][要説明]。1958年から1965年にかけて、プライアーは Charles Leonard Hamblin と共同で時相論理について研究した。1967年、時相論理に関する研究の集大成として Past, Present, and Future を出版。その2年後に亡くなった[3]

ハンス・カンプ英語版は1968年の博士論文で二値の時相作用素 SinceUntil を導入し[4]、その論文で時相論理と一階述語論理を関連付ける重要な考察も行い、それが「カンプの定理」と呼ばれるようになった[5][2][6]

形式的検証では、線形時相論理アミール・プヌーリによる線形時間論理の一種)と計算木論理エドムンド・クラークアレン・エマーソンによる分岐時間論理の一種)が競っている。後者のほうが分岐を扱えるぶんだけ前者よりも効果的であると指摘されることがある。エマーソンと Lei は、いかなる線形論理も複雑性を変えずに分岐論理に拡張可能であることを示した。

時相作用素

時相論理では2種類の作用素を使用する。論理作用素様相作用素英語版である[1]。論理作用素は一般的な真理関数作用素である(

単項演算 N
F
G
A カテゴリ - 関係記事更新

辞典・百科事典の検索サービス - Weblio辞書辞典・百科事典の検索サービス - Weblio辞書

「Temporal logic」の例文・使い方・用例・文例

Weblio日本語例文用例辞書はプログラムで機械的に例文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。


英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  

辞書ショートカット

カテゴリ一覧

すべての辞書の索引



Weblioのサービス

「temporal logic」の関連用語





5
18% |||||






temporal logicのお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



temporal logicのページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
All text is available under the terms of the GNU Free Documentation License.
この記事は、ウィキペディアの時相論理 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。
Tanaka Corpusのコンテンツは、特に明示されている場合を除いて、次のライセンスに従います:
 Creative Commons Attribution (CC-BY) 2.0 France.
この対訳データはCreative Commons Attribution 3.0 Unportedでライセンスされています。
浜島書店 Catch a Wave
Copyright © 1995-2025 Hamajima Shoten, Publishers. All rights reserved.
株式会社ベネッセコーポレーション株式会社ベネッセコーポレーション
Copyright © Benesse Holdings, Inc. All rights reserved.
研究社研究社
Copyright (c) 1995-2025 Kenkyusha Co., Ltd. All rights reserved.
日本語WordNet日本語WordNet
日本語ワードネット1.1版 (C) 情報通信研究機構, 2009-2010 License All rights reserved.
WordNet 3.0 Copyright 2006 by Princeton University. All rights reserved. License
日外アソシエーツ株式会社日外アソシエーツ株式会社
Copyright (C) 1994- Nichigai Associates, Inc., All rights reserved.
「斎藤和英大辞典」斎藤秀三郎著、日外アソシエーツ辞書編集部編
EDRDGEDRDG
This page uses the JMdict dictionary files. These files are the property of the Electronic Dictionary Research and Development Group, and are used in conformance with the Group's licence.

©2025 GRAS Group, Inc.RSS