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

Этап 5 - использование дистрибутивных законов для & и #

На этом этапе исходная формула исчисления предикатов претерпела довольно много изменений. Формула больше не содержит в явном виде кванторов, а из логических связок в ней остались лишь & и # (помимо отрицания, входящего в состав литералов). Теперь формула преобразуется к специальному виду - конъюнктивной нормальной форме, характерной тем, что дизъюнктивные члены формулы не содержат внутри себя конъюнкцию. Таким образом, формулу можно преобразовать к такому виду, когда она будет представлять последовательность элементов, соединенных друг с другом конъюнкциями, а каждый элемент является либо литералом, либо состоит из нескольких литералов, соединенных дизъюнкцией. Чтобы привести формулу к такому виду, необходимо использовать следующие два тождества:

(А&В) # С эквивалентно (А # С)&(В # С)

А # (В&С) эквивалентно (А # В)&(А # С)

Так, например, формула:

выходной(Х) # (работает(крис, X) & (сердитый (крис) # унылый(крис)))

(Для каждого X либо X – выходной день, либо Крис работает в день X и при этом он либо сердитый, либо унылый) эквивалентна следующей:

выходной(Х) # (работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))

(Для каждого X, во-первых, X является выходным днем или Крис работает в день X; во-вторых, либо X – выходной день, либо Крис сердитый или унылый).

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