Метод семантических таблиц

Рассматривается интерпретация M формул языка УИП сигнатуры W.

Семантической таблицей называется упорядоченная пара множеств формул , где – множество истинных для рассматриваемой интерпретации M формул и – множество ложных для рассматриваемой интерпретации M формул.

Семантическая таблица называется выполнимой, если существует такая интерпретация M и такая оценка предметных переменных a, что

- для любой формулы

- для любой формулы

Примеры.

1. Семантическая таблица

Выполнима для двухэлементной интерпретации.

2. Семантическая таблица

невыполнима.

Теорема (о табличной проверке общезначимости формул).

Для любой формулы F языка УИП сигнатуры W условие выполняется тогда и только тогда, когда семантическая таблица невыполнима.

Семантическая таблица называется

- закрытой, если

- атомарной, если множества состоят из атомарных формул.

Предложение. Каждая закрытая семантическая таблица невыполнима и каждая незакрытая атомарная семантическая таблица выполнима.

Следствие. Если для формулы F языка УИП сигнатуры W выполнимость семантической таблицы сводится к выполнимости некоторой закрытой семантической таблицы, то формула F общезначима.

Правила корректного преобразования семантических таблиц, сохраняющие выполнимость этих таблиц, называются правилами табличного вывода.

Для семантических таблиц такие правила символически записываются выражениями вида или , которые означают, что таблица выполнима в том и только том случае, если выполнима таблица (или, соответственно, одна из таблиц ). Основные правила табличного вывода

где в правилах формула F(t) – результат замены всех вхождений переменной x в формулу F(x) термом t, переменные которого не попадают в формуле в области действия кванторов по этим переменным,

и в правилах формула F(c) – результат замены всех вхождений переменной x в формулу F(x) постоянным символом c, которыйне содержится ни в формуле ни в формулах из множеств

Лемма (корректность основных правил табличного вывода).

Для всех основных правил табличного вывода вида или таблица выполнима в том и только том случае, если выполнима таблица (или, соответственно, одна из таблиц ).

Табличным выводом для семантической таблицы называется корневое дерево, корнем которого является таблица и вершинами являются такие семантические таблицы, что из вершины в вершину (и в вершину ) идет дуга в том и только том случае, если или являются правилами табличного вывода. При этом листьями такого дерева являются закрытые или атомарные таблицы.

Табличный вывод называется успешным, если он является конечным деревом, все листья которого являются закрытыми таблицами.

Теорема полноты табличного вывода. Семантическая таблица невыполнима в том и только том случае, если для этой таблицы существует успешный табличный вывод.

Следствие. Формула F языка УИП сигнатуры W общезначима в том и только том случае, если для семантической таблицы существует успешный табличный вывод.

Автоматическое доказательство теорем

В исчислении предикатов (сокращенно, ИП) с помощью понятия вывода формул определяется множество Th(ИП) всех теорем ИП, которое в силу теоремы полноты совпадает с множеством общезначимых формул ИП.

Из неразрешимости ИП следует, что не существует универсальной эффективной процедуры (алгоритма), которая для любой формулы определяет, является ли эта формула теоремой ИП.

Тем не менее, существуют алгоритмы поиска доказательства, которые для общезначимых формул подтверждают, что эти формулы общезначимы, и для необщезначимых формул в общем случае не заканчивают свою работу.

Автоматические системы построения доказательств называют пруверами и предъявляют им следующие требования:

1) корректность,

2) полнота,

3) эффективность.

Примером такого алгоритма является метод семантических таблиц, который:

1) корректен,

2) полон,

3) но малоэффективен, так как использует двойной переборный поиск:

· выбор формулы, к которой применяется правило вывода,

· выбор правила, которое нужно применять к формуле (и которое предполагает практически невозможный перебор всех термов).

Поэтому необходим способ быстрого и точного вычисления тех термов, которые необходимо подставлять в формулы вместо переменных, связанных кванторами.

Альтернативную систему автоматического поиска доказательства разработали Жак Эрбран, Дж.Робинсон и др. на основе алгоритма нахождения интерпретации, опровергающей рассматриваемую формулу. Так как для общезначимых формул опровергающих интерпретаций нет, то такой алгоритм заканчивает работу за конечное число шагов.

Первым шагом алгоритма Эрбрана является приведение рассматриваемой формулы к специальным нормальным формам, которые аналогичны ДНФ и КНФ для формул исчисления высказываний (сокращенно, ИВ).

Не нашли, что искали? Воспользуйтесь поиском по сайту: