Редактирование: Семантическая таблица
Перейти к навигации
Перейти к поиску
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий ниже, чтобы убедиться, что это нужная вам правка, и запишите страницу ниже, чтобы отменить правку.
Текущая версия | Ваш текст | ||
Строка 57: | Строка 57: | ||
===Закрытие=== | ===Закрытие=== | ||
Каждая таблица может рассматриваться как графическое представление формулы, эквивалентное множеству, из которого построена таблица. Эта формула выглядит следующим образом: каждая ветвь таблицы представляет соединение своих формул; таблица представляет дизъюнкцию своих ветвей. Правила расширения преобразуют таблицу в таблицу, имеющую эквивалентную представленную формулу. Поскольку таблица инициализируется как единая ветвь, содержащая формулы входного множества, все последующие таблицы, полученные из нее, представляют формулы, эквивалентные этому множеству (в варианте, где начальная таблица является единственным узлом, обозначенным true, формулы, представленные таблицами, являются следствиями исходного множества.) | Каждая таблица может рассматриваться как графическое представление формулы, эквивалентное множеству, из которого построена таблица. Эта формула выглядит следующим образом: каждая ветвь таблицы представляет соединение своих формул; таблица представляет дизъюнкцию своих ветвей. Правила расширения преобразуют таблицу в таблицу, имеющую эквивалентную представленную формулу. Поскольку таблица инициализируется как единая ветвь, содержащая формулы входного множества, все последующие таблицы, полученные из нее, представляют формулы, эквивалентные этому множеству (в варианте, где начальная таблица является единственным узлом, обозначенным true, формулы, представленные таблицами, являются следствиями исходного множества.) | ||
Строка 68: | Строка 67: | ||
Это правило учитывает, что формула может встречаться в нескольких ветвях (это в том случае, если есть хотя бы точка ветвления "ниже" узла). В этом случае правило для расширения формулы должно быть применено так, чтобы ее заключение(выводы) были приложены ко всем этим ветвям, которые все еще открыты, прежде чем можно будет заключить, что таблица не может быть далее расширена и что формула поэтому выполнима. | Это правило учитывает, что формула может встречаться в нескольких ветвях (это в том случае, если есть хотя бы точка ветвления "ниже" узла). В этом случае правило для расширения формулы должно быть применено так, чтобы ее заключение(выводы) были приложены ко всем этим ветвям, которые все еще открыты, прежде чем можно будет заключить, что таблица не может быть далее расширена и что формула поэтому выполнима. | ||
===Таблица с меткой набора=== | ===Таблица с меткой набора=== | ||