|
? подстановка вида {е/х}, где е индивидная константа. Если формулы А и В не имеют вхождений свободной переменной (т.е. они замкнутые), то тогда ? = Р. Далее, временную теорию с умолчаниями определим как четверку: = <Р, ck, D1, Ff>, (3.35) где Р множество всех предикатных символов, встречающихся в элементах множеств D' и F1; ск присваивание часов, т.е. отображение из множества Р в множество всех часов СК, являющееся множеством всех подпоследовательностей последовательности натуральных чисел; D* множество временных умолчаний вида (3.35); Fc= Rules % Events, где Rules и Events непересекающиеся множества формул TLC, такие, что формулы, входящие в множество Rules, имеют вид А I В, где А и В любые замкнутые формулы TLC, а формулы, входящие в множество Events, имеют вид first next [n] р (е{, ..., е*), где п натуральное число, меньшее или равное числу моментов времени на часах формулы р(еь ... , е^), если эти часы являются конечной последоаательностью натуральных чисел; р k-местный предикатный символ; в ,..., еь • термы, не имеющие вхождений индивидных переменных. По терминологии TLC формулы такого вида называются атомарными событиями (р (el, ..., ek) • “чистый временной атом”) и относятся к классу т.н. формул фиксированного времени (fixed-time formula), т.е. формул, значения которых зависят ровно от одного момента времени. Значение формулы first next [п] А для любого момента времени на её локальных часах ck^ равно значению формулы А для момента времени, соответствующему пму элементу ск^. Расширение временной теории с умолчаниями определим следующим образом. Пусть L j l c язык логики TLC, X подмножество из L t l c > T h 1 ( X ) |
а подстановка вида {е/х}, где е индивидная константа. Если формулы А и В не имеют вхождений свободной переменной (т.е. они замкнутые), то тогда ст= 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 [п] А для любого момента времени на её и з |