Исключение кванторов существования

Приведение формул исчисления предикатов к дизъюнктам Хорна.

Пример: Привести к дизъюнктам Хорна следующую ППФ:

" x {R(x) ® {" y {R(y) ® R(j (x, y))} Ùù " y {J(x, y) ® R(y)}}}.

Процесс преобразования ППФ в форму дизъюнктов Хорна состоит

из следующих этапов:

1. Исключение знаков импликации. Знак импликации можно исключить подстановкой в исходном утверждении вместо A® B ºù A Ú B. Такая подстановка даёт возможность записать:

" x {ù R(x) Ú {" y {ù R(y) Ú R(j (x, y))} Ùù " y {ù J(x, y) Ú Ú R(y)}}}.

2. Уменьшение области действия знаков отрицания. Необходимо, чтобы знак отрицания применялся не более чем к одной предикатной букве. С помощью повторного применения указанных далее подстановок можно свести область действия каждого знака отрицания до отдельной предикатной буквы:

заменить ù (A Ù B) на ù A Ú ù B;

заменить ù (A Ú B) на ù A Ù ù B;

заменить ù ù A на A;

заменить ù " A на $ {ù A};

заменить ù $ A на " {ù A}.

Тогда ППФ примет сначала вид: " x {ù R(x) Ú {" y {ù R(y) ÚR(j (x, y))} Ù$ y {ù {ù J(x, y) Ú R(y)}}}}, а затем: " x {ù R(x) Ú {" y {ù R(y)ÚR(j (x, y))}Ù$ y {J(x, y) Ù ù R(y)}}}.

3.Стандартизация переменных. В области действия любого квантора переменная, связываемая им, не влияет на значения истинности предикатов, включающих эту переменную. Поэтому везде в области действия квантора её можно заменить другой переменной, и это не приведёт к изменению значения истинности ППФ. Стандартизация переменных в ППФ означает переименование связанных переменных, с тем чтобы каждый квантор имел свою собственную переменную. Так вместо " x {R(x) ® $ x J(x)} следует написать " x {R(x) ® $ y J(y)}. Стандартизация в этом примере даёт запись вида :"x {ù R(x) Ú {" y {ù R(y) Ú R(j (x, y))} Ù $ w {J(x, w) Ùù R(w)}}}.

Рассмотрим ППФ " y $ x R (x, y), которую можно интерпретировать, например, так: для всех y существует такой x (возможно зависящий от y), что x больше y. Заметим, что поскольку квантор существования ($ x) находится внутри области действия квантора всеобщности (" y), допускается, что значение x может зависеть от значения y. Пусть эта зависимость определяется явно с помощью некоторой функции g(y), отображающей каждое значение y в x, которой “существует”. Такая функция называется функцией Сколема. Если вместо x, который “существует”, взять функцию Сколема, то можно исключить квантор существования: " y R (g(y), y). Общее правило исключения из ППФ квантора существования состоит в замене в ней всюду переменной, относящейся к квантору существования, функцией Сколема, аргументами которой служат переменные, относящиеся к тем кванторам всеобщности,

области действия, которых охватывают область действия исключаемого квантора существования. Функциональные буквы для функций Сколема должны быть ”новыми” в том смысле, что они не должны совпадать с теми буквами, которые уже имеются в ППФ. Если исключаемый квантор существования не принадлежит области действия ни одного из кванторов всеобщности, то функция Сколема не содержит аргументов, т.е. является просто константой. Так ППФ $ x R (x) превращается в R (c), где c-константа, про которую известно, что она “существует”. Чтобы исключить все переменные, относящиеся к кванторам существования, надо применить описанную ранее процедуру по очереди к каждой переменной. В нашем примере исключение квантора существования даёт ППФ вида:

"x {ù R(x) Ú {" y {ù R(y) Ú R(j (x,y))}Ù{J(x,g(x)) Ùù R(g(x))}}},

где g(x)- функция Сколема.

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

Предваренная нормальная форма для ППФ примера имеет вид:

"x " y {ù R(x) Ú {{ù R(y) Ú R(j (x, y))}Ù{J(x,g(x)) Ùù R(g(x))}}}.

6. Приведение матрицы к конъюнктивной нормальной форме. Любую матрицу можно представить в виде конъюнкций конечного множества дизъюнкций предикатов и (или) их отрицаний. Говорят, что такая матрица имеет конъюнктивную нормальную форму. Любую матрицу можно привести в конъюнктивную нормальную форму, применяя несколько раз следующее правило:

Заменить A Ú {B Ù R} на {A Ú B} Ù {A Ú R}.

После приведения матрицы ППФ в конъюнктивную нормальную форму она примет вид: "x " y {{ù R(x) Ú ù R(y) Ú R(j (x, y))}Ù Ù{ù R(x) Ú J(x,g(x)) }Ù{ ù R(x) Ú ù R(g(x))}}.

7. Исключение кванторов всеобщности. Так как все переменные ППФ должны быть связанными, то все оставшиеся на этом этапе переменные относятся к кванторам всеобщности. Так как порядок расположения кванторов всеобщности несуществен, то

эти кванторы можно явным образом не указывать, условившись, что все переменные в матрице относятся к кванторам всеобщности. Таким образом, остаётся лишь матрица в конъюнктивной нормальной форме.

8. Исключение связок (конъюнкций). Исключение конъюнкций происходит путём замены записи A Ù B двумя ППФ A и B. Результатом многократной замены будет конечное множество ППФ, каждая из которых представляет собой дизъюнкту Хорна.

Таким образом, ППФ представляется теперь в виде следующих дизъюнкт Хорна:

ù R(x) Ú ù R(y) Ú R(j (x, y));

ù R(x) Ú J(x,g(x));

ù R(x) Ú ù R(g(x)).

Следовательно, ограничение правила резолюции, накладываемое на вид аксиом и ППФ теоремы несущественно.

Дата добавления: 2015-06-27