uzluga.ru
добавить свой файл
РАЗРЕШИМОСТЬ ЛИНЕЙНОЙ ЛОГИКИ ЗНАНИЯ

И ВРЕМЕНИ LTK.

Лукьянчук А.Н., Римацкий В.В.


В настоящее время быстро развивается изучение модальных и много-модальных логик, описывающих человеческие рассуждения. Одной из таких логик является много-модальная логика знания и времени LTK (Linear Time and Knowledge), которая совмещает в себе модальности по времени и знанию.

Логика определяется семантически как множество формул, истинных на LTK-фреймах,

где LTK-фрейм это много-модальный фрейм Крипке, сочетающий в себе линейное и дискретное представление потока времени и S5-модальность, определенную в каждый момент времени и представляющую знание.

Язык состоит из счетного множества пропозициональных переменных , стандартных булевых операций и множества модальных операторов , . Значение модальных операторов: (а) означает, что формула всегда будет истинна, (в) означает, что известна всем в рассматриваемый момент времени, (с) означает, что действующему агенту “” известна формула на протяжении всего потока времени. Мы рассматриваем случай логики LTK, где количество агентов “” может быть любым.

LTK-фрейм это много-модальный фрейм , где:

(а) это не пустое множество миров,

(в) бинарное отношение линейно, иртранзитивно, рефлексивно/иррефлексивно,

(с) бинарное отношение это универсальное S5-отношение внутри сгустка по времени,

(d) некоторое отношение эквивалентности внутри сгустка по времени.

Доказано следующее утверждение:

Утверждение: В логике LTK справедливо .

Первый важный результат, который мы получили, это финитная аппроксимируемость логики LTK. Логика называется финитно аппроксимируемой, если для любой формулы , не доказуемой в , существует конечный фрейм (или конечная алгебра), адекватный , на котором опровергается формула . Из финитной аппроксимируемости логики следует ее разрешимость. Напомним, что логика является разрешимой, если существует алгоритм, позволяющий распознать, принадлежит ли произвольная формула логике или нет.

Далее будем рассматривать логику LTK с интранзитивным и рефлексивным отношением времени T. Обозначим ее

Возьмем формулу такую, что и . Тогда существует фрейм , означивание и элемент такие, что .

Определим модель следующим образом:

,


где

Причем мощность модели ограниченна размером формулы и ее временной степенью .

Доказано, что формула опровергается на конечной модели . То есть справедлива теорема:

Теорема: Логика финитно аппроксимируема.

Использую данный результат, получили следующую лемму:

Лемма 1: Логика разрешима.

Для логики LTK с интранзитивным и иррефлексивным отношением времени T получены аналогичные результаты.

Так же была построена характеристическая модель логики LTK. Модель Крипке является характеристической для логики тогда и только тогда, когда: (а) (в) для любой формулы от переменных , .

Шаг 1. Возьмем класс конечных LTK- фреймов такой, что для любого фрейма , Обозначим как класс всех возможных различных не изоморфных моделей , где:

(а) ;

(в)

(с)

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

Шаг 2. К каждому сгустку из приписываем снизу все из в том случаи, если не изоморфен подмодели сгустка . Результатом такого добавления станет модель .

Шаг 3. Предположим, что модель для построена так, что ее фрейм, это LTK-фрейм, и для любых двух сгустков этого фрейма, если это непосредственный предшественник , то не изоморфен как подмодель. Модель строим следующим образом. К каждому сгустку глубины приписываем снизу все из в том случаи, если не изоморфен подмодели сгустка .

В конечном счете, получили модель

.

Свойства построенной модели сформулированы в следующих утверждениях:

Лемма 2: Модель является характеристической для логики LTK.

Лемма 3: Модель является формульной.

Напомним, что модель является формульной тогда и только тогда, когда существует формула такая, что