§ 35. Логические программы.

Обозначим через PR множество всех правил A ¬ A₁, …, A_k, k ³ 0 сигнатуры W, где A, A₁, …, A_k – атомы сигнатуры W. Если атом A отсутствует, то правило ¬ A₁, …, A_k называется целью (запросом). Если k = 0, то правило A ¬ называется фактом.

Логическая программа Pr есть конечная совокупность правил. Подстановкой называется отображение q: X ® T. Подстановка q(x) = x называется тождественной. Обозначим через Q множество всех подстановок. Подстановки естественным образом распространяются на произвольные выражения. Так для терма t = f(t₁, ..., t_n) и атома A = P(t₁, ..., t_n) их подстановки соответственно равны tq = f(t₁q, ...,  t_nq), Aq = P(t₁q, ..., t_nq). Правило Aq ¬ A₁q, ..., A_nq называется вариантом правила A ¬ A₁, …, A_n если q – перестановка множества X.

Зафиксируем правило вычисления R, определяющее в каждом запросе выделенный атом. Пусть N = ¬ A₁& ... &A_i& ... &A_k, k ³ 1 запрос, в котором правилом R выделен атом A_i и A ¬ B₁& ... &B_l – вариант некоторого правила программы Pr, в котором все переменные отличны от переменных запроса. Пусть q – наиболее общий унификатор атомов A_i и A. Тогда запросы

¬ (A₁& ... &B₁& ... &B_l& ... &A_k)q, если l ³ 1; (1)

¬ (A₁& ... &A_i& ... &A_k)q, если l = 0

будем называть выводимыми из запроса N по правилу A ¬ B₁& ... &B_l с помощью подстановки q и правила вычисления R. Как видно из определения, атом A_i не удаляется из запроса при его унификации с некоторым фактом программы. Такие атомы выделяются жирным шрифтом. Будем предполагать, что правило R не выбирает для очередного шага вывода выделенные атомы.

Пространством вычислений для программы Pr и правила вычисления R называется множество всех возможных запросов сигнатуры W с заданным на нем отношением выводимости. SLDF-выводом (Linear resolution with Selection rule for Definite clauses and underlined Facts) цели N в некотором пространстве вычислений, назовем максимальную последовательность запросов N = N₀, N₁, N₂ ... вместе с последовательностью правил C₀, C₁, ... и унификаций q₀, q₁, ...,  такую что запросы N_i+1 выводимы из запросов N_i по правилам C_i с помощью подстановок q_i и правила R. SLDF-вывод – максимальный путь в пространстве вычислений, начинающийся с N. SLDF-вывод, заканчивающийся запросом, в котором все атомы выделены, называется успешным. Конечный SLDF-вывод, не являющийся успешным – тупиковым. Множество всех SLDF-выводов, начинающихся с цели N, обычно представляют в виде дерева (префикс дерева SLDF-выводов) и называют SLDF-деревом вычислений запроса N. SLDF-дерево, содержащее успешный SLDF-вывод, называется успешным.