Аксиома разрешение

Question

Я пытаюсь понять, как работает разрешение аксиомы в прологе.

Давайте предположим, что я определяю две основные операции над натуральными числами:

• s (термин)(обозначает преемника) и

• add (term, anotherTerm).

Семантика добавления задается как

• add (0, x1) -> x1

• add (x1, 0) -> x1

• add (s (x1), y1) -> s (добавьте (x1, y1))

Затем я хотел бы решить уравнение

add (x, add(y, z)) = s (0)

Я полагаю, что одной стратегией может быть

• проверка, если правая часть (RHS) уравненияравно его левой стороне (LHS)

• , если не видите, можно ли найти решение, ища наиболее общий объединитель

• , еслиНе пытайтесь найти аксиому, которая может быть использована в этом уравнении.Стратегия для выполнения этой работы может заключаться в том, чтобы (для каждой аксиомы): попытаться решить RHS уравнения, равного RHS аксиомы.Если есть решение, то попытайтесь решить LHS уравнения, равного LHS аксиомы.Если это удастся, то мы нашли правильную аксиому.

• в конце концов, если нет решения и LHS и RHS уравнения - это одна и та же операция (т.е. одна и та же сигнатура, но не одна и та же)операнды), примените алгоритм к каждому операнду, и решение будет найдено, если решение найдено для каждого операнда.

Я думаю, что этот (простой) алгоритм может работать.Тем не менее, я хотел бы знать, есть ли у кого-нибудь опыт решения такого рода проблем?Кто-нибудь знает, где я могу найти документацию о лучшем алгоритме?

Заранее спасибо

Answer 1

Программа Prolog - это набор предикатов.

Предикат - это набор предложений.

Предложение имеет форму

Head :- Body.

, означающее "Head истина, если Body истина ".

Существует сокращенная форма предложения

Head.

, которая означает то же самое, что и

Head :- true.

, где trueявляется встроенной функцией, которая всегда верна.

Возвращаясь к части Body предложения, Body - это цель, которая может принимать одну из следующих форм (A, B иC обозначает произвольные цели):

Atom            % This is true if Atom is true (see below).
A, B            % This is true if A is true and B is true.
(A ; B)         % This is true if A is true or B is true.
\+ A            % This is true if A is not true.
(A -> B ; C)    % If A is true then B must be true, else C must be true.

В Прологе есть некоторые особые правила, касающиеся порядка оценки (слева направо) и «срезов» (которые сокращают дерево поиска), но это тонкая деталь, котораявыходит за рамки этого краткого руководства.

Теперь, чтобы решить, является ли Atom истинным, Atom может иметь одну из следующих форм (X и Y обозначают произвольные термины):

true                % or some other builtin with given truth rules.
X = Y               % True if X and Y are successfully unified.
p(X, Y, ...)        % True if p(X, Y, ...) matches the head of some clause
                    % and the Body is true.

Термин - это, по сути, любой фрагмент синтаксиса.

Ключевым моментом здесь является то, что ПрологНет функций!Где на функциональном языке вы можете определить функцию add(X, Y), которая оценивается как сумма X и Y, в Прологе вы определяете предикат с головой add(X, Y, Z), который, в случае успеха, объединяет Z стермин, обозначающий сумму X и Y.

Учитывая все это, мы можем определить ваши правила в Прологе следующим образом:

add(0, Y, Y).                        % 0 + Y = Y.
add(Y, 0, Y).                        % Y + 0 = Y.
add(s(X), Y, s(Z)) :- add(X, Y, Z).  % s(X) + Y = s(X + Y).

, где я использую 0 для обозначения нуля (!) и s(X) для обозначения преемника X.

Рассмотрим оценку add(s(s(0)), s(0), Z):

add(s(s(0)), s(0), Z)                 % Only the third head for add matches, so...
---> Z = s(Z0), add(s(0), s(0), Z0).

add(s(0), s(0), Z0)                   % Only the third head for add matches, so...
---> Z0 = s(Z1), add(0, s(0), Z1).

add(0, s(0), Z1)                      % Only the first head for add matches, so...
---> Z1 = s(0).

Соединение всех этих объединений для Z вместе, у нас есть Z = s(s(s(0))).

Теперь вы можете спросить «что произойдет, если в предложении будет найдено более одной головы» или «что произойдет, если путь оценки потерпит неудачу?», на что даны ответы «недетерминизм»"," backtracking "и, вообще, прочитайте учебник Пролога!

Надеюсь, это поможет.

Answer 2

То, что вы ищете, называется сужение .Он реализован на некоторых языках функциональной логики, таких как Curry , но не в самом Прологе.

Answer 3

«Представление и обоснование знаний» Брахмана и Левеска дает довольно хорошее представление о том, как эти вещи работают.