Введение
1 Решение систем уравнений в языке первого порядка 12
1.1 Язык первого порядка 12
1.2 Канонизатор 13
1.3 Алгоритм решения уравнений 17
2 Решение систем уравнений в языке второго порядка 25
2.1 Язык второго порядка 25
2.2 Канонизатор для языка второго порядка 29
2.3 Канонизатор для языка первого порядка в расширенной сигнатуре 34
2.4 Решения уравнений с функциональными переменными 38
2.5 Построение согласованных подстановок 43
2.6 Алгоритм унификации 48
2.7 Вычисление а 57
2.8 Условная унификация 64
3 Выполнимость и унифицируемость 68
3.1 Модели первого порядка 68
3.2 Модели второго порядка 70
3.3 Операция mod
