Showing proofs involving clpr constraints in Swish

Help!
1

Hi!

My problem is that I would like to be able to show proofs for queries that involve clpr constraints in swish. I got some very useful suggestions from people here and on SO for constructing a meta-interpreter (thank you!) that does this (see this related question). But sandbox limitations in swish won’t allow using call/1 on goals that are clpr constraints so such a meta-interpreter does not work for use on swish. On swish, this program (with the query ?-prove(p(X, fire), Proof)) returns a Sandbox limitation error (on regular Prolog this works great though).

:-use_module(library(clpr)).

p(1, johnWasTired).
p(1, presenceOfFlammableMaterial).

p(X1, johnDroppedAMatch):-
    p(X2, johnWasTired),
    {X1 = 0.5 * X2}.

p(X1, fire):-
    p(X2, presenceOfFlammableMaterial),
    p(X3, johnDroppedAMatch),
    {X1 = 0.7 * X2 * X3}.

prove(true, true):- !.
prove((G1, G2), (P1, P2)):- !, prove(G1, P1), prove(G2, P2).
prove((G1; _), P1):- prove(G1, P1).
prove((_; G2), P2):- prove(G2, P2).
prove(G, P):- G = {_}, !, call(G), P = subproof(G, true).
prove(H, subproof(H, Subproof)):- clause(H, Body), prove(Body, Subproof).

I know that i can use trace/0 on swish, and i personally really like it, but i would like my end users to get something more human readable that i can output with format/2. Such as:

p(0.35,fire) <=
     p(1,presenceOfFlammableMaterial) <= TRUE
     p(0.5,johnDroppedAMatch) <=
          p(1,johnWasTired) <= TRUE
          {0.5=0.5*1} <= TRUE
     {0.35=0.7*1*0.5} <= TRUE

Any suggestions would be greatly appreciated! I want my finished product to be easily accessible so swish is ideal for me. I have been looking at cplint but this does not work for me since the term expansions and goal expansions i use clash with cplint. Also i don’t want to put antecedents and consequents in a single predicate (e.g. implies([flammable, johnDroppedMatch], fire)) because i really like the clean and simple typical prolog representation with the consequent in the head and all antecedents in the body.

Kind regards, JCR

1 Like