|
специфики предлагается вариант временной логики умолчаний, специализированный для формализации рассуждений в ДЭС и являющейся, по<уществу, синтезом логики умолчаний Рейтера и временной логики с часами. Подобно тому, как обычные логики умолчаний базируются, т.е. в некотором смысле расширяют, классическую логику первого порядка, предлагаемая в данном разделе временная логика умолчаний основана на временной логике с часами TLC) и логике умолчаний. Будем называть эту логику TDLC (Temporal Default Logic with Clock). TDLC строится аналогично обычным логикам умолчаний. Временные умолчания здесь имеют вид: а мв — а ' (3.33) где А н В формулы TLC, такие, что ск^ скд; причём В формула, имеющая ровно одно вхождение некоторого одноместного предикатного символа (вхождений других предикатных символов нет) и если В имеет свободную переменную, то в А эта переменная имеет только свободные вхождения (одно или больше), иначе данное умолчание замкнутое. Заметим, что умолчания, определённые таким образом, соответствуют классу т.н. нормальных умолчаний в обычных логиках умолчаний, для которых гарантировано существование расширений /5/. В отличие от обычных логик умолчаний, не только открытые, но и замкнутые умолчания вида (3.33) в TDLC представляют собой общие схемы вывода, т.е. являются по сути множествами замкнутых умолчаний, имеющих вид: firSwxt[n?.4 :М / е \ 7 7 “’ (3-34) где пнатуральное число, меньшее или равное числу моментов времени на часах формулы А , т.е. ск^, если ск^ • конечная последовательность; 165 |
существу синтезом логики умолчаний Рейтера и временной логики с часами, подробно рассмотренные в предыдущей главе. Подобно тому, как обычные логики умолчаний базируются, т.е. в некотором смысле расширяют, классическую логику первого порядка, предлагаемая в данном разделе временная логика умолчаний основана на временной логике с часами 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 |