Редактирование: Семантическая таблица
Перейти к навигации
Перейти к поиску
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий ниже, чтобы убедиться, что это нужная вам правка, и запишите страницу ниже, чтобы отменить правку.
Текущая версия | Ваш текст | ||
Строка 134: | Строка 134: | ||
Если мы начнем с произвольной формулы c классической логики и применим эти эквивалентности повторно, чтобы заменить левые стороны на правые стороны в C, то мы получим формулу C', которая логически эквивалентна C, но которая имеет свойство, что C' не содержит никаких последствий и появляется только перед атомарными формулами. Говорят, что такая формула находится в отрицательной нормальной форме, и можно формально доказать, что каждая формула c классической логики имеет логически эквивалентную формулу C' в отрицательной нормальной форме. То есть, C выполним тогда и только тогда, когда c' выполним. | Если мы начнем с произвольной формулы c классической логики и применим эти эквивалентности повторно, чтобы заменить левые стороны на правые стороны в C, то мы получим формулу C', которая логически эквивалентна C, но которая имеет свойство, что C' не содержит никаких последствий и появляется только перед атомарными формулами. Говорят, что такая формула находится в отрицательной нормальной форме, и можно формально доказать, что каждая формула c классической логики имеет логически эквивалентную формулу C' в отрицательной нормальной форме. То есть, C выполним тогда и только тогда, когда c' выполним. | ||
==Логическая таблица первого порядка== | ===Логическая таблица первого порядка=== | ||
Таблицы расширены до логики предикатов первого порядка двумя правилами для работы с универсальными и экзистенциальными кванторами соответственно. Два различных набора правил могут использоваться; оба используют форму Skolemization для обработки экзистенциальных кванторов, но отличаются на обработке универсальных кванторов. | Таблицы расширены до логики предикатов первого порядка двумя правилами для работы с универсальными и экзистенциальными кванторами соответственно. Два различных набора правил могут использоваться; оба используют форму Skolemization для обработки экзистенциальных кванторов, но отличаются на обработке универсальных кванторов. | ||
Предполагается, что набор формул для проверки достоверности здесь не содержит свободных переменных; это не является ограничением, поскольку свободные переменные неявно универсально квантифицированы, поэтому универсальные кванторы над этими переменными могут быть добавлены, в результате чего формула без свободных переменных. | Предполагается, что набор формул для проверки достоверности здесь не содержит свободных переменных; это не является ограничением, поскольку свободные переменные неявно универсально квантифицированы, поэтому универсальные кванторы над этими переменными могут быть добавлены, в результате чего формула без свободных переменных. | ||
===Таблица первого порядка без объединения=== | ===Таблица первого порядка без объединения=== | ||