Vamos a exponer el árbol de resolución de forma parecida al del ejemplo que mencionas. Para ello denominaremos R1, R2 y H1 a las dos reglas y al hecho dados respectivamente como base del conocimiento:
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
Así comenzamos el árbol de resolución con la primera pregunta u objetivo 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: ...
Dejo los dos últimos nodos sin resolver y la pregunta 2 como ejercicio, ya que se calculan siguiendo el proceso descrito. Como pista diré que uno de los nodos termina en fallo ya que llega a expresión a la que ya no se le puede aplicar ninguna regla y/o hecho. De todas maneras la solución completa se puede observar para comprobar el resultado en el siguiente enlace para la pregunta 1, y en éste otro para la pregunta 2.
Dichos árboles de resolución fueron generados por la herramienta JSldDraw desarrollada por A.J. Pareces García para la Universidad de Málaga. La herramienta requiere Java instalado, se ejecuta a través de un fichero por lotes '.bat' que también funciona desde Linux si lo ejecutamos en un terminal mediante:
$ sh run.bat
Hay otras herramientas similares y más información proporcionadas por la mencionada Universidad aquí. El uso de estas herramientas es muy aconsejable, ya que el proceso de construcción de los árboles de resolución puede ser engorroso cuando se dan reglas y preguntas de cierto tamaño y complejidad.
Es habitual realizar la tarea de encontrar el unificador más general de forma lógica, mediante la aplicación de la sustitución que permita aplicar una regla, pero más adecuadamente se usa el algoritmo de unificación de Robinson, del que se puede ver su funcionamiento en la misma herramienta aconsejada JSldDraw, como se observa en los siguientes ejemplos: A y B.
Comentar que en ninguno de los problemas se produce ninguna poda en el árbol por repetición. Más información sobre el proceso y Prolog puede leerse aquí.
Espero que sirva de ayuda.
Paz.