How to show that a clause is derivable from a set of clauses in Prolog?

Using the logic programming notation, given the following clause:

C = m(P,X) <- m(Q,X), m(R,X)

It is possible to resolve the head of C with the first body literal of C' to give the substitution {P/Q',X/X'} and the clause:

D = m(P',X') <- m(Q,X'), m(R,X'), m(R',X').

How can I show this with Prolog? In other words, how can I show that you can derive D from C?

Solution

You clarified your question after my first post, but there is already some discussion below it. To prevent confusion, I will not edit it but write a second one:

There are two reasons why you cannot directly write down your problem as a prolog program:

you want to resolve without query
you want to see the resolvent of a (single) derivation step

Therefore we will encode the clause database in the predicate mi_clause which has two arguments: the head and a list with the body. The predicate clause_clause_resolvent has 6 arguments: head and body for each clause as well as for the resolvent. Here, the resolvent is the result of resolving over the head of the second clause with the first element of the body of the first clause. Doing it the other way round would also work.

mi_clause(m(_P,X), [m(_Q,X), m(_R,X)]). % your original clause, anonymous variables are prefixed with _ for compiler reasons

clause_clause_resolvent( Head1, Body1, Head2, Body2, RHead, RBody) :- 
    copy_term(clause(Head1,Body1), clause(H1,B1)), % create a variant of the first clause
    copy_term(clause(Head2,Body2), clause(H2,B2)), % same for second clause
    B1 = [H2|Rest1],                               % the prolog execution order always uses the first literal
    H1 = RHead,                                    % head of resolvent is the same (is only resolved with the query)
    append(Rest1, B2, RBody).                      % create the new body

The comments should be more or less self-explanatory: The copy_terms create variants of the input clause, otherwise you could lose resolvents. Then you pick the first element of the second clauses' body and try to unifiy. Actually, this unification is sufficient to instantiate both clauses correctly. Now we create our resolvent clause:the head of clause 1 is carried over(modulo the unifier substitution), the resolvent's body is clause 1's body without the resolved literal prepended to the body of the second clause's body.

Now try out the predicate, for instance in SWI Prolog:

?- mi_clause(H1,B1), mi_clause(H2,B2), clause_clause_resolvent(H1,B1,H2,B2,RH,RB).
H1 = m(_G1028, _G1029),
B1 = [m(_G1034, _G1029), m(_G1040, _G1029)],
H2 = m(_G1043, _G1044),
B2 = [m(_G1049, _G1044), m(_G1055, _G1044)],
RH = m(_G1068, _G1069),
RB = [m(_G1080, _G1069), m(_G1099, _G1069), m(_G1105, _G1069)].

As you can see, H1 and H2 are variants of your clause head containing fresh anonoymous variables. Still all elements of RB are of the form m(_, _G1069), obtaining a variant of the clause you expected.

If you want to check a general resolution step, replace the line B1 = [H2|Rest1] with member_of_rest(H2, B1, Rest1) and define this as:

member_of_rest(X, [X|Xs], Xs).
member_of_rest(X, [H|Xs], [H|Ys]) :-
    member_of_rest(X, Xs, Ys).

As a nice exercise you could extend the program by the deductive closure of clause_clause_resolvent to see arbitrary resolution sequences(you might want to be sure of the chaining order or you run into infinite recursions).

Have fun!