Home / Questions / 158604
Accepted
I likeThatMeow
Asked: 2020-04-24 18:30:56 +0800 CST 2020-04-24 18:30:56 +0800 CST

About a resolution tree in Prolog

  • 772

Consider the following knowledge base

c(v,A,A). 

c(l(X,A),B,l(X,C)) :- c(A,B,C). 

e(X,A) :- c(B,l(X,C),A).

How to write the resolution trees corresponding to the knowledge base and the questions?

1. ?- e(X,l(p,l(q,v))).
2. ?- c(A,B,l(p,l(q,v))).

I don't understand anything, I don't know how to solve it, someone help me please.

I saw an example that I did understand, but I can't relate it to this exercise to be able to solve it.enter image description here

prolog

1 Answers

  1. Best Answer

    We are going to expose the resolution tree in a similar way to the example you mention. For this, we will call R1, R2 and H1 the two rules and the fact given respectively as the basis of knowledge:

    c(v,A,A).  %% H1

c(l(X,A),B,l(X,C)) :- c(A,B,C). %% R1

e(X,A) :- c(B,l(X,C),A). %% R2

    So we start the resolution tree with the first question or objective P1:

    Nodo 1: e(X,l(p,l(q,v))).
      | la única regla que podemos aplicar es R2
      | (única que transforma el predicado 'e')
      | para ello se aplica el unificador más general siguiente (UMG):
      |  {X1/X, A1/l(p(l(q,v))} sustitución que transforma la pregunta
      |     a la forma de R2 de la siguiente manera:
Nodo 2: c(B1,l(X,C1),l(p(l(q,v))). 
                       /        \ dos ramas, ya que es posible aplicar H1 y R1
                      /          \
     H1              /            \     R1
con siguiente UMG:  /              \
{B1/v,A2/l(p,l(q,v)),X/p,C1/l(q,v)} \  
                 /                   \ UMG:{B1/l(p,A2),B2/l(X,C1),X2/p,C2/l(q,v)} 
Nodo 3: Éxito. Resultado:{X=p}        \
                                  Nodo 4: c(A2,l(X,C1),l(q,v)).
                                     /      \
                             H1     /        \ R1
                                   /          \
                                  /            \
                           Nodo 5: ...        Nodo 6: ...

    I leave the last two nodes unsolved and question 2 as an exercise, since they are calculated following the process described. As a hint I will say that one of the nodes ends in failure since it reaches an expression to which no rule and/or fact can no longer be applied. In any case, the complete solution can be observed to check the result in the following link for question 1 , and in this one for question 2 . These resolution trees were generated by the JSldDraw tool developed by AJ Seems García for the University of Malaga. The tool requires Java installed, it is executed through a batch file '.bat' that also works from Linux if we execute it in a terminal with:

         $ sh run.bat

    There are other similar tools and more information provided by the mentioned University here . The use of these tools is highly recommended, since the process of building resolution trees can be cumbersome when rules and questions of a certain size and complexity are given. It is usual to perform the task of finding the most general unifier logically, by applying the substitution that allows a rule to be applied, but more appropriately, the Robinson unification algorithm is used , whose operation can be seen in the same tool JSldDraw is recommended, as seen in the following examples: A and B .
    Comment that in none of the problems is there any pruning of the tree by repetition. More information about the process and Prolog can be read here .

    Hope that helps. Peace.

    • 10