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




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


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

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

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

Смысл этой формулы таков: если из  а   следует  b  и из  b  следует   с,  то из  а  следует  с.

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

        (р1  v  p2   v  ...)  &  (q1  v  q2   v  ...)
                                        &   (r1  v  r2  v  ...)   &  ...

Здесь  рi,  qi,  ri   -  элементарные утверждения или их отрицания. Конъюнктивная нормальная форма есть конъюнкция членов, называемых дизъюнктами, например (p1  v   p2    v   ...)  -  это дизъюнкт.

Любую пропозициональную формулу нетрудно преобразовать в такую форму. В нашем случае это делается следующим образом. У нас есть исходная формула

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




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