Tento článek potřebuje úpravy.

Můžete Wikipedii pomoci tím, že ho vylepšíte. Jak by měly články vypadat, popisují stránky Vzhled a styl, Encyklopedický styl a Odkazy.

---

Konkrétní problémy: v podstatě celé neověřeno - chybí řádkové citace, poznámky a literatura jsou zpracovány newikipedickým způsobem

Temporální logika je široké spektrum formálních systémů, jejichž společným cílem je formalizovat a analyzovat věty obsahující časové (temporální) komponenty jako někdy, vždy či dokud. Kromě původních, spíše lingvistických a filosofických motivací nachází temporální logika od poslední třetiny dvacátého století uplatnění i v informatice a umělé inteligenci.

Úvod

Temporální logika má svůj počátek v díle Arthura Priora.^{[pozn. 1]} Jak už naznačuje její název, jde o formální vědu zabývající se studiem modelů času. Jejím cílem není odhalit ty charakteristiky, které „skutečně" času náleží, naopak podobně jako jiná odvětví matematické logiky ji lze spíše chápat jako nástroj na popis a zpřehlednění struktur, které si s během času a problémem jeho zachycení lze představit. Oproti běžnému úzu ve studiu modálních logik postupoval historický vývoj jednotlivých temporálních logik od zamýšlených interpretací (modelů, struktur) k formálním systémům, a nikoli naopak.

Z hlediska času jako takového nachází temporální logika uplatnění například ve filosofických diskuzích.^{[pozn. 2]} Už však motivace jejího vzniku byly především lingvistického rázu,^{[pozn. 3]} totiž objasnit strukturu temporálních forem přirozeného jazyka, případně nabídnout pro tyto formy adekvátní sémantiku. To se například týká temporálních adverbií nebo slovesných časů. Na konci šedesátých a v sedmdesátých letech dvacátého století se začaly objevovat aplikace některých systémů v oblasti umělé inteligence^{[pozn. 4]} a v informatice.^{[pozn. 5]} To vedlo k dalšímu rozšiřování již tak velkého množství různých teorií co do šířky (například obohacování syntaxe), hloubky (studium logických vlastností jako úplnost, rozhodnutelnost, definovatelnost, kvantitativní aspekty) a spektra záběru.

Priorova výroková temporální logika TL

Výrokovou verzi Minimální temporální logiky ${\displaystyle K_{t}}$ lze syntakticky chápat jako rozšíření klasické výrokové logiky KVL o dva unární modální operátory ${\displaystyle G}$ a ${\displaystyle H}$. Interpretace výroku ${\displaystyle Gp}$ je „vždy v budoucnosti p”, interpretace ${\displaystyle Hp}$ je „vždy v minulosti p”. Podobně jako v modální logice s operátorem ${\displaystyle \Box }$ mají i ${\displaystyle G}$ a ${\displaystyle H}$ svoje duální verze ${\displaystyle F}$ a ${\displaystyle P}$, „někdy v budoucnosti” a „někdy v minulosti”.^[1] Ze sémantického hlediska lze ${\displaystyle K_{t}}$ také chápat jako zjemnění KVL, totiž tak, že hodnota formule ${\displaystyle \varphi }$ se relativizuje vzhledem k časovému okamžiku ${\displaystyle t}$. Sémantika klasické logiky je v sémantice ${\displaystyle K_{t}}$ zahrnuta v tom smyslu, že čistě výrokové formule, které neobsahují temporální operátory, se vyhodnocují lokálně.

Syntax a sémantika

Nechť ${\displaystyle L_{t}}$ značí jazyk KVL obohacený o operátory ${\displaystyle G}$ a ${\displaystyle H}$. Jejich duály ${\displaystyle P}$ a ${\displaystyle F}$ jsou definovány následovně:

${\displaystyle {\begin{aligned}P\varphi &\equiv \neg H\neg \varphi \\F\varphi &\equiv \neg G\neg \varphi \end{aligned}}}$

Interpretaci formulí ${\displaystyle L_{t}}$ tvoří standardní sémantika modálních logik, kripkovské rámce, které se v temporální logice nazývají časové rámce. Jde o dvojici ${\displaystyle (T,R)}$, z níž ${\displaystyle T}$ je neprázdná množina časových okamžiků a ${\displaystyle R}$ je binární relace, intuitivně ${\displaystyle R(t_{1},t_{2})}$ značí tvrzení „${\displaystyle t_{2}}$ následuje po ${\displaystyle t_{1}}$”.

Pro temporální logiku je tedy zamýšlená interpretace relace ${\displaystyle R}$ ostré (částečné) uspořádání ${\displaystyle <}$, u minimální logiky ${\displaystyle K_{t}}$ se však na ${\displaystyle R}$ žádná omezení nekladou. Ohodnocení proměnných je funkce ${\displaystyle e:(Var,T)\rightarrow \{0,1\}}$, tedy každé dvojici ${\displaystyle (atom,vrchol)}$ se přiřadí hodnota True ci False. Model ${\displaystyle M}$ nad rámcem ${\displaystyle (T,R)}$ je trojice ${\displaystyle (T,R,e)}$ pro nějaké ${\displaystyle e}$.

