Программирование на языке ПРОЛОГ для искуственного интеллекта




Простая программа для автоматического докаэательства теорем - часть 4


И наконец, после применения правила 2 получаем искомую конъюнктивную нормальную форму

        (~а  v  b)   &  (~b  v  с)  &  а   &  ~с

состоящую из четырех дизъюнктов. Теперь можно приступить к резолюционному процессу.

Элементарный шаг резолюции выполняется всегда, когда имеется два дизъюнкта, в одном из которых встретилось элементарное утверждение  р,   а в другом -  ~р.  Пусть этими двумя дизъюнктами будут

        р  v  Y                 и                 ~р   v  Z

Шаг резолюции порождает третий дизъюнкт:

        Y  v  Z

Нетрудно показать, что этот дизъюнкт логически следует из тех двух дизъюнктов, из которых он получен. Таким образом, добавив выражение (Y   v  Z) к нашей исходной формуле, мы не изменим ее истинности. Резолюционный процесс порождает новые дизъюнкты. Появление "пустого дизъюнкта" (обычно записываемого как "nil") сигнализирует о противоречии. Действительно, пустой дизъюнкт nil  порождается двумя дизъюнктами вида

        x    и     ~x

которые явно противоречат друг другу.

fig16_6.gif (1078 bytes)

Рис. 16. 6.  Доказательство теоремы  (а=>b)&(b=>с)=>(a=>с)   методом
резолюции. Верхняя строка - отрицание теоремы в конъюнктивной
нормальной форме. Пустой дизъюнкт внизу сигнализирует, что
отрицание теоремы противоречиво.

На рис. 16.6 показан процесс применения резолюций, начинающийся с отрицания нашей предполагаемой теоремы и заканчивающийся пустым дизъюнктом.

На рис. 16.7 мы видим, как резолюционный процесс можно сформулировать в форме программы, управляемой образцами. Программа работает с дизъюнктами, записанными в базе данных.


Содержание  Назад  Вперед