Home > Archive > Prolog > April 2005 > Evaluation of a subset of clauses
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
Evaluation of a subset of clauses
|
|
| Eddie Jobson 2005-04-08, 8:58 am |
| 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.
| |
| Bart Demoen 2005-04-08, 4:00 pm |
| 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
| |
| Eddie Jobson 2005-04-08, 4:00 pm |
| 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?
| |
| Bart Demoen 2005-04-08, 8:58 pm |
| Eddie Jobson wrote:
> Bart Demoen <bmd@cs.kuleuven.ac.be> wrote in message news:<1112967918.654404@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
|
|
|
|
|