Редактирование: Семантическая таблица
Перейти к навигации
Перейти к поиску
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий ниже, чтобы убедиться, что это нужная вам правка, и запишите страницу ниже, чтобы отменить правку.
| Текущая версия | Ваш текст | ||
| Строка 337: | Строка 337: | ||
Добавление этого правила (Правило прореживания) делает результирующее исчисление неконфлюентным: таблицу для несогласованного множества может быть невозможно закрыть, даже если существует замкнутая таблица для того же множества. | Добавление этого правила (Правило прореживания) делает результирующее исчисление неконфлюентным: таблицу для несогласованного множества может быть невозможно закрыть, даже если существует замкнутая таблица для того же множества. | ||
Правило ( θ ) тета )недетерминировано: набор формул, которые должны быть удалены (или быть сохранены), может быть выбран произвольно; это создает проблему выбора набора формул, чтобы отбросить, который не настолько велик, это делает получающееся множество выполнимым и не настолько маленьким, это делает необходимые правила расширения неприменимыми. Наличие большого количества возможных вариантов затрудняет поиск замкнутой таблицы. | Правило ( θ ) {\displaystyle (\theta )} (\тета )недетерминировано: набор формул, которые должны быть удалены (или быть сохранены), может быть выбран произвольно; это создает проблему выбора набора формул, чтобы отбросить, который не настолько велик, это делает получающееся множество выполнимым и не настолько маленьким, это делает необходимые правила расширения неприменимыми. Наличие большого количества возможных вариантов затрудняет поиск замкнутой таблицы. | ||
Этого недетерминизма можно избежать, ограничив использование ( θ ) тета )таким образом, что он применяется только перед модальным правилом расширения и удаляет только формулы, которые делают это другое правило неприменимым. Это условие также может быть сформулировано путем объединения двух правил в одно. Полученное правило дает тот же результат, что и старое, но неявно отбрасывает все формулы, которые сделали старое правило неприменимым. ( θ ) тета )Доказано, что этот механизм удаления сохраняет полноту для многих модальных логик. | Этого недетерминизма можно избежать, ограничив использование ( θ ) {\displaystyle (\theta )} (\тета )таким образом, что он применяется только перед модальным правилом расширения и удаляет только формулы, которые делают это другое правило неприменимым. Это условие также может быть сформулировано путем объединения двух правил в одно. Полученное правило дает тот же результат, что и старое, но неявно отбрасывает все формулы, которые сделали старое правило неприменимым. ( θ ) {\displaystyle (\theta )} (\тета )Доказано, что этот механизм удаления сохраняет полноту для многих модальных логик. | ||
Аксиома Т выражает рефлексивность отношения доступности: каждый мир доступен сам по себе. Соответствующее правило расширения таблицы: | Аксиома Т выражает рефлексивность отношения доступности: каждый мир доступен сам по себе. Соответствующее правило расширения таблицы: | ||
( T ) A 1 ; … ; A n ; ◻ B A 1 ; … ; A n ; ◻ B ; B {\displaystyle (T){\frac {A_{1};\ldots ;A_{n};\Box B}{A_{1};\ldots ;A_{n};\Box B;B}}} (T){\frac {A_{1};\ldots ;A_{n};\Box B}{A_{1};\ldots ;A_{n};\Box B;B}} | |||
Это правило связывает условия над одним и тем же миром: если ◻ B | Это правило связывает условия над одним и тем же миром: если ◻ B {\displaystyle \Box B} \Box Bистинно в мире, то рефлексивность B {\displaystyle B} Бтакже истинна и в том же мире . Это правило статично, а не транзакционно, поскольку и его предварительное условие, и последующее относятся к одному и тому же миру. | ||
Это правило копируется ◻ B | Это правило копируется ◻ B {\displaystyle \Box B} \Box Bиз предварительного условия в последующее, несмотря на то, что эта формула была "использована" для генерации B {\displaystyle B} Б. Это правильно, так как рассматриваемый мир один и тот же, то ◻ B {\displaystyle \Box B} \Box Bи держится там. Это "копирование" необходимо в некоторых случаях. Например, необходимо доказать несогласованность ◻ ( a ∧ ¬ ◻ a ) {\displaystyle \Box (a\wedge \neg \Box a)} \Box (a\wedge \neg \Box a): единственные применимые правила-это порядок ( T ) , ( ∧ ) , ( θ ) , ( K ) {\displaystyle (T),(\wedge ),(\theta ),(K)} (T), (\wedge), (\theta ), (K), из которого один блокируется, если ◻ a {\displaystyle \Box a} \Box aне копируется. | ||
Вспомогательные таблицы | |||
Другой метод для того, чтобы иметь дело с формулами, держащимися в альтернативных мирах, должен начать различную таблицу для каждого нового мира, который введен в таблицу. Например, ¬ ◻ A | Другой метод для того, чтобы иметь дело с формулами, держащимися в альтернативных мирах, должен начать различную таблицу для каждого нового мира, который введен в таблицу. Например, ¬ ◻ A {\displaystyle \neg \Box A} \neg \Box Aподразумевает, что A {\displaystyle A} Одинложно в доступном мире, таким образом, каждый начинает новую таблицу, укорененную ¬ A {\displaystyle \neg A} \neg A. Эта новая таблица присоединена к узлу исходной таблицы, где было применено правило расширения; закрытие этой таблицы немедленно генерирует закрытие всех ветвей, где тот узел, независимо от того, связан ли тот же самый узел с другими вспомогательными таблицами. Правила расширения для вспомогательных таблиц такие же, как и для исходной таблицы; поэтому вспомогательная таблица может иметь в свою очередь другие (суб-)вспомогательные таблицы. | ||
Глобальные предположения | |||
Приведенные выше модальные таблицы устанавливают согласованность набора формул и могут быть использованы для решения задачи локального логического следствия. Это проблема определения того , истинна ли для каждой модели | Приведенные выше модальные таблицы устанавливают согласованность набора формул и могут быть использованы для решения задачи локального логического следствия. Это проблема определения того , истинна ли для каждой модели M {\displaystyle M} М, если A {\displaystyle A} Одинона истинна в мире w {\displaystyle w} Вт, то B {\displaystyle B} Бтакже истинна и в том же мире. Это то же самое, что проверка истинности B {\displaystyle B} Бв мире модели, в предположении, что A {\displaystyle A} Одинэто также верно в том же мире той же модели. | ||
Связанная с этим проблема является глобальной проблемой следствия, где предполагается, что формула (или набор формул) | Связанная с этим проблема является глобальной проблемой следствия, где предполагается, что формула (или набор формул) G {\displaystyle G} Гверна во всех возможных мирах модели. Проблема в том, чтобы проверить, верно ли во всех моделях M {\displaystyle M} М, где G {\displaystyle G} Гверно во всех мирах, B {\displaystyle B} Бтакже верно во всех мирах. | ||
Локальные и глобальные предположения различаются на моделях, где предполагаемая формула верна в некоторых мирах, но не в других. В качестве примера, { P , ¬ ◻ ( P ∧ Q ) } влечет ¬ ◻ | Локальные и глобальные предположения различаются на моделях, где предполагаемая формула верна в некоторых мирах, но не в других. В качестве примера, { P , ¬ ◻ ( P ∧ Q ) } влечет ¬ ◻ Q {\displaystyle \neg \Box Q} \neg \Box Qза собой глобально, но не локально. Локальное вовлечение не имеет места в модели, состоящей из двух миров, делающих '''P Pи ¬ P , Q P, Q''' истинных соответственно, и где второе доступно из первого; в первом мире предположение верно, но ◻ Q } \Box Qложно. Этот контрпример работает, потому P P что можно считать истинным в мире и ложным в другом. Если, однако, то же предположение считается глобальным, ¬ P P не допускается ни в одном мире модели. | ||
Эти две проблемы могут быть объединены, так что можно проверить, является ли B | Эти две проблемы могут быть объединены, так что можно проверить, является ли B {\displaystyle B} Блокальным следствием A Одинглобального предположения G {\displaystyle G} Г. Табличные исчисления могут иметь дело с глобальным предположением по правилу, позволяющему добавлять его к каждому узлу, независимо от мира, к которому он относится. | ||
==Обозначение== | ==Обозначение== | ||