Редактирование: Семантическая таблица
Перейти к навигации
Перейти к поиску
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий ниже, чтобы убедиться, что это нужная вам правка, и запишите страницу ниже, чтобы отменить правку.
Текущая версия | Ваш текст | ||
Строка 61: | Строка 61: | ||
Каждая таблица может рассматриваться как графическое представление формулы, эквивалентное множеству, из которого построена таблица. Эта формула выглядит следующим образом: каждая ветвь таблицы представляет соединение своих формул; таблица представляет дизъюнкцию своих ветвей. Правила расширения преобразуют таблицу в таблицу, имеющую эквивалентную представленную формулу. Поскольку таблица инициализируется как единая ветвь, содержащая формулы входного множества, все последующие таблицы, полученные из нее, представляют формулы, эквивалентные этому множеству (в варианте, где начальная таблица является единственным узлом, обозначенным true, формулы, представленные таблицами, являются следствиями исходного множества.) | Каждая таблица может рассматриваться как графическое представление формулы, эквивалентное множеству, из которого построена таблица. Эта формула выглядит следующим образом: каждая ветвь таблицы представляет соединение своих формул; таблица представляет дизъюнкцию своих ветвей. Правила расширения преобразуют таблицу в таблицу, имеющую эквивалентную представленную формулу. Поскольку таблица инициализируется как единая ветвь, содержащая формулы входного множества, все последующие таблицы, полученные из нее, представляют формулы, эквивалентные этому множеству (в варианте, где начальная таблица является единственным узлом, обозначенным true, формулы, представленные таблицами, являются следствиями исходного множества.) | ||
Таблица для выполнимого множества {A⋀c, A⋁b}: все правила были применены к каждой формуле на каждой ветви, но таблица не закрыта (только левая ветвь закрыта), как ожидалось для выполнимых множеств | Таблица для выполнимого множества {A⋀c, A⋁b}: все правила были применены к каждой формуле на каждой ветви, но таблица не закрыта (только левая ветвь закрыта), как ожидалось для выполнимых множеств | ||
Метод таблиц работает, начиная с начального набора формул, а затем добавляя к таблицам более простые и простые формулы, пока противоречие не будет показано в простой форме противоположных литералов. Поскольку формула, представленная таблицей, является дизъюнкцией формул, представленных ее ветвями, противоречие получается, когда каждая ветвь содержит пару противоположных литералов. | Метод таблиц работает, начиная с начального набора формул, а затем добавляя к таблицам более простые и простые формулы, пока противоречие не будет показано в простой форме противоположных литералов. Поскольку формула, представленная таблицей, является дизъюнкцией формул, представленных ее ветвями, противоречие получается, когда каждая ветвь содержит пару противоположных литералов. |