Темпоральная логика

---

Темпоральная логика (временна́я логика; англ. temporal logic) — логика, в высказываниях которой учитывается временной аспект. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале.

В древности применение логики во временно́м аспекте изучали философы мегарской школы, в частности Диодор Крон, и стоики. Современная символическая темпоральная логика, впервые концептуализированная и сформулированная в 1950-е годы Артуром Прайором^[en][1] на основе модальной логики, наибольшее распространение и развитие получила в информатике благодаря трудам лауреата Тьюринговской премии Амира Пнуэли.

Смысл утверждения «я голоден» не меняется со временем, однако его истинность может измениться: в конкретный момент времени оно может быть истинным, либо ложным, но не одновременно. В противоположность нетемпоральным логикам, где значения утверждений не меняются со временем, в темпоральной логике значение зависит от того, когда оно проверяется. Темпоральная логика позволяет выразить утверждения типа «я всегда голоден», «я иногда голоден» или «Я голоден, пока я не поем».

В темпоральных логиках бывает два вида операторов: логические и модальные. В качестве логических операторов обычно используются (${\displaystyle \neg ,\lor ,\land ,\rightarrow }$). Модальные операторы, используемые в логике линейного времени и логике деревьев вычислений, определяются следующим образом.

${\displaystyle \phi }$ V ${\displaystyle \psi }$

${\displaystyle \phi ~{\mathcal {V}}~\psi }$

---