Родитель(имя,имя)

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

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

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

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

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

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

Текст пролог-программы:

domains% Раздел доменов

имя=symbol

predicates% Раздел предикатов