Logika temporalna

Logika temporalna – logika umożliwiająca rozważanie zależności czasowych bez wprowadzania czasu explicite. Pierwotnie służyła jako narzędzie do filozoficznych rozważań nad naturą czasu, dzisiaj jest używana głównie w informatyce. Czas można wprowadzić do zwykłego rachunku predykatów pierwszego rzędu.Np. aby powiedzieć, że zawsze, kiedy jedzie pociąg, szlaban musi być opuszczony (żeby uniknąć wypadku), oraz że dla każdej chwili szlaban kiedyś się podniesie (aby samochody mogły w końcu przejechać), możemy napisać: Dowodzenie twierdzeń w tak ogólnej notacji może być jednak trudne. Z tego powodu dodaje się do rachunku zdań bez kwantyfikatorów pewne operatory modalne. Brak kwantyfikatorów umożliwia nam łatwe dowodzenie twierdzeń, zaś operatory modalne umożliwiają nam rozważanie zależności czasowych. Logik temporalnych jest wiele. Można je jednak podzielić na dwie grupy – te, które zakładają liniową strukturę czasu, oraz te, które zakładają rozgałęzioną strukturę czasu. Logiki temporalne zazwyczaj operują czasem składającym się z wydarzeń dyskretnych, choć możliwe są też logiki używające czasu ciągłego.