Как было обещано в гл. 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. При представлении логических связок как функторов, формулы исчисления предикатов превращаются в структуры, которые могут быть изображены в виде деревьев. Каждый из шести основных этапов перевода в стандартную форму представляет некоторое преобразование дерева, которое отображает входное дерево в выходное.
Полезно для вашего бизнеса - http://alexjiang.ucoz.com. |
Главная
Каталог файлов
