Главная страница Случайная страница
КАТЕГОРИИ:
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника
Tt′ A
|
|
читается так: если событие А всегда будет в некоторый момент времени t, то оно будет в любой будущий момент времени t′, достижимый из t (то есть если tRt′).
II. FG. Ft GA
Ft′ A
читается: так: если ложно, что событие А всегда будет в момент времени t, то А будет ложным хотя бы в один момент времени t′ в будущем, достижимый из t (то есть если tRt′), причем t′ не встречался в предыдущих строках той ветви таблицы, где применяется правило FG.
III. TH. Tt HA
Tt′ A
читается так: если событие А всегда было в момент времени t, то оно было в любой момент времени t′ в прошлом, достижимый из t (то есть если tRt′).
IV. FH Ft HA
Ft′ A
читается так: если ложно, что событие А всегда было в момент времени t, то А ложно хотя бы в один момент времени t′ в прошлом, такой, что (tRt′), причем t′ не встречался в предыдущих строках той ветви таблицы, где применяется правило FH.
V. TF Tt FA
Tt′ A
читается так: если событие А произойдет в некоторый момент времени t, то А будет истинным хотя бы в один момент времени t′ в будущем такой, что (tRt′), причем t′ не встречается в предыдущих строках ветви таблицы, в которой применяется правило TF.
VI. FF. Ft FA
Ft′ A
читается так: если событие А не произойдет в некоторый момент времени t, то А будет ложным в любой момент времени в будущем такой, что (tRt′).
VII. TP. Tt PA
Tt′ A
читается так: если событие А происходило в некоторый момент времени t, то А было истинным хотя бы в один предыдущий момент времени t′ такой, что ( tRt´), причем t´ не встречается в предыдущих строках ветви таблицы, в которой применяется правило TP.
VIII. FP Ft PA
Ft′ A
читается так: если событие А не происходило в некоторый момент времени t, то А было ложным в любой предшествующий момент времени t′ такой, что ( tRt′).
С помощью приведенных правил можно построить аналитические таблицы для любых формул темпоральной логики с целью определения их семантического статуса.
Обратимся к иллюстрации.
Пусть имеется формула p É GPp.
Построив для нее аналитическую таблицу, определим, является он логическим законом, противоречием или выполнимой.
0. F (p É GPp)
I 1. Tt p
2. Ft GPp 0, FÉ
II 3. Ft´ Pp 2, FG
III 4. Ft p 3, FP
+
Таким образом, данная формула является логическим законом темпоральной огики.