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




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


Ее отрицание имеет вид

        ~ ( (а  =>  b) & (b  =>  с) => (а  =>  с) )

Для преобразования этой формулы в конъюнктивную нормальную форму можно использовать следующие известные правила:

    (1)        х  =>   у                     эквивалентно                 ~х   v  у
    (2)        ~(x   v  y)                    эквивалентно                 ~х   &  ~у
    (3)        ~(х   &  у)                   эквивалентно                 ~х   v  ~у
    (4)        ~( ~х)                         эквивалентно                   х

Применяя правило 1, получаем

        ~ ( ~ ( (a  =>  b)   &  (b  =>  с))  v  (а  =>   с) )

Далее, правила 2 и 4 дают

        (а  =>  b)   &  (b  =>  с)  &  ~(а   =>  с)

Трижды применив правило 1, получаем

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




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