Вычисление семантики вероятностной логической программы

В этом пункте мы рассмотрим вычисление оператора Sem (P) для базисной вероятностной логической программы P. Обозначим множество всех базисных (неаннотированных) атомов (эрбранов универсум, включающий как экстенсиональные атомы, так и атомы действий) через U. Интерпретация f: U >[0,1] сопоставляет каждому атому q (c1,…cm)U его вероятность f (q (c1,…cm)). Атом действия a (c1,…cm):p выполнен на интерпретации f, если p? f (a (c1,…cm)). Аннотированный экстенсиональный атом вида q (t1,…, tk):[l, u] выполнен на интерпретации f, если l? f (q (t1,…, tk))? u. Выполнимость литералов сообщений вида msg (Sender, A, Msg) или not msg (Sender, A, Msg) определяется относительно текущего состояния MsgBoxA обычным образом. Выполнимость встроенных предикатов определяется их естественной семантикой. Предложение a (c1,…cm):p : — L1,…, Ln выполняется на интерпретации f (для данного MsgBoxA), если при условии, что каждый Li выполняется на f, имеет место неравенство f (a (c1,…cm))? p. Интерпретация f является моделью P, если на ней выполнены все предложения P. Определим на множестве интерпретаций частичный порядок? следующим образом: f1? f2 для каждого атома q U f1(q)? f2(q). Модель f программы P назовем минимальной, если для всякой другой модели f1 программы P неверно, что f1? f. Множество моделей P замкнуто относительно «минимизации» .

Лемма 1. Пусть f1 и f2 — модели программы P. Тогда и интерпретация.

f = min (f1,f2)= {q:p|q U Л p=min (f1(q), f2(q))}.

является моделью P.

Из этой леммы следует существование минимальной модели P. Ее вычисление обеспечивается процедурой вычисления неподвижной точки, аналогичной процедуре из [9].

Теорема 1. Для всякой вероятностной логической программы P (определенного в этой работе типа) существует минимальная модель fminP, которая вычислима за полиномиальное время от gr (P).

Определим.

Perm = Sem (P).

как множество всех аннотированных атомов действий a (c1,…cm):p из fminP.