Determinism error in s(CASP) human_justification_tree

General
1

I’m using s(CASP) through SwiplServer, and running the following code:

:- use_module(library(scasp)).
:- style_check(-discontiguous).
:- style_check(-singleton).
:- set_prolog_flag(scasp_unknown, fail).

#pred bird(X) :: '@(X) is a bird'.
#pred according_to(R,bird(X)) :: 'according to @(R), @(X) is a bird'.
#pred legally_holds(_,bird(X)) :: 'it legally holds that @(X) is a bird'.
#pred penguin(X) :: '@(X) is a penguin'.
#pred according_to(R,penguin(X)) :: 'according to @(R), @(X) is a penguin'.
#pred legally_holds(_,penguin(X)) :: 'it legally holds that @(X) is a penguin'.
bird(X) :-
penguin(X).

#pred thing(X) :: '@(X) is a thing'.
#pred according_to(R,thing(X)) :: 'according to @(R), @(X) is a thing'.
#pred legally_holds(_,thing(X)) :: 'it legally holds that @(X) is a thing'.
#pred flies(Y,X) :: 'it is @(X) that @(Y) flies'.
#pred according_to(R,flies(Y,X)) :: 'according to @(R), it is @(X) that @(Y) flies'.
#pred legally_holds(_,flies(Y,X)) :: 'it legally holds that it is @(X) that @(Y) flies'.


according_to( ba__2_end,flies(A,true)) :-
bird(A).

overrules(ba__3_end,ba__2_end).
opposes(  flies(A,true),  flies(A,false)).
opposes(  flies(A,false),  flies(A,true)).

according_to( ba__3_end,flies(A,false)) :-
penguin(A).

penguin(tweety).

#pred overrules(R1,R2) :: 'the conclusion in @(R1) overrules the conclusion in @(R2)'.
#pred opposes(C1,C2) :: 'the conclusion @(C1) opposes the conclusion @(C2)'.
#pred defeated(R,_) :: 'the conclusion in @(R) is defeated'.
#pred refuted(R,_) :: 'the conclusion in @(R) is refuted'.

refuted(R,C) :-
    opposes(C,OC),
    overrules(OR,R),
    according_to(OR,OC).

defeated(R,C) :-
    refuted(R,C).

legally_holds(R,C) :-
    according_to(R,C),
    not defeated(R,C).


%?- scasp(legally_holds(_,flies(tweety,A)),[tree(Tree)]),with_output_to(string(Human), human_justification_tree(Tree,[])).

The code works properly if run on swish. But if you run it through SwiplServer, or at the Prolog top-level, you get a determinism error on human_justification_tree.

The response at top-level is:

?- scasp(legally_holds(_,flies(tweety,A)),[tree(Tree)]),with_output_to(string(Human), human_justification_tree(Tree,[])).
Correct to: "scasp_just_human:human_justification_tree(Tree,[])"? 
Please answer 'y' or 'n'? yes
ERROR: Deterministic procedure scasp_just_human:human_justification_tree/2 failed
ERROR: In:
ERROR:   [11] with_output_to(string(_19662),scasp_just_human:human_justification_tree(...,[]))
ERROR:   [10] '<meta-call>'('<garbage_collected>') <foreign>
ERROR:    [9] toplevel_call('<garbage_collected>') at /usr/lib/swi-prolog/boot/toplevel.pl:1162
   Call: (12) modules:destroy_module('tmp-1-3739224655756611777') ? Unknown option (h for help)
   Call: (12) modules:destroy_module('tmp-1-3739224655756611777') ? creep
^  Call: (13) retractall(system:'$load_context_module'(_24636, 'tmp-1-3739224655756611777', _24640)) ? creep
^  Exit: (13) retractall(system:'$load_context_module'(_24636, 'tmp-1-3739224655756611777', _24640)) ? creep
   Exit: (12) modules:destroy_module('tmp-1-3739224655756611777') ? creep
?-

The query runs and behaves properly if it is just ?- scasp(legally_holds(_,flies(tweety,A))).

I’m using swipl 8.5.9 and the latest version of the s(CASP) library.

2

The interface is still a bit clumsy :frowning: There is a predicate ovar_analyze_term/1 from library(scasp/output) that one needs to call on the term one wants to emit which you pass the query variables and one of or both the model and tree (the things you want to print). That annotates variable names and whether or not they appear once or multiple times. You get the correct result e.g. using

:- use_module(library(scasp)).
:- use_module(library(scasp/human)).
:- use_module(library(scasp/output)).

run :-
    Query = legally_holds(_,flies(tweety,A)),
    run(Query, Human),
    format('Got ~p~nBecause~n~s', [Query, Human]).

:- meta_predicate
    run(0,-).

run(Query, Human) :-
    scasp(Query,[tree(Tree)]),
    ovar_analyze_term(t(A, Tree)),
    with_output_to(string(Human),
                   human_justification_tree(Tree,[])).

Please do not consider this interface final …

1 Like
3

Nothing I’m writing is remotely good enough to bother waiting for final interfaces. :slight_smile:

Clumsy is just fine. Thanks for the help!

4

So close!

I am able to get your proposed solution to work in the Prolog top level, but I need it to work in Swiplserver in a way where the contents of Human are returned to the Python code. So I’m using the body of of your run/2 definition as the query, which also works in Prolog top-level. But when I do it in swiplserver, it seems to go into an infinite loop, or something.

I’m treading new ground trying to troubleshoot anybody else’s code, so I thought I’d post it here in case it’s a straightforward problem from anyone else’s perspective. I’ll follow up if I can narrow down the problem any more.

The file test.pl contains the following:

:- use_module(library(scasp)).
:- use_module(library(scasp/human)).
:- use_module(library(scasp/output)).

#pred overrules(R1,R2) :: 'the conclusion in @(R1) overrules the conclusion in @(R2)'.
#pred opposes(C1,C2) :: 'the conclusion @(C1) opposes the conclusion @(C2)'.
#pred defeated(R,_) :: 'the conclusion in @(R) is defeated'.
#pred refuted(R,_) :: 'the conclusion in @(R) is refuted'.

refuted(R,C) :-
    opposes(C,OC),
    overrules(OR,R),
    according_to(OR,OC).

defeated(R,C) :-
    refuted(R,C).

legally_holds(R,C) :-
    according_to(R,C),
    not defeated(R,C). 

#pred bird(X) :: '@(X) is a bird'.
#pred according_to(R,bird(X)) :: 'according to @(R), @(X) is a bird'.
#pred legally_holds(_,bird(X)) :: 'it legally holds that @(X) is a bird'.
#pred penguin(X) :: '@(X) is a penguin'.
#pred according_to(R,penguin(X)) :: 'according to @(R), @(X) is a penguin'.
#pred legally_holds(_,penguin(X)) :: 'it legally holds that @(X) is a penguin'.
bird(X) :-
penguin(X).

#pred thing(X) :: '@(X) is a thing'.
#pred according_to(R,thing(X)) :: 'according to @(R), @(X) is a thing'.
#pred legally_holds(_,thing(X)) :: 'it legally holds that @(X) is a thing'.
#pred flies(Y,X) :: 'it is @(X) that @(Y) flies'.
#pred according_to(R,flies(Y,X)) :: 'according to @(R), it is @(X) that @(Y) flies'.
#pred legally_holds(_,flies(Y,X)) :: 'it legally holds that it is @(X) that @(Y) flies'.


according_to( ba__2_end,flies(A,true)) :-
bird(A).

overrules(ba__3_end,ba__2_end).
opposes(  flies(A,true),  flies(A,false)).
opposes(  flies(A,false),  flies(A,true)).

according_to( ba__3_end,flies(A,false)) :-
penguin(A).

penguin(tweety).

The python code I’m running is this:

from swiplserver import PrologMQI

with PrologMQI() as swipl:
    with swipl.create_thread() as swipl_thread:
        test1 = swipl_thread.query("['/path/to/test.pl'].")
        test2 = swipl_thread.query("scasp(legally_holds(_,flies(tweety,A)),[tree(Tree)]),ovar_analyze_term(t(A, Tree)),with_output_to(string(Human),human_justification_tree(Tree,[])).")

It just stalls on the second query.

I’m assuming (once it’s working through swiplserver) that it will be necessary to detect all of the variables being used in the query, and add an ovar_analyze_term(t(VariableName,Tree)) for each. Let me know if I’m misunderstanding that.

5

It seems that the infinite loop is happening at line 891 of prologmqi.py, because the call to self._socket.recv(4096) is returning nothing. No idea why that might be.

Note that if I include the code you gave me above in test.pl, and change the last line of the python to

test2 = swipl_thread.query("run.")

then it runs, but the answer that swiplserver returns in test2 is True.

6

Never mind. I have got it working by using your code and converting run/0 to run2(Query,Human), and calling run2(Q,H) instead.

Thanks again!

1 Like