시간 논리

논리학에서 시간 논리(時間論里, temporal logic)는 시간의 개념을 나타낼 수 있는 논리 체계를 이르는 말이다. 특히 시제 논리(時制論里, tense logic)라 하면 양상 논리를 기반으로 한 시간 논리를 가리키는 말로, 선형 시제 논리와 계산 트리 논리 등이 알려져 있으며 컴퓨터 과학 분야에서 중요하게 응용되고 있다.

Prior의 시제 논리 (TL)

Arthur Prior가 1950년대에 저서 Time and Modality에서 처음 도입한 시제 논리 체계에는 일반적 1차 논리 연산자에 더하여 다음의 4가지 양상 연산자가 더해졌다.

• P a: "과거의 어떤 시점에 a 라는 일이 있었다"
• F a: "미래의 어떤 시점에 a 라는 일이 있을 것이다"
• G a: "미래의 모든 시점에 a 라는 일이 있을 것이다"
• H a: "과거의 모든 시점에 a 라는 일이 있었다"

다음과 같이 P와 F로부터 G와 H가 도출될 수 있고, 그 역도 그러하다:

${\begin{aligned}F&\equiv \lnot G\lnot \\P&\equiv \lnot H\lnot \end{aligned}}$

같이 보기

• 선형 시제 논리
• 양상 논리
• 시간