Axiom resolution

I try to understand how axiom resolution works in prolog.

Let's assume that I define the two basic operations on the natural numbers:

• s(term) (stands for successor) and

• add(term, anotherTerm).

The semantic of add is given by

• add (0, x1) -> x1

• add (x1, 0) -> x1

• add(s(x1), y1) -> s(add(x1, y1))

Then, I would like to solve the equation

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

I imagine that one strategy could be to

• test if the right hand side (RHS) of the equation is equal to its left hand side (LHS)

• if not see if a solution can be find by looking for the most general unifier

• if not then try to find an axiom which can be used in this equation. A strategy for doing this job could be to (for each axiom): try to solve the RHS of the equation equals to the RHS of the axiom. If there is开发者_如何学Go a solution then try to solve the LHS of the equation equals to the LHS of the axiom. If it succeeds, then we have found the right axiom.

• eventually, if there is no solution and the LHS and RHS of the equation are the same operation (i.e. same signature but not same operands), apply the algorithm on each operand and a solution is found if a solution is found for each operand.

I think that this (simple) algorithm may work. However, I would like to know if anyone has experience solving this kind of problem? Does anyone know where I can find some documentation about a better algorithm?

Thanks in advance

---

A Prolog program is a collection of predicates.

A predicate is a collection of clauses.

A clause has the form

Head :- Body.

meaning "Head is true if Body is true".

There is a shorthand clause form

Head.

which means the same as

Head :- true.

where true is a builtin that is always true.

Going back to the Body part of a clause, Body is a goal which can take one of the following forms (A, B, and C denote arbitrary goals):

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.

There are some special rules in Prolog concerning evaluation order (left to right) and "cuts" (which prune the search tree), but that's fine detail which is beyond the scope of this brief tutorial.

Now, to decide whether an Atom is true, Atom can be one of the following forms (X and Y denote arbitrary terms):

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.

A term is, essentially, any piece of syntax.

The key thing to spot here is that Prolog has no functions! Where in a functional language you might define a function add(X, Y) which evaluates to the sum of X and Y, in Prolog you define a predicate whose head is add(X, Y, Z) which, if it succeeds, unifies Z with the term denoting the sum of X and Y.

Given all that, we can define your rules in Prolog as follows:

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).

where I'm using 0 to denote zero (!) and s(X) to denote the successor of X.

Consider evaluating 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).

Putting all those unifications for Z together, we have Z = s(s(s(0))).

Now, you may ask "what happens if more than one head matches in a clause" or "what happens if an evaluation path fails?", to which the answers are "nondeterminism", "backtracking", and, in general, read a Prolog textbook!

Hope this helps.

---

What you are looking for is called narrowing. It is implemented in some functional-logic languages such as Curry, but not in Prolog itself.

---

"Knowledge representation and reasoning" by Brachmann and Levesque gives a fairly good introduction to how these things work.