How to find facts that do not have contribution in goal

Question

I'm trying to write a program that can check if the student program can fulfill a certain goal or not. I can do that part. Now, I want to check if the student program actually contains unnecessary code or not. For solving this case, I think I need to know if the student program contains facts that do not contribute to the specified goal. However, I cannot figure it out, how to find facts that do not contribute to the goal.

To make it easier to understand, let's consider a simpler example. In this example, the specified goal is: is john the grandfather of tomy?

father(john, jim).
father(jim, tomy).
father(john, david).
father(bruce, anne).
mother(mary, jim).

grandfather(A,B) :- father(A, X), father(X,B).

goal:- grandfather(john, tomy).

Actually the goal can be satisfied by the following facts only:

father(john, jim).
father(jim, tomy).

And the things that I want to know is which facts that actually do not contribute to the goal. The answer would be all the following facts:

father(john, david).
father(bruce, anne).
mother(mary, jim).

Any help is really appreciated. Thanks

Answer 1

Your question cannot be directly answered in Prolog, but you can answer it manually by using a failure-slice. Simply add false goals into your program and always test whether goal still succeeds. Here is the minimal program I obtained.

father(john, jim).
father(jim, tomy).
father(john, david) :-  false.
father(bruce, anne) :- false.
mother(mary, jim) :- false.

grandfather(A,B) :- father(A, X), father(X,B).

goal:- grandfather(john, tomy).

Every time you insert a goal false into a pure, monotonic program, you know for sure that the set of solutions is reduced (or stays the same). So finding such a slice involves about as many trials as there are places to set such goals. Sometimes you might want to add goals X = term to narrow down the program even further.

Failure slices are particularly useful when you want to understand the termination properties of a program, see failure-slice for more.

Answer 2

Unbelievably, there is a partial solution to this problem here. To reproduce the relevant portion here is substantial code, so let me make it clear that this is not my own work, I am just including the work here in case the website above goes missing in the future.

First, you need a meta-circular interpreter:

mi_circ(true).
mi_circ((A,B)) :-
    mi_circ(A),
    mi_circ(B).
mi_circ(clause(A,B)) :-
    clause(A,B).
mi_circ(A \= B) :-
    A \= B.
mi_circ(G) :-
    G \= true,
    G \= (_,_),
    G \= (_\=_),
    G \= clause(_,_),
    clause(G, Body),
    mi_circ(Body).

This works for \=/2 and clause/2. To generalize this pattern to all built-in predicates, we can use predicate_property/2 to identify them as such for calling them directly:

provable(true, _) :- !.
provable((G1,G2), Defs) :- !,
    provable(G1, Defs),
    provable(G2, Defs).
provable(BI, _) :-
    predicate_property(BI, built_in),
    !,
    call(BI).
provable(Goal, Defs) :-
    member(Def, Defs),
    copy_term(Def, Goal-Body),
    provable(Body, Defs).

This gives you a reified meta-interpreter, meaning you can pass provable/2 a goal and a set of definitions and it will tell you whether the definitions supplied are sufficient to prove the goal. I bet you can taste how close we are to the final solution now!

With the following additional definitions, we can use this MI to identify redundant facts in some predicate definitions:

redundant(Functor/Arity, Reds) :-
    functor(Term, Functor, Arity),
    findall(Term-Body, clause(Term, Body), Defs),
    setof(Red, Defs^redundant_(Defs, Red), Reds).

redundant_(Defs, Fact) :-
    select(Fact-true, Defs, Rest),
    once(provable(Fact, Rest)).

This is using select/3 to portion out one definition at a time and see if the predicate is still provable. By doing that across all the definitions you can get the set of all unnecessary rules.

Given the definitions:

as([]).
as([a]).   % redundant
as([a,a]). % redundant
as([A|As]) :-
    A = a,           % test built-in =/2
    5 is 2 + 3,      % test built-in is/2
    1 > 0,           % test built-in >/2
    as(As).

we can ask for facts which are deducible from all (respective) remaining clauses and hence redundant:

?- redundant(as/1, Reds).
Reds = [as([a]), as([a, a])]

Alas, this does not work out-of-the-box on your problem, but I do think that with some study you could find a way to apply this technique to it and come up with something. For instance, you could create a meta-interpreter that takes a list of facts to check and perform the same sort of remove-one-then-prove loop to find them.

Hope this helps and is at least interesting.

Answer 3

Another option is to modify and use a unit testing framework that does predicate clause coverage. Define a unit test with the goal for which you want to find out which clauses don't contribute to it. The modifying bit, if necessary, will be to modify the coverage report to also identify those clauses. Just as an example of what I mean, in case it's not clear, consider the following output of the Logtalk lgtunit tool using one of the examples in the Logtalk distribution:

?- {ack(tester)}.
% 
% tests started at 2013/6/5, 19:54:9
% running tests from object tests
% file: /Users/pmoura/logtalk/examples/ack/tests.lgt
% ack_1: success
% ack_2: success
% ack_3: success
% 3 tests: 0 skipped, 3 passed, 0 failed
% completed tests from object tests
% ack: ack/3 - [1,2,3] (3/3)
% 1 unit declared in the test file containing 3 clauses
% 1 unit covered containing 3 clauses
% 3 out of 3 clauses covered, 100,000000% coverage
% tests ended at 2013/6/5, 19:54:9
% 
true.

The line:

% ack: ack/3 - [1,2,3] (3/3)

shows which clauses were used by the three unit tests for the ack/3 predicate.