Реализация метода резолюций в языке Пролог

Самая высокая степень понимания алгоритма доказательства теоремы может быть достигнута в том случае, когда описание каждого шага алгоритма иллюстрируется соответствующими действиями на конкретном примере, полнота которого позволяет отразить все тонкости алгоритма.

Рассмотрим работу алгоритма доказательства теорем методом резолюций на примере известной задачи о родственных отношениях[7]. В качестве машинной реализации будет использована Турбо-версия языка Пролог[15,16], в которой допускается запись предикатов на русском языке. Рисунок 4.1 отображает отношения родителей и детей, причем по той причине, что в языке Пролог константы начинаются со строчной буквы, все имена на рисунке так и представлены.

Рис. 4.1. Дерево родственных отношений.

Тот факт, что Том является родителем Боба, можно записать на Прологе так: родитель(том,боб).

Здесь мы выбрали родитель в качестве отношения (предиката), а том и боб являются аргументами этого отношения. В пролог-программе в разделе domains аргументы предиката родитель и ниже описанного предиката предок описаны как атомы символьного типа (symbol). В разделе clauses программы непосредственно по дереву родственных отношений записаны все имеющиеся факты, а также два правила для определения предиката предок, пояснения которых будут даны позднее.