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

В логическом выводе используют предикаты в предваренной форме, когда все кванторы вынесены в формуле влево, т.е. предваряют формулу. Эту формулу, которая уже не содержит кванторов, можно свести к конъюнктивной нормальной форме. Преобразование в предваренную форму легко выполнить применением свойств эквивалентности и заменой переменных. Например, приведем формулу ("х)P(х)Þ($х)R(x) в предваренную форму:

("х)P(х)Þ($х)R(x) º Ø("х)P(х)Ú ($х)R(x) º ($х) ØP(х)Ú($х)R(x) º ($х)[ØP(х)ÚR(x)] º ($х)[P(х) ÞR(x)].

Логический вывод легко применяется в случае, если в предваренной форме представления фактов присутствует только квантор всеобщности. В логике предикатов разработан метод, позволяющие исключить квантор существования из формулы в предваренной форме. Этот метод связан с введением так называемых “скулемовских функций”. Рассмотрим этот метод, опуская обоснования, которые можно найти в [ЧЛ83].

Пусть предикат F находится в предваренной форме (Q₁x₁)…(Q_nx_n)M, где М есть предикат в конъюнктивной нормальной форме, а (Q₁x₁)…(Q_nx_n) - префикс кванторов. Пусть Q_r есть самый левый квантор существования, 1£r£n. Если никакой квантор всеобщности не стоит левее Q_r, то выберем новую константу с, отличную от других констант, входящих в М, заменим все вхождения x_r, встречающиеся в М, на с и вычеркнем (Q_rx_r) из префикса. Если же Q_s1…Q_sm - все кванторы всеобщности, встречающиеся левее Q_r, 1£s₁<s₂<…<s_m<r£n, выбираем новый m-местный функциональный символ f, отличный от всех других функциональных символов, заменим все, заменим все вхождения x_r, встречающиеся в М, на f(x_s1,x_s2,…x_sm) и вычеркнем (Q_rx_r) из префикса. Эту операцию применим для всех кванторов существования в префиксе слева направо; последняя из полученных формул есть скулемовская стандартная форма, к которой, собственно, и применяется алгоритм логического вывода. Константы и функции, использованные для замены переменных квантора существования, называются скулемовскими константами и функциями.

Пример 2.15. Построим скулемовскую стандартную форму предиката ($x)("y)("z)($u)("v)($w) P(x,y,z,u,v,w).

Левее ($x) в формуле нет никаких кванторов всеобщности, левее ($u) стоят кванторы всеобщности ("y) и ("z), левее ($w) стоят кванторы всеобщности ("y), ("z) и ("v). Заменяем переменную х на константу а, переменную u на двухместную функцию f(y,z), а переменную w - на трехместную функцию g(y,z,v). Скулемовская стандартная форма представленной выше формулы - ("y)("z)("v)P(а,y,z,f(y,z),v,g(y,z,v)).ÿ

Пример 2.16. Рассмотрим следующую теорему теории групп [ЧЛ83]. Теорема (о коммутативной группе). Если произведение любого элемента группы G на себя есть единица этой группы, то группа G - коммутативна.

Очевидно, что для доказательства эта теорема должна быть записана формально. Пусть предикат Р(х,у,z) означает следующее утверждение: Если хÎG и уÎG, то zÎG и ху=z (мы опускаем здесь знак бинарной операции умножения группы). Тогда теорема будет выглядеть так (единицу группы обозначим е): ("x) Р(х,х,е) Þ ("u) ("v) ("w)[Р(u,v,w) Þ Р(v,u,w)].

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

А1: в группе существует единичный элемент (т.е. для любого хÎG хе=х и ех=х)

A2: для каждого элемента группы существует обратный элемент (если х^-1 - обратный к х, то х х^-1= х^-1 х = е).

А3: любая группа удовлетворяет свойству ассоциативности (т.е. х, у и zÎG влечет x(yz) = (xy)z);

Формальное выражение этих аксиом:

А1: ("x)[P(е,х,x)&P(х,е,x)];

A2: ("у)($х)[P(x,y,e)&P(y,x,e)].

A3: ("x)("у)("z)("u) ("v)("w) [P(x,y,u) &P(y,z,v) Þ[P(x,v,w)ÛP(u,z,w)] ];

Для доказательства сформулированной выше теоремы В = {("x) Р(х,х,е) Þ ("u) ("v) ("w)[Р(u,v,w) Þ Р(v,u,w)]} просто покажем, что она является логическим следствием аксиом А1-А3. Отрицание этой теоремы:

ØB = {("x) Р(х,х,е) & Ø("u) ("v) ("w) [Р(u,v,w) Þ Р(v,u,w)]} =

{("x) Р(х,х,е) & ($u) ($v) ($w) Ø[Р(u,v,w) Þ Р(v,u,w)]}

Скулемовские формы для аксиом и отрицания следствия:

А1: ("x)[P(e,x,x)&P(x,e,x)];

A2: ("у)[P(i(у),у,e)&P(у,i(у),e)];

A3: ("x)("у)("z)("u) ("v)("w) [P(x,y,u) &P(y,z,v) Þ[P(x,v,w)ÛP(u,z,w)] ];

ØB: ("x){Р(х,х,е) & Ø[Р(a,b,c) Þ Р(b,a,c)]}.

Список дизъюнктов для метода резолюции:

(1) P(e,x,x) из А1;

(2) P(x,e,x) из А1;

(3) P(i(у),у,e) из А2;

(4) P(у,i(у),e) из А2;

(5) Р(х,х,е) из ØВ;

(6) ØP(x,y,u) Ú ØP(y,z,v) Ú ØP(x,v,w) Ú P(u,z,w) из А3;

(7) ØP(x,y,u) Ú ØP(y,z,v) Ú Ø P(u,z,w) ÚP(x,v,w) из А3;

(8) Р(a,b,c) из ØВ;

(9) ØР(b,a,c) из ØВ.

ÿ