Метод резолюции требует, чтобы делались подстановки в дизъюнкты так, чтобы две литеры с противоположными знаками содержали совпадающие атомы. Так как эти атомы могут содержать переменные, можно делать и дальнейшие подстановки вместо них, а литеры по-прежнему будут отличаться только знаками Процесс нахождения наиболее общей подстановки, делающей две литеры контрарными, называется унификацией. Рассмотрим унификацию двух литер.
Р(а, х, f(g(у)) и ~Р(z, f(z),f(u)).
Постепенно строим подстановку S. которая представляет собой набор пар вида (t/х), где t - терм, х - переменная, вместо которой он будет подставлен. Вот еще пример: S={harry/х, z/w}. В общем случае пишем S={t1/v1, t2/v2,...}, где vi - попарно различные переменные и каждый терм ti отличен от своей переменной vi. Идем слева направо, отыскивая пары термов, которые не совпадают друг с другом. Так последовательно получаем:
Совместить Р(а,х,f(g(у)) с ~Р(z,f(z),f(u))
S={a/z} Совместить Р(а,х,f(g(у)) с ~Р(а,f(а),f(u))
S={a/z,f(a)/x} Совместить Р(а,f(а),f(g(у))) с
~Р(а,f(а),f(u))
S={a/z,f(a)/x,g(y)/u} Совместить Р(а,f(а),f(g(у))) с
~Р(а,f(a),f(g(y))).
Этот метод дает наиболее общий унификатор. Были сделали подстановки вместо z,x, и u но не меняли у. Более ограничительная подстановка может иметь вид
S={a/z, f(a)/x, g(y)/u, a/y}, что дает Р(а, f(а),f(g(a))).
Этот процесс играет важную роль в языке Пролог, так как он обобщает механизм вызова процедур, используемый в обычных языках программирования. Обычно аргументы вызова процедуры - это выражения, которые подставляются вместо формальных параметров и могут быть только именами переменных. Однако в Прологе разрешается, чтобы сами формальные параметры были термами, и потому процесс вызова "логической процедуры" включает совмещение термов, являющихся аргументами вызова, с термами из заголовка процедуры с помощью метода унификации. Если унификация оканчивается неудачей из-за того, что никакая подстановка не сможет совместить нужные литеры, то вызова не произойдет, но будет сделана попытка совмещения с другим определением процедуры, если таковое имеется.
Исчисление предикатов дает возможность выразить многое из того, о чем хотели бы говорить или рассуждать. Используя предикаты, кванторы, переменные и функциональные символы, можно выразить весьма сложные утверждения; простые факты записать в виде атомов, состоящих из предикатов с константами в качестве аргументов. Таким образом, можно выражать различные знания, как общие аксиомы, так и факты, в рамках единого формализма, что важно для экспертных систем.
При автоматизации вывода доказательств методами исчисления предикатов требуется определить ряд процедур для выбора правил, позволяющих предотвратить комбинаторный взрыв и обеспечить проведение немонотонных рассуждений. При этом наметилось два подхода.
При первом подходе к решению задачи управления, нашедшем широкое распространение в приложениях концепции искусственного интеллекта, отбрасывался принцип универсальности и производился поиск методов обработки данных, эффективных для решения конкретных задач в пределах определенной предметной области. Источником высокой эффективности этих методов служат введенные в систему обширные знания в конкретной предметной области и следование наблюдаемому факту, заключающемуся в том, что человек, выступающий в роли эксперта- решателя задач, очень редко пользуется процедурами общего характера, достигая успеха за счет хорошего “знания” содержания задачи. С целью упростить процесс программирования для таких “основанных на знаниях” систем были разработаны соответствующие формализмы, обладающие меньшими выразительными возможностями, чем исчисление предикатов, но более удобные для реализации на ЭВМ. Многие подобные приемы были разработаны с использованием средств языка обработки списков- Лисп.
Второй подход, развиваемый в рамках традиционной логики, был направлен на сохранение универсальности, свойственной исчислению предикатов, путем выявления процедур вывода доказательств, универсальных по своему характеру и в то же время позволяющие обойти проблему выбора правил и комбинаторного взрыва. Этот подход в основном представляет интерес для самой логики, в частности, при разработке методов автоматизации вывода доказательств (названного “доказательством теорем”). Для этого и был разработан язык программирования Пролог, представляющий собой комбинацию одного из методов доказательства теорем- “метода резолюции” и исключительно эффективной стратегии управления.
Увидели также, каким образом утверждения исчисления предикатов приводятся к нормальной форме и как использовать метод резолюции для доказательства их истинности и нахождения значений переменных (связанных кванторами существования), которые удовлетворяют этим утверждениям. Эти методы составляют также основу языка Пролог.
