Книга: ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ

Этап 3 - сколемизация

Предикат skolem имеет три аргумента, соответствующих: исходной формуле, преобразованной формуле и списку переменных, которые на текущий момент были введены посредством кванторов общности.

skolem(all(X,P),all(X,P1),Vars):-!, scolem(P,Pl,[X|Vars]).

skolem(exists(X,P),P2,Vars):-!, gensym(f,F), Sk =..[F|Vars], subst(X,Sk,P,P1), skolem(P1,P2,Vars).

skolem((P # Q),(P1 # Q1),Vars):-!, skolem(P,P1,Vars), skolem(Q,Q1,Vars).

skolem((P & Q),(P1 & Q1), Vars):-!, skoIem(P,P1,Vars), skolem(Q,Q1,Vars).

skolem(P,P,_).

В этом определении используются два новых предиката. Предикат gensym должен быть определен таким образом, что целевое утверждение gensym(X, Y) вызывает конкретизацию переменной Y значением, представляющим новый атом, построенный из атома X и некоторого числа. Он используется для порождения сколемовских констант, не использовавшихся ранее. Предикат gensym определен в разд. 7.8 как генатом. Второй новый предикат, о котором уже упоминалось, это subst. Мы требуем, чтобы subst(Vl,V2,F1,F2) было истинно, если формула F2 получается на F1 в результате замены всех вхождений V1 на V2. Определение этого предиката оставлено в качестве упражнения для читателя. Оно аналогично определениям, приведенным в разд. 7.5 и 6.5.

Оглавление книги