Пример 6
По заданной формуле ([p] & [q] & [(p q)] найдём свойство шкал (W, R), относительно которых эта формула является тавтологией. Положим:
А = [p] & [q] & [(p q)];
(t) = t1t2t3R(t, t1) & R(t1, t2) & p*(t2) & R(t, t3) & q*(t3) & ((p*(t) q*(t))).
Из условий истинности:
p*(t2) = x(R(t2, x) p*(x)),
q*(t3) = x(R(t3, x) q*(x)),
найдём ленивые определения:
p*(x) = R(t2, x); q*(x) = R(t3, x).
Подставляя их в (t) и учитывая, что p*(t2) = 1 и , q*(t3) = 1, получим:
(t) = t1t2t3R(t, t1) & R(t1, t2) & R(t, t3) & (x(R(t, x) R(t2, x)) R(t3, x)).
Утверждение (W, R) |= t(t) приводит к формуле 1-го порядка:
tt1t2t3(R(t, t1) R(t1, t2) R(t, t3) x(R(t, x) R(t2, x)) R(t3, x).
Упражнения
Найти свойства шкал Крипке, соответствующих формулам:
-
А А (Ответ: u(wRu));
-
А А (Ответ: wRu & wRu vRu);
-
А А (Ответ: wRv & wRu v = u);
-
А А (Ответ: wRv u(wRu & uRv));
-
А А (Ответ: wRv & wRx u(vRu & xRu)).
- 6. Модальная и темпоральная логикИ
- 6.1. Синтаксис модальной логики
- Дополнительные логические связки
- Приоритеты операций
- Смысловые значения модальностей
- 6.2. Семантика модальной логики
- Модели Крипке
- Упражнение 1
- Упражнение 2
- Семантика темпоральной логики
- Упражнение 3
- Тавтологии
- Упражнение 4
- Условные тавтологии
- Упражнение 5
- 6.3. Алгоритмическая логика Хоара
- Пропозициональная динамическая логика
- Семантика пропозициональной динамической логики
- Аксиомы pdl
- Правила вывода
- Логика Хоара
- Корректность и полнота систем Гильберта
- Свойства шкал Крипке
- Алгоритм Салквиста
- Пример 2
- Пример 3
- Пример 6
- 6.5. Темпоральная логика
- Система Гильберта для темпоральной логики
- Линейные потоки времени
- Стандартный перевод
- Завтра и вчера
- Выбор операторов
- 7. Алгоритмы и рекурсивные функции
- 7.1. Частично рекурсивные функции
- Простейшие функции
- Пример 1
- Оператор примитивной рекурсии
- Пример 2
- Пример 4
- Пример 5
- Пример 6
- Оператор минимизации
- Пример 7
- 7.2. Машины Тьюринга
- Пример 1
- Пример 2
- Пример 3
- Упражнение
- 7.3. Вычислительная сложность
- Труднорешаемые и np-полные задачи
- 6. Модальная и темпоральная логикИ 49
- 7. Алгоритмы и рекурсивные функции 65