線形論理

きっかけ

直観主義論理, 古典論理と並ぶ論理体系の一種

A: 「私は110円持っている」

B: 「私は110円のコーラを買える」

C: 「私は110円のチョコレートを買える」

このとき $A \to B \land A \to C$ なので通常の論理だと $A \to (B \land C)$

「110円持っていればコーラも買えてかつチョコレートも買える」

議論:

X: 「コーラもチョコレートも好きな方を買えるので “かつ” は正しい」(どちらも好きな方を成立できる)

Y: 「どっちかを買ったらお金はなくなるのでどちらも買えるは間違い」(同時に成立する)

含意も $\to$ ではなく違う記号-oで表し, 前者のかつを &, 後者を ^ で表すと

X: $A - o (B & C)$

Y: $A - o (B \land C)$

線形論理は限りあるリソースを表現できるとしてコンピュータサイエンスで注目されて並行分散処理とかで注目された.

tags	math/logic
aliases	Linear Temporal Logic, LTL