|
A : U B ~ 7 ’ где А и 5 формулы TLC, такие, что ck* = скв : причём В формула, имеющая ровно одно вхождение некоторого одноместного предикатного символа (вхождений других предикатных символов нет) и если В имеет свободную переменную, то в А эта переменная имеет только свободные вхождения (одно или больше), иначе данное умолчание замкнутое. Заметим, что умолчания, определённые таким образом, соответствуют классу т.к. нормальных умолчаний в обычных логиках умолчаний, для которых гарантировано существование расширений [16]. В отличие от обычных логик умолчаний, не только открытые, но и замкнутые умолчания вида (3.30) в TDLC представляют собой общие схемы вывода, т.е. являются по сути множествами замкнутых умолчаний, имеющих вид: fimnextln1?/f :М 1 8 ( а д где пнатуральное число, меньшее или равное числу моментов времени на часах формулы А, т.е. ск^, если скл конечная последовательность; ? подстановка вида {е/х}, где е индивидная константа. Если формулы А и В не имеют вхождений свободной переменной (т.е. они замкнутые), то тогда ? ж Р. Далее, временную теорию с умолчаниями определим как четверку: & ' = < P,ck,D ‘, F 4 (3.32) где Р множество всех предикатных символов, встречающихся в элементах множеств D' и F1; ск присваивание часов, т.е. отображение из множества Р в множество всех часов СК, являющееся множеством всех подпоследовательностей последовательности натуральных чисел; 160 |
существу синтезом логики умолчаний Рейтера и временной логики с часами, подробно рассмотренные в предыдущей главе. Подобно тому, как обычные логики умолчаний базируются, т.е. в некотором смысле расширяют, классическую логику первого порядка, предлагаемая в данном разделе временная логика умолчаний основана на временной логике с часами TLC (Temporal Logic with Clock) и логике умолчаний. Будем называть эту логику TDLC (Temporal Default Logic with Clock). TDLC строится аналогично обычным логикам умолчаний. Временные умолчания здесь имеют вид: АМВ , (3.2) В где А и В формулы TLC, такие, что ск4 = скв ; причём В формула, имеющая ровно одно вхождение некоторого одноместного предикатного символа (вхождений других предикатных символов нет) и если В имеет свободную переменную, то в А эта переменная имеет только свободные вхождения (одно или больше), иначе данное умолчание замкнутое. Заметим, что умолчания, определённые таким образом, соответствуют классу т.н. нормальных умолчаний в обычных логиках умолчаний, для которых гарантировано существование расширений [186]. В отличие от обычных логик умолчаний, не только открытые, но и замкнутые умолчания вида (3.2) в TDLC представляют собой общие схемы вывода, т.е. являются по сути множествами замкнутых умолчаний, имеющих вид first next [n](ji4 : М (уВ Q ^ ^ а в где пнатуральное число, меньшее или равное числу моментов времени на часах формулы А, т.е. скл, если ск^ конечная последовательность; 112 а подстановка вида {е/х}, где е индивидная константа. Если формулы А и В не имеют вхождений свободной переменной (т.е. они замкнутые), то тогда ст= 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 [п] А для любого момента времени на её и з |