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

ПРИЛОЖЕНИЕ В. ПРОГРАММА ПРИВЕДЕНИЯ ФОРМУЛ ИСЧИСЛЕНИЯ ПРЕДИКАТОВ К СТАНДАРТНОЙ ФОРМЕ

ПРИЛОЖЕНИЕ В. ПРОГРАММА ПРИВЕДЕНИЯ ФОРМУЛ ИСЧИСЛЕНИЯ ПРЕДИКАТОВ К СТАНДАРТНОЙ ФОРМЕ

Как было обещано в гл. 10, мы проиллюстрируем процесс преобразования формулы исчисления предикатов в стандартную форму, представив фрагменты программы на Прологе, выполняющей это преобразование. Верхний уровень программы выглядит следующим образом:

translate(X):-

 implout(X,Xl), /* Этап 1 */

 negin(Xl,X2), /* Этап 2 */

 skolem(X2,X3,[]), /* Этап 3 */

 univout(X3,X4), /* Этап 4 */

 conjn(X4,X5), /* Этап 5 */

 clausify(X5,Clauses, []), /* Этап 6 */

 pclauses(Clauses). /* Печать дизъюнктов */

Здесь приведено определение предиката translate, действующего таким образом, что, если выполнить целевое утверждение translate(X), где X – это формула исчисления предикатов, то программа напечатает эту формулу в стандартной форме в виде последовательности дизъюнктов. В этой программе формулы исчисления предикатов представляются в виде структур языка Пролог, как на это указывалось ранее (в гл. 10). Однако мы сделаем некоторое отступление от предыдущего описания и будем представлять переменные, входящие в формулы исчисления предикатов, атомами языка Пролог, с целью облегчить их обработку. Предполагается, что можно отличить переменные в формулах исчисления предикатов от констант, используя некоторое соглашение относительно формы записи имен. Например, можно считать, что имена переменных всегда начинаются с одной из букв х, у, z. В действительности, переменные всегда вводятся в формулу посредством кванторов и, следовательно, их легко можно опознать. Лишь при чтении результата, печатаемого программой, программисту необходимо помнить, какие имена соответствуют переменным формул исчисления предикатов, а какие константам.

Прежде всего, необходимо объявить операторы для логических связок, используемых в формулах:

?- op(30,fx,~).

?- op(100,xfy,#).

?- op(100,xfy,&).

?- op(150,xfy,-›).

?- op(150,xfy,‹-›).

Следует обратить внимание на то, как определены операторы. В частности ~ имеет более низкий приоритет чем # и &. Для начала, необходимо сделать одно важное предположение. Предполагается, что переменные переименованы таким образом, что в обрабатываемой формуле одна и та же переменная никогда не вводится более чем одним квантором. Это необходимо, чтобы предотвратить возможные конфликты в употреблении имен в дальнейшем.

Для преобразования формул к стандартной форме мы используем метод преобразования дерева, обсуждавшийся в разд. 7.11 и 7.12. При представлении логических связок как функторов, формулы исчисления предикатов превращаются в структуры, которые могут быть изображены в виде деревьев. Каждый из шести основных этапов перевода в стандартную форму представляет некоторое преобразование дерева, которое отображает входное дерево в выходное.

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