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

Этап 6 - выделение множества дизъюнктов

Здесь представлена последняя часть программы приведения формулы к стандартной форме. Прежде всего, определим предикат clausify, который осуществляет построение внутреннего представления совокупности дизъюнктов. Эта совокупность представлена в виде списка, каждый элемент которого является структурой вида cl(A, В). В этой структуре А – это список литералов без отрицания, а В – список литералов с отрицанием (знак отрицания ~ явно не содержится). Предикат clausify имеет три аргумента. Первый аргумент для формулы, передаваемой с пятого этапа обработки, Второй и третий аргументы используются для представления списков дизъюнктов. Предикат clausify создает список, заканчивающийся переменной, а не пустым списком ([]) как обычно, и возвращает эту переменную посредством третьего аргумента. Это позволяет другим правилам добавлять элементы в конец этого списка, конкретизируя соответствующим образом указанную переменную. В программе выполняется проверка с целью выявления ситуаций, когда одна и та же атомарная формула входит в дизъюнкт как с отрицанием, так и без него. Если такая ситуация имеет место, то соответствующий дизъюнкт не добавляется к списку, так как подобные дизъюнкты являются тривиально истинными и не дают ничего нового. Выполняется также проверка неоднократного вхождения литерала в дизъюнкт.

clausify((P& Q),C1,C2):-!, clausify(P,C1,C3), clausify(Q,C3,C2).

clausify(P,[cl(A,B)|Cs],Cs):- inclause(P,A,[],B,[]),!.

clausify(_,C,C).

inclause((P # Q), A, A1, B, B1):-!, inclause(P,A2,A1,B2,B1),inclause(Q,A,A2,B,B2).

inclause((~P),A,A,B1,B):-!, notin(P,A), putin(P,B,B1).

inclause(P,A1,A,B,B):- notin(P,B), putin(P,A,A1).

notin(X,[X|_]):-!, fail.

notin(X,[_|L]):-!, notin(X,L).

notin(X,[]).

putin(X,[],[X]):-!.

putin(X,[X|L],L):-!.

putin(X,[Y|L], [Y|L1]):- putin(X,L,L1).

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