Сколемовская стандартная форма

Наличие разноименных кванторов в префиксе не позволяет осуществлять вывод заключения, опираясь только на матрицу. Однако есть эффективный алгоритм Сколема, удаляющий из префиксной части кванторы существования и преобразующий формулу к виду . В этом случае вывод заключения возможен только по формуле матрицы. Для устранения в префиксе кванторов существования вводится сколемовская функция от предметных переменных кванторов всеобщности, которая замещает в матрице связанную квантором существования предметную переменную.

Алгоритм приведения формулы к виду ССФ:

Шаг 1. Представить формулу в виде ПНФ, т. е. , где , а .

Шаг 2: Найти в префиксе самый левый квантор существования и заменить его по правилу:

А. «Если квантор существования находится на первом месте префикса, то вместо переменной, связанной этим квантором, подставить в матрице всюду предметную постоянную a, отличную от встречающихся постоянных, а квантор существования удалить».

Например, в формуле переменную заменим константой , получим . Такие константы называют сколемовскими константами.

Б. «Если квантор существования находится на i-м месте префикса, т.е. , то выбрать -местную функцию , отличную от функций матрицы М и выполнить замену предметной переменной , связанной квантором существования, на функцию и квантор существования из префикса удалить».

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

Шаг 3: найти в префиксе следующий слева квантор существования и перейти к исполнению шага 2, иначе конец.

Формулу ПНФ, полученную в результате введения сколемовских функций называют сколемовской стандартной формой (ССФ).

Преобразованная таким образом матрица может быть допущена к анализу истинности суждения по принципу резолюции.

Пример 1. Дано . Преобразовать формулу к виду ССФ.

Решение.

Принять и удалить :

.

Принять и удалить :

Принять и удалить :

Матрица ССФ содержит два дизъюнкта:

.

Пример 2. Дано

.

Преобразовать формулу к виду ССФ.

Решение.

Принять и удалить :

Принять и удалить :

Множество дизъюнктов матрицы:

.