Search code examples
algorithmprologaxiomsuccessor-arithmetics

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

Solution

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