Редактирование: Семантическая таблица
Перейти к навигации
Перейти к поиску
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий ниже, чтобы убедиться, что это нужная вам правка, и запишите страницу ниже, чтобы отменить правку.
Текущая версия | Ваш текст | ||
Строка 23: | Строка 23: | ||
Принцип таблицы заключается в том, что формулы в узлах одной ветви рассматриваются совместно, а различные ветви считаются дизъюнктивными. В результате таблица является древовидным представлением формулы, которая является дизъюнкцией соединений. Эта формула эквивалентна множеству, чтобы доказать неудовлетворительность. Процедура изменяет таблицу таким образом, что формула, представленная результирующей таблицей, эквивалентна исходной. Одно из этих соединений может содержать пару комплементарных литералов, и в этом случае это соединение оказывается неудовлетворительным. Если все соединения оказываются неосуществимыми, то исходный набор формул неосуществим. | Принцип таблицы заключается в том, что формулы в узлах одной ветви рассматриваются совместно, а различные ветви считаются дизъюнктивными. В результате таблица является древовидным представлением формулы, которая является дизъюнкцией соединений. Эта формула эквивалентна множеству, чтобы доказать неудовлетворительность. Процедура изменяет таблицу таким образом, что формула, представленная результирующей таблицей, эквивалентна исходной. Одно из этих соединений может содержать пару комплементарных литералов, и в этом случае это соединение оказывается неудовлетворительным. Если все соединения оказываются неосуществимыми, то исходный набор формул неосуществим. | ||
===И === | ===И === | ||
Всякий раз, когда ветвь таблицы содержит формулу A ∧ B A\клин B, которая является соединением двух формул, эти две формулы являются следствиями этой формулы. Этот факт может быть формализован следующим правилом для расширения таблицы: | Всякий раз, когда ветвь таблицы содержит формулу A ∧ B A\клин B, которая является соединением двух формул, эти две формулы являются следствиями этой формулы. Этот факт может быть формализован следующим правилом для расширения таблицы: | ||
Строка 34: | Строка 32: | ||
Вариант этого правила позволяет узлу содержать набор формул, а не одну. В этом случае формулы в этом наборе рассматриваются совместно, поэтому можно добавить { A , B } в конце ветви, содержащей '''A ∧ B''' . Точнее, если узел на ветке помечен X ∪ { A ∧ B } , можно добавить к ветке новый лист '''X ∪ { A , B }''' . | Вариант этого правила позволяет узлу содержать набор формул, а не одну. В этом случае формулы в этом наборе рассматриваются совместно, поэтому можно добавить { A , B } в конце ветви, содержащей '''A ∧ B''' . Точнее, если узел на ветке помечен X ∪ { A ∧ B } , можно добавить к ветке новый лист '''X ∪ { A , B }''' . | ||
===Или === | ===Или === | ||
[[Файл:Дупльмок.JPG|200px|thumb|right|a⋁b генерирует A и b]] | [[Файл:Дупльмок.JPG|200px|thumb|right|a⋁b генерирует A и b]] |