|
Dl • множество временных умолчаний вида (3.31); F1 = Rules 4 Events, где Rules и Events непересекающиеся множества формул TLC, такие, что формулы, входящие в множество Rules, имеют вид А 1 В, где А и В любые замкнутые формулы TLC, а формулы, входящие в множество Events, имеют вид first next [n] р (e i,..., е^), где п • натуральное число, меньшее или равное числу моментов времени на часах формулы p(ej, ... , е*), если эти часы являются конечной последовательностью натуральных чисел; р • k-местный предикатный символ; еь ..., е^ • термы, не имеющие вхождений индивидных переменных. По терминологии TLC формулы такого вида называются атомарными событиями (р (el, ..., ek) “чистый временной атом”) и относятся к классу т.н. формул фиксированного времени (fixed-time formula), т.е. формул, значения которых зависят ровно от одного момента времени. Значение формулы first next [п] А для любого момента времени на её локальных часах ска равно значению формулы А для момента времени, соответствующему пму элементу скл. Расширение временной теории с умолчаниями определим следующим образом. Пусть L n c язык логики TLC, X подмножество из L uc >Th1 ( X ) множество замкнутых формул, выводимых из X с использованием аксиом и правил вывода логики TLC при конкретном присваивании часов ск: Th1 ( X ) = {w w Jfr Ljlc , w замкнута и X w }. Пусть g i' = <Р, ck, D1, FT>временная теория с умолчаниями, S В Luc* Обозначим через jb'(S) наименьшее подмножество множества Ltlc> удовлетворяющее следующим условиям: 1)Fl П a l(S), 2 )T ht 3) если * D1, Л 1 £ '(S ) в и s, то в ъ a l(s). 161 |
а подстановка вида {е/х}, где е индивидная константа. Если формулы А и В не имеют вхождений свободной переменной (т.е. они замкнутые), то тогда ст= 0 . Далее, временную теорию с умолчаниями определим как четверку: Д*= <Р, ck, D', F*>, (3.4) где Р множество всех предикатных символов, встречающихся в элементах множеств D' и F1 ; ck присваивание часов, т.е. отображение из множества Р в множество всех часов СК, являющееся множеством всех подпоследовательностей последовательности натуральных чисел; D1 множество временных умолчаний вида (3.2); F‘= Rules u Events, где Rules и Events непересекающиеся множества формул TLC, такие, что формулы, входящие в множество Rules, имеют вид А з В, где А и В любые замкнутые формулы TLC, а формулы, входящие в множество Events, имеют вид first next [nj р (ej, ... , eic), где n натуральное число, меньшее или равное числу моментов времени на часах формулы р(еь ... , ек), если эти часы являются конечной последовательностью натуральных чисел; р k-местный предикатный символ; еь ... , ек термы, не имеющие вхождений индивидных переменных. По терминологии TLC формулы такого вида называются атомарными событиями (р ( e l,..., ек) “чистый временной атом”) и относятся к классу т.н. формул фиксированного времени (fixed-time formula), т.е. формул, значения которых зависят ровно от одного момента времени. Значение формулы first next [п] А для любого момента времени на её и з локальных часах ck,( равно значению формулы А для момента времени, соответствующему n-му элементу ск> Расширение временной теории с умолчаниями определим следующим образом. Пусть Ltlc язык логики TLC, X подмножество из L tlc >Thl ( X ) множество замкнутых формул, выводимых из X с использованием аксиом и правил вывода логики TLC при конкретном присваивании часов ск: Thl ( X ) = {w w e Ltlc , w замкнута и X -ckw }. Пусть A1 = Множество формул El c L назовём расширением для А1 тогда и только тогда, когда Г1(Е1 ) = Е1 (т.е. Е‘ неподвижная точка оператора Г1 ). Процесс рассуждения с умолчаниями в рамках TDLC представляег собой построение всех расширений для каждого элемента последовательности А * о , А ‘ь ..., который является временной теорией с умолчаниями, и для любых A‘¡= <Р, ck, D1 ,-, Fl¡>, AVi = <Р, ск, DVi, F Vi> выполняются следующие условия: 1)D \=D \,u 2) Rules ‘¡= Rules Vi> 3) Events ‘j с Events Vt, причём любая формула, входящая в Events Vi, но не входящая в Events '¡, фиксирована на момент времени, 114 |