1.4. Формирование правил вывода в динамической среде  

Подобно тому, как обычные логики умолчаний базируются, т.е.

AMB

(1.14)

где А и В - формулы TLC, такие, что скл = скв ;

причём В - формула, имеющая ровно одно вхождение некоторого одноместного предикатного символа (вхождений других предикатных символов нет) и если В имеет свободную переменную, то в А эта переменная имеет только свободные вхождения (одно или больше), иначе данное умолчание замкнутое. Заметим, что умолчания, определённые таким образом, соответствуют классу т.н. нормальных умолчаний в обычных логиках умолчаний, для которых гарантировано существование расширений [18].

36 В отличие от обычных логик умолчаний, не только открытые, но и

замкнутые умолчания вида (1.14) в TDLC представляют собой общие схемы

вывода, т.е. являются по сути множествами замкнутых умолчаний, имеющих

вид:

first next [n]?А: М?g

(1-15)

где п- натуральное число, меньшее или равное числу моментов времени на часах формулы А, т.е. cki, если ск^ - конечная последовательность;

? - подстановка вида {е/х}, где е - индивидная константа. Если формулы А и В не имеют вхождений свободной переменной (т.е.

Далее, временную теорию с умолчаниями определим как четверку:

${ = lt;?,ск,В\?1gt;,(1-16)

где Р - множество всех предикатных символов, встречающихся в элементах множеств D1 и F1;

ск - присваивание часов, т.е. отображение из множества Р в множество всех часов СК, являющееся множеством всех подпоследовательностей последовательности натуральных чисел;

D1 - множество временных умолчаний вида (1.14);

F* = Rules і Events, где Rules и Events - непересекающиеся множества формул TLC, такие, что формулы, входящие в множество Rules, имеют вид А 8 В, где А и В - любые замкнутые формулы TLC, а формулы, входящие в множество Events, имеют вид first next [п] р (еь ... , ek), где п - натуральное число, меньшее или равное числу моментов времени на часах формулы р(еь ... , ek), если эти часы являются конечной последовательностью натуральных чисел; р - k-местный предикатный символ; е1з ... , ек - термы, не имеющие вхождений индивидных переменных.

37 По    терминологии    TLC    формулы    такого    вида    называются

атомарными событиями  (р  (el,  ...  ,  ek)  - "чистый временной атом")  и

относятся к классу т.н. формул фиксированного времени (fixed-time formula),

т.е. формул, значения которых зависят ровно от одного момента времени.

Значение формулы    first next [п] А для любого момента- времени на её

локальных часах ск^ равно значению- формулы А- для момента времени,

соответствующему п-му элементу ск^.

Расширение временной теории с умолчаниями определим следующим образом. Пусть Ltlc - язык логики TLC, X - подмножество из LTLC , Thl ( X ) -множество замкнутых формул, выводимых из X с использованием аксиом и правил вывода логики TLC при конкретном присваивании часов ck:

Thl (X)={wlw|i Ltlc , w замкнута и X  | -ck w }.

Пусть i$ = lt;Р, ck, Dl, Fl gt;- временная теория с умолчаниями, S Н LTLc.

l)Fl И ^,l(S),

2. Th? CatfS)) = damp;'(S),
3. если ЛШАft D*, АЪ damp;'(S)

в

n^Bg s, товъda'(S).

Множество формул El H L является расширением для ^ тогда и только тогда, когда ^1(Е1) = Е1 (т.е. Е1 - неподвижная точка оператора МЇ).

Процесс рассуждения с умолчаниями в рамках TDLC представляет собой построение всех расширений для каждого элемента последовательности $f0i..., ^ь — , который является временной теорией с умолчаниями, и для любых ^1; = lt;Р, ck, D\, Fljgt;, ^Vi = lt;?gt; ck, DVi, F ti+igt; выполняются следующие условия:

OD^DVi,

2) Rules 'і = Rules Vi,

38 3) Events \H Events Vi, причём любая формула, входящая в Events

Vi, но не входящая в Events \, фиксирована на момент времени, тот же или

более    поздний,   чем    самый lt;  поздний    момент   времени,    на   который

фиксирована любая формула из множества Events \.

Таким образом, рассуждения, формализуемые в TDLC, это рассуждения о мире, эволюционирующем во времени и знания о котором неполны, но пополняются и изменяются по мере поступления новых частных фактов, выражаемых формулами, входящими в множество Events соответствующей временной- теории с умолчаниями. При этом операционные знания об этом мире не меняются во времени. Их можно подразделить на надёжные, выражаемые формулами из множества Rules, и правдоподобные, выражаемые при помощи временных умолчаний. Эти рассуждения немонотонны, причём немонотонность обусловлена необходимостью пересмотра» выводов, которые делаются на основе ошибочных предположений, принятых в условиях дефицита времени.

Механизм функционирования предлагаемой немонотонной временной логики умолчаний рассмотрим на модельной задаче "Инцидент". Пусть в момент времени tl обнаруженному ранее и находящемуся в опасной близости от охраняемого объекта летательному аппарату (ЛА 1) был послан запрос с требованием идентифицировать себя.

Рассуждения стороны, предположившей, что ЛА1 - неприятельский, а потом отказавшейся от этого предположения, реконструируем с использованием TDLC, для чего будем использовать следующие предикатные символы (элементы множества Р):

запрос (х,у) - объекту х направлен запрос у;

39 ответ (х,у) - от объекта х получен ответ у;

враг(х) - объект (х) является неприятельским.

Будем считать, что всем перечисленным выше предикатным символам присваиваются одни и те же локальные часы, совпадающие с глобальными часами gck = lt;1, 2, 3, .... gt;, т.е. ск = {запрос Щ gck, ответ % gck, враг % gck}.

Далее, рассмотрим последовательность теорий с умолчаниями   $?і , amp;І2, amp;'з,  где ^1,= lt;Р,ск, D\?\gt;,

amp;ї2= lt; Р, ск, Dl, Fl2gt;,

?*з = lt; Р, ск, Dl, Fl3gt;,

Dl ={dl}, ?\= Rulesl І Events1!,

Fl2 = Rules 'tEvents'z,

Fl3= Rules ^Events^

Rules l={rl},

Events1^ {evl, ev2 },              ;

Eventsl2= {evl, ev2 ,..., ev32},

Events^ ={evl, ev2,..., ev38, ev39}.

Временное умолчание dl:

30

запрос(х,"Ты чей")'-' ** ^next[i] ответ(х,"Я свой"): М Пвраг(х)

i=0

DBpar(x)

Правило rl: (^Цх) ответ (х, "Я свой") В ? ^вра^х)

События (ev і):

(evl) first next [tl] запрос(ЛА1,"Ты чей"),

(ev2) «* first next [tl] ответ (ЛА1, "Я свой")

(ev3) ^ first next [tl+1] ответ (JIA1, "Я свой")

40 (ev32) ^ first next [tl + 30] ответ (ЛА1, "Я свой")

(ev38) ^ first next [tl + 36] ответ (ЛА1, "Я свой")

(ev39) first next [tl + 37] ответ (ЛА1, "Я свой") .

Расширения временных теорий с умолчаниями:

amp;',   : E^Tr^F1,);

amp;'2   :Е'2=Т1і1(Р1ГІ{Пвраг(ЛА1)});

^3:Е1з = Т1і1(Р1з І {D  ^враг(ЛАІ)}).

Содержательно расширению Е * і соответствует "возможный мир", в котором в момент времени t] был направлен запрос "Ты чей".

Расширению Е12 соответствует "возможный мир", в котором на момент времени t2 (спустя 30 секунд после запроса) не было получено никакого ответа на запрос "Ты чей" (В этом мире ЛА1- неприятельский).

Расширению Е'з соответствует "возможный мир", в котором на момент времени t3 получен ответ "Я свой". (В этом мире ЛА1- не является неприятельским).