백과

명제의 진위가 시간에 의존하는 논리. 상황논리의 일종으로 위치시킨다. 통상의 논리연산 이외에 시상연산자(temporal operator)가 이용된다. 연산자로서는 F, P가 기본이다. 이들 연산자의 직관적인 의미는 A를 임의의 논리식으로서 FA : 미래의 어떤 시점에서 A가 참이다, PA : 과거의 어떤 시점에서 A가 참이다라고 해석된다. 이들을 이용해 GA≡-F-A : 미래의 모든 시점에서 A가 참이다, HA≡-P-A : 과거의 모든 시점에서 A가 참이다, □A≡GA∧HA∧A : 항상 A가 참이다, ◇A≡-□-A : 언젠가는 A가 참이다. 등의 연산을 도입할 수 있다.

시상논리의 해석은 시점 t를 파라미터로서 주어지는 것을 없애는 통상의 논리와 같다. 시점 t의 집합 T+의 구조, 즉 시간 사이의 순서관계 R(t, t’)이 시상연산자의 의미를 결정하므로 기본적인 역할을 한다. 순서관계 R(t, t’)에 제약을 부과하는 것에 의해서 시간추이의 관계가 정해지고 그것에 대응하는 시상논리가 구성된다. 시간추이의 성질로서는

추이성(transitivity) :
∀t∀s∀r(R(t, s)∧R(s, r)→R(t, r))

후방선형성(backward linearity) :
∀t∀s∀r(R(t, r)∧R(s, r)→R(t, s)∨(t=s)∨R(s, t))

전방선형성(forward linearity) :
∀s∀t∀r(R(r, t)∧R(r, s)→R(s, t)∨(s=t)∨R(t, s))

이외에 편방향무한성, 양방향무한성, 이산성, 조밀성, 연속성 등이 있다. 시상논리는 시공간 개념을 수반하는 추론, 병행 프로그램의 수단기술, 검증 등으로 응용되고 있다.