Meta-interpreting logical cut in Prolog (Edited to accommodate comments)

Question

I am implementing a geometric theorem prover in Sicstus Prolog; and in order to get over the problem of backtracking over I/O, I am using a meta-interpreter. This last however does not seem to handle cuts as expected.

My meta-interpreter looks like the following. The first argument to solve/5 is the goal to be evaluated, the second and third arguments allow me to control the search depth, and the fourth and fifth arguments are for handling backtracking over output.

solve(true,_,_, O, O) :- 
        !.
solve(_,CurrentDepth,DepthLimit, _, _) :- 
        CurrentDepth > DepthLimit, 
        !, 
        fail.
solve(nl,_,_, O, [nl|O]):- !.
solve(write(X),_,_, O, [X|O]):- !.
solve((A,B),CurrentDepth,DepthLimit, O0, O2) :- 
        !, 
        solve(A,CurrentDepth,DepthLimit, O0, O1),
        solve(B,CurrentDepth,DepthLimit, O1, O2).
solve((A;B),CurrentDepth,DepthLimit, O0, O2) :- 
        !, 
        (
                (solve(A,CurrentDepth,DepthLimit, O0, O2); 
                solve(B,CurrentDepth,DepthLimit, O0, O2))
        ).

solve(A,_,_, O, O) :-
        (
                predicate_property(A, built_in);
                predicate_property(A, imported_from(lists))
        ),
        !,
        call(A).
solve(Goal,CurrentDepth,DepthLimit, O0, O1) :-  
        !,        
        predicate_property(Goal, interpreted),!,        
        NewDepth is CurrentDepth+1,!,        
        clause(Goal,SubGoals),
        solve(SubGoals,NewDepth,DepthLimit, O0, O1).

I have followed the instructions in the thread Implementing cut in tracing meta interpreter prolog and changed the meta-interpreter to the following.

solve(true,_,_, O, O) :- 
        !.
solve(_,CurrentDepth,DepthLimit, _, _) :- 
        CurrentDepth > DepthLimit, 
        !, 
        fail.
solve(nl,_,_, O, [nl|O]):- !.
solve(write(X),_,_, O, [X|O]):- !.
solve(!, _,_,_,_):- !, ( true ; throw(cut)).
solve((A,B),CurrentDepth,DepthLimit, O0, O2) :- 
        !, 
        solve(A,CurrentDepth,DepthLimit, O0, O1),
        solve(B,CurrentDepth,DepthLimit, O1, O2).
solve((A;B),CurrentDepth,DepthLimit, O0, O2) :- 
        !, 
        (
                (solve(A,CurrentDepth,DepthLimit, O0, O2); 
                solve(B,CurrentDepth,DepthLimit, O0, O2))
        ).
solve(A,_,_, O, O) :-
        (
                predicate_property(A, built_in);
                predicate_property(A, imported_from(lists))
        ),
        !,
        call(A).
solve(Goal,CurrentDepth,DepthLimit, O0, O1) :-  
        !,        
        predicate_property(Goal, interpreted),!,        
        NewDepth is CurrentDepth+1,!,        
        clause(Goal,SubGoals),
        catch(
                (       
                        solve(SubGoals,NewDepth,DepthLimit, O0, O1)
                ),
                cut,
                fail
        ).

However now, solve/5 fails for some of the problems fed to the theorem prover. It is worth noting that I do not have any of the predicates call/1, catch/3, or throw/1 in my theorem prover. An example problem is the following.

:- dynamic test_goal/2.
:- dynamic predicate_with_small_depth/2.
:- dynamic predicate_with_large_depth/2.
:- dynamic p_1/2.
:- dynamic p_2/2.
:- dynamic p_3/2.
:- dynamic p_4/2.
:- dynamic p_5/2.

test_goal(X,Y):-
        predicate_with_small_depth(X,Y),!,
        predicate_with_large_depth(X,Y).

predicate_with_small_depth(X,Y):-
        X < Y,
        write('Small Depth Outcome 1'), nl.

predicate_with_small_depth(X,Y):-
        X > Y,
        write('Small Depth Outcome 2'), nl.

predicate_with_large_depth(X,Y):-
        p_1(X,Y).

p_1(X,Y):- p_2(X,Y).

p_2(X,Y):- p_3(X,Y).

p_3(X,Y):- p_4(X,Y).

p_4(X,Y):- p_5(X,Y).

p_5(X,Y):-    
        predicate_with_small_depth(X,Y),!,    
        write('Large Depth Outcome: '), write(X), write(' '), write(Y), nl.

If the goal solve(test_goal(1,2),0,8,O1,O2) is evaluated, Prolog's answer using the modified meta-interpreter is:

O2 = [nl,2,' ',1,'Large Depth Outcome: '|_A] ?

but the answer should be

O2 = [nl,2,' ',1,'Large Depth Outcome: ',nl,'Small Depth Outcome 1',nl,'Small Depth Outcome 1'|O1] ?

which is the one given by my meta-interpreter prior to adding the cut adaptation.

Does the new meta-interpreter implementation look correct in terms of handling the cut operator?

Many thanks.

---

EDIT

In trying to identify the problem set and way to solve the problems in the comments below the following was made apparent:

1. the TGTP contains the kind of problems that my program tackles

2. Geometric Theorem Proving by Pedro Quaresma, Days in Logic 2012, University of Evora, 6-8 February 2012

   (Gelernter's work) best capture my program.

   Slies: 27/99

and 28/99

also

The cut is necessary for me as it allows the program to stop working on alternative solutions of a given goal once one solution is found. For example, if I have

prove(X):-(p1(X),!);(p2(X),!);p3(X), if p1(X) is satisfiable, 

I do not want other solutions via p2/1 and p3/1 to be found. This saves a lot of computation.

Answer 1

The clause for cut is incorrect. The clause for cut should record the written data the same way as the clause for true. I think you want:

solve(!, _,_,O,O):- !, ( true ; throw(cut)).