Система Гильберта для темпоральной логики
Формальная теория Kt состоит из следующих аксиом и правил вывода.
Аксиомы
-
Формулы D(B1, … Bn), где D(p1, …, pn) – пропозициональные тавтологии.
-
[F](A B) ([F]A [F]B); [P](A B) ([P]A [P]B) (нормальность).
-
[F]A [F][F]A (транзитивность).
-
A [F]<P>A; A [P]<F>A (отражение).
Правила вывода
; .
Здесь А, В, В1, …, Вn – темпоральные формулы, возможно, содержащие [F] и [P].
Исходя из того, что для любой интерпретации с помощью шкалы Крипке формулы A [F]<P>A и A [P]<F>A будут тавтологиями, легко доказать следующую теорему корректности и полноты:
Теорема 1. Для любой темпоральной формулы А утверждение KtA верно, если и только если А – тавтология относительно каждой шкалы Крипке (W, R), имеющей транзитивное отношение R. Здесь Kt ,означает, что А – теорема в формальной теории Kt.
Потоки времени
В темпоральной логике используются нерефлексивные транзитивные шкалы Крипке.
Шкала Крипке (W, <) называется потоком времени, если
-
x W ((x < x)),
-
x, y, z W (x < y & y < z x < z).
Если t < v, то v называется будущим для t, а t – прошлым для v.
Теорема 2. Для любой темпоральной формулы А утверждение KtA верно, если и только если А – тавтология относительно всех потоков времени.
- 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