Книга: ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ
Этап 2 - перенос отрицания внутрь формулы
Этап 2 - перенос отрицания внутрь формулы
Здесь необходимо определить два предиката – negin и neg. Целевое утверждение negin(X, Y) означает, что формула Y получена из X в результате применения к ней преобразования «перенос отрицания». Этот предикат является основным и именно к нему производится обращение из программы. Целевое утверждение neg(X, Y) означает, что формула Y получена из формулы ~X с помощью того же преобразования, что и в negin. В обоих случаях предполагается, что формула прошла обработку на первом этапе и, следовательно, не содержит -› и ‹-›
negin((~P),P1):-!, neg(P,P1).
negin(all(X,P),all(X,P1)):-!, negin(P,P1).
negin(exists(X,P),exists(X,P1)):-!, negin(P,P1).
negin((P & Q),(P1 & Q1)):-!, negin(P,P1), negin(Q,Q1).
negin((P # Q),(P1 # Q1)):-!, negin(P,P1), negin(Q,Q1).
negin(P,P).
neg((~P),P1):-!, negin(P,P1).
neg(all(X,P), exists(X,P1)):-!, neg(P,P1).
neg(exists(X,P),all(X,P1)):-!, neg(P,P1).
neg((P & Q),(P1 # Q1)):-!, neg(P,P1), neg(Q, Q1).
neg((P # Q),(P1 & Q1)):~!, neg(P,P1), neg(Q, Q1).
neg(P,(~P)).
- Этап 6 - выделение множества дизъюнктов
- Этап 5 - использование дистрибутивных законов для. & и #
- Этап 1 - исключение импликаций и зквивалентностей
- Этап 4 - вынесение кванторов общности в начало формулы
- Этап 1 - исключение импликаций
- Этап 3 - сколемизация
- 1.8. СТАДИИ И ЭТАПЫ РАЗРАБОТКИ ПРОГРАММ
- Полиморфизм на этапе выполнения
- 1.1. Схема и основные этапы разработки новой продукции