Средства разработки приложений
Алгоритм унификации
Дадим алгоритм поиска наиболее общего унификатора для конечного множества простых выражений S. В том случае, если это множество не унифицируемо, алгоритм должен обнаруживать эту ситуацию.
Шаг 1. Полагаем k=0, ? 0=ε.
Шаг 2. Если S?k — одноэлементное множество, останавливаем алгоритм, ?k — наиболее общий унификатор для S. В противном случае строим множество рассогласований d(S?k) и переходим к третьему шагу.
Шаг 3. Если в d(S?k) существуют переменная x и терм t такие, что x не входит в t, то полагаем что ?k+1=?k{x/t}. Увеличиваем на единицу k, переходим ко второму шагу. Иначе останавливаем алгоритм, множество S не унифицируемо.
Обратите внимание, что алгоритм унификации заканчивает свою работу за конечное число шагов для любого конечного множества простых выражений, потому что на каждом проходе мы уменьшаем количество переменных. Так как множество простых выражений было конечным, то и множество различных переменных в нем конечно, и, значит, через число шагов, не превышающее количества различных переменных, алгоритм завершится.
Утверждение о том, что для любого унифицируемого конечного множества простых выражений S алгоритм унификации закончит свою работу и выдаст наиболее общий унификатор для S, называется теоремой унификации.
Теперь можно перейти к рассмотрению метода резолюций.
В чем вообще заключается задача? Мы хотим построить алгоритм, который позволял бы нам автоматически давать ответ на вопрос, может ли быть выведено некоторое заключение из множества имеющихся посылок. Известно, что в общем случае даже для логики первого порядка такой алгоритм невозможен. Как правило, формальные системы, для которых можно построить подобный разрешающий алгоритм, обладают небольшой выразительной силой. К ним, например, относится логика высказываний и логика одноместных предикатов.
Однако Робинсон решил, что правила вывода, используемые компьютером при автоматическом выводе, не обязательно должны совпадать с правилами вывода, используемыми при «человеческом» выводе.
Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий