Evaluation of a subset of clauses

Another newbie question for you...

In my program I have to extract/create some clauses, and prove goals
against this 'fresh' set of clauses. For this purpose I extended the
classic 'Vanilla' meta-interpreter


solve(true).
solve((A,B)) :- solve(A), solve(B).
solve(A) :- clause(A,B), solve(B).


obtaining (Prg is obviously a list of clauses)


sub_solve(true, Prg).

sub_solve( (G1, G2), Prg) :-
sub_solve(G1, Prg),
sub_solve(G2, Prg).

sub_solve(Goal, Prg) :-
member(Clause, Prg),
sub_unify(Goal, Clause, Rest),
sub_solve(Rest, Prg).

sub_unify(Goal, (A :- B), Rest) :-
Goal =.. L1,
A =.. L2,
are_equal(L1, L2),
Rest = B.

are_equal([],[]).

are_equal([H1 | L1], [H2 | L2]) :-
H1 = H2,
are_equal(L1, L2).


Is this correct? Thanks in advance.

Eddie Jobson wrote:

> sub_solve(true, Prg).
>
> sub_solve( (G1, G2), Prg) :-
>    sub_solve(G1, Prg),
>    sub_solve(G2, Prg).
>
> sub_solve(Goal, Prg) :-
>    member(Clause, Prg),
>    sub_unify(Goal, Clause, Rest),
>    sub_solve(Rest, Prg).
>
> sub_unify(Goal, (A :- B), Rest) :-
>    Goal =.. L1,
>    A =.. L2,
>    are_equal(L1, L2),
>    Rest = B.
>
> are_equal([],[]).
>
> are_equal([H1 | L1], [H2 | L2]) :-
>    H1 = H2,
>    are_equal(L1, L2).
>
>
> Is this correct? Thanks in advance.

Prolog uses a renamed clause at each resolution step.
The built-in clause/2 does such renaming for you.
But member/2 doesn't, so you must do it yourself;
just before calling sub_unify would be a good place.

Why can't you define sub_unify as follows ...


sub_unify(Goal, (Goal :- Body), Body).

?

Cheers

Bart Demoen

Bart Demoen <bmd@cs.kuleuven.ac.be> wrote in message news:<1112967918.654404
@seven.kulnet.kuleuven.ac.be>...

> Prolog uses a renamed clause at each resolution step.
> The built-in clause/2 does such renaming for you.
> But member/2 doesn't, so you must do it yourself;
> just before calling sub_unify would be a good place.

Sorry Bart, I don't understand what I've to do :-(
Can you give me more hints, please?

Eddie Jobson wrote:
> Bart Demoen <bmd@cs.kuleuven.ac.be> wrote in message news:<1112967918.6544
04@seven.kulnet.kuleuven.ac.be>...
>
> 
>
>
> Sorry Bart, I don't understand what I've to do :-(
> Can you give me more hints, please?

Read about resolution.
Read about copy_term/2.

Think about the query ?- f(1), f(2).
when the program consists of only one clause: f(X).
Should the query succeed ? Does it with your metainterpreter ? What is
required to make it succeed ?

Cheers

Bart Demoen