2015-04-01
564
1. Надо знать и помнить всего одно правило.
2. Применение этого правила можно автоматизировать(запрограммировать на ПК).
3.Ответы можно извлекать из унификаторов.
Недостатки:
Не гарантируется конец работы (бесконечный цикл при попытке найти доказательство). Но это бывает очень редко, так как большинство реальных задач не содержат “неразрешимых ” формул.
Общий вывод:
1. Предложения Пролога можно интерпретировать как предложения исчисления предикатов первого порядка.
(фразы Хорна)
2. Компилятор Пролога можно рассматривать как резолюционную процедуру доказательства, использующую поиск в глубину (сверху - вниз и слева – направо)
3. 
Все вычислительные задачи можно сформулировать, пользуясь только отрицанием, правилами и фактами, а те из задач, которые являются разрешимыми, можно решить с помощью общей резолюции сверху вниз.
(неразрешимыми считаем те задачи, которые не имеют опровержения)
Дополнительная информация:
Резолюция обладает важными свойствами корректности и полноты.
Резолюция корректна в том смысле, что если с ее помощью из множества допущений S1 и отрицания 
F 
выводится противоречие, то обязательно справедливо отношение S1 |-- F .
Резолюция полна в том смысле, что если справедливо S1|-F ,то противоречие непременно выводится из S1 и F .
Проблема общезначимости
Логика первого порядка только частично разрешима. Но есть алгоритмы, которые всегда устанавливают справедливость отношения S1|- F ,если оно действительно имеет место. Это значит, что если составили неразрешимую логическую программу, то есть не имеющую опровержения и подали ее на вход частично разрешимой процедуры, основанной на резолюции и реализовали на ЭВМ,то может произойти зацикливание.
Исследования подтвердили, что логика хорновских дизъюнктов является универсальным вычислительным формализмом. Ее проверили на множестве натуральных чисел, на частично рекурсивных функциях, на классе алгоритмов Маркова и тому подобное.