Formální sémantiku temporálních operátorů tvoří následující dvě klauze (hodnota formule se počítá vůči modelu ${\displaystyle M}$ a vrcholu ${\displaystyle t}$):

${\displaystyle {\begin{aligned}M,t\models H\varphi \ \Leftrightarrow \ \forall t'&<t\ (M,t'\models \varphi )\\M,t\models G\varphi \ \Leftrightarrow \ \forall t'&>t\ (M,t'\models \varphi )\end{aligned}}}$

Tvrzení ${\displaystyle M,t\models \varphi }$ značí, že ${\displaystyle \varphi }$ je splněna v ${\displaystyle t}$ ohodnocením ${\displaystyle e}$. Definice platnosti v modelu, rámci a třídě rámců je následující: ${\displaystyle \varphi }$ platí v ${\displaystyle M}$ právě tehdy, když ${\displaystyle \varphi }$ je splněna v každém ${\displaystyle t}$, formule ${\displaystyle \varphi }$ platí v ${\displaystyle T}$ právě tehdy, když ${\displaystyle \varphi }$ platí v každém modelu nad ${\displaystyle T}$, a formule ${\displaystyle \varphi }$ platí ve třídě rámců ${\displaystyle C}$ právě tehdy, když ${\displaystyle \varphi }$ platí v každém ${\displaystyle T\in C}$.

Definovatelnost

Definice platnosti ve třídě časových rámců umožňuje zkoumat, které třídy rámců jsou „vydělitelné" pomocí některé formule ${\displaystyle L_{t}}$, případně porovnávat expresivitu jazyka prvořádové logiky a jazyka ${\displaystyle L_{t}}$ logiky temporální. Temporální formule ${\displaystyle \varphi }$ definuje (charakterizuje) třídu rámců ${\displaystyle C}$, pokud ${\displaystyle \varphi }$ platí právě v každém rámci ${\displaystyle T}$ ve třídě ${\displaystyle C}$. Lze se například ptát, zda existují temporální formule charakterizující částečně uspořádané rámce, lineární rámce, hustě uspořádané lineární rámce, diskrétně uspořádané lineární rámce (jednoznačný následník a předchůdce každého bodu), shora neomezené rámce (každý bod má následníka), dobře uspořádané rámce, úplně uspořádané rámce, a další. Existují prvořádové vlastnosti, které nejsou vyjádřitelné temporální formulí. Jako příklady lze vzít antireflexivitu a antisymetrii. Na druhou stranu existují i vlastnosti rámců definovatelné temporální formulí, které nejsou vyjádřitelné jazykem prvořádové logiky. Důležité příklady jsou spojitost a dobré uspořádání.^[2]

Standardní překlad, axiomatizace, úplnost

Nechť ${\displaystyle L_{t}=\{\neg ,\wedge ,H,G,\bot \}}$. Minimální logiku ${\displaystyle K_{t}}$ lze přeložit do klasické predikátové logiky s rovností. Nechť její jazyk ${\displaystyle L_{p}}$ obsahuje jeden binární predikát ${\displaystyle R}$ a spočetně mnoho unárních predikátů ${\displaystyle P_{1},P_{2},P_{3},\dots }$ Potom lze nadefinovat standardní překlad ${\displaystyle sp}$ z jazyka ${\displaystyle L_{t}}$ do ${\displaystyle L_{p}}$ následovně:

${\displaystyle {\begin{aligned}sp(p_{i})&=P_{i}(x)\\sp(\bot )&=\bot \\sp(\neg \varphi )&=\neg sp(\varphi )\\sp(\varphi \wedge \psi )&=sp(\varphi )\wedge sp(\psi )\\sp(H\varphi )&=\forall y(yRx)\rightarrow st(\varphi _{y}(x))\\sp(G\varphi )&=\forall y(xRy)\rightarrow st(\varphi _{y}(x))\end{aligned}}}$

Proměnná ${\displaystyle x}$ symbolizuje aktuální stav věcí (přítomnost) a zápis ${\displaystyle \varphi _{y}(x)}$ značí substituci proměnné ${\displaystyle x}$ za všechny volné výskyty ${\displaystyle y}$ ve ${\displaystyle \varphi }$. Tímto způsobem lze každou formuli temporálního jazyka ${\displaystyle L_{t}}$ přeložit do prvořádové logiky.^[3] Ačkoli je studium temporálních logik primárně motivováno strukturami zamýšlenými k popisu, například přirozenými ${\displaystyle \mathbb {N} }$ či racionálními ${\displaystyle \mathbb {Q} }$ čísly, jako u všech ostatních logik je k dispozici i deduktivní (axiomatická) stránka. Minimální temporální logika ${\displaystyle K_{t}}$ má kromě vhodných výrokových axiomů následující dvě temporální obdoby modálního axiomu ${\displaystyle K}$, dva axiomy stanovující dualitu operátorů ${\displaystyle G}$ a ${\displaystyle H}$, a nakonec tranzitivitu ${\displaystyle G}$ (a tedy i ${\displaystyle H}$):

Zdroj:
>Text je dostupný pod licencí Creative Commons Uveďte autora – Zachovejte licenci, případně za dalších podmínek. Podrobnosti naleznete na stránce Podmínky užití.

---