Здесь представлена последняя часть программы приведения формулы к стандартной форме. Прежде всего, определим предикат 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).
|
Главная
Каталог файлов
