|
множество замкнутых формул, выводимых из X с использованием аксиом и правил вывода логики TLC при конкретном присваивании часов ск; Th, ( X ) = { w l w l i Ln(C, w замкнута и X -ckw }. Пусть ^ = <Р, ck, Dc, F 1>• временная теория с умолчаниями, S И Ltu> Обозначим через J1((S) наименьшее подмножество множества L u o удовлетворяющее следующим условиям: 1)Fl 8 * ‘(S), 2)Th‘ (& \S ))= & \S \ 3)если А Ъ & Х S) в и ^ В 8, ю В Ъ dbr(S), Множество формул Е* BI L назовём расширением для $ тогда и только тогда, когда = Ес(т.е. Е* неподвижная точка оператора Д 1). Процесс рассуждения с умолчаниями в рамках T D L C представляет собой построение всех расширений для каждого элемента последовательности й£'о. й ь ••• * который является временной теорией с умолчаниями, и для любых = <Р, ck, D*j, F lj>, jgfaVi “ <Р> ск, DVi, F выполняются следующие условия: 1)D \= D \,b 2) Rules \ я Rules Vi, 3) Events В Events Vi, причём любая формула, входящая в Events \+ь но не входящая в Events фиксирована на момент времени, тот же или более поздний, чем самый поздний момент времени, на который фиксирована любая формула из множества Events Таким образом, рассуждения, формализуемые в TDLC, это рассуждения о мире, эволюционирующем во времени и знания о котором неполны, но пополняются и изменяются по мере поступления новых частных фактов, выражаемых формулами, входящими в множество Events соответствующей временной теории с умолчаниями. При этом операционные знания об этом мире не меняются во времени. Их можно подразделить на надёжные, |
локальных часах 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 115 тот же или более поздний, чем самый поздний момент времени, на который фиксирована любая формула из множества Events \. Таким образом, рассуждения, формализуемые в TDLC, это рассуждения о мире, эволюционирующем во времени и знания о котором неполны, но пополняются и изменяются по мере поступления новых частных фактов, выражаемых формулами, входящими в множество Events соответствующей временной теории с умолчаниями. При этом операционные знания об этом мире не меняются во времени. Их можно подразделить на надёжные, выражаемые формулами из множества Rules, и правдоподобные, выражаемые при помощи временных умолчаний. Эти рассуждения немонотонны, причём немонотонность обусловлена необходимостью пересмотра выводов, которые делаются на основе ошибочных предположений, принятых в условиях дефицита времени. Механизм функционирования предлагаемой немонотонной временной логики умолчаний рассмотрим на модельной задаче “Инцидент”. Пусть в момент времени tl обнаруженному ранее и находящемуся в опасной близости от охраняемого объекта летательному аппарату (JIA 1) был послан запрос с требованием идентифицировать себя. Пусть в течении 30 секунд после запроса никакого ответа не последовало, и в момент времени t2=tl+ 30 был сделан вывод, что летательный аппарат неприятельский. Пусть в момент времени t3=tl+ 37 от него был получен ответ о его принадлежности к союзникам. Рассуждения стороны, предположившей, что ЛА1 неприятельский, а потом отказавшейся от этого предположения, реконструируем с использованием TDLC, для чего будем использовать следующие предикатные символы (элементы множества Р): запрос (х,у) объекту х направлен запрос у; ответ (х,у) от объекта х получен ответ у; |