Access sCASP output through MQI/swiplserver

Help!
1

I’m using the latest version of swi-prolog stable, and installing the sCASP library.

If in Python I use thread.query('scasp(mortal(X))'), I get the bindings only. The model and the justification that the scasp() predicate would provide inside the REPL are not there.

I suspect that the way the MQI is implemented it does not process any output from queries other than bindings. How can I access the output of the scasp() predicate through swiplserver?

from swiplserver import PrologMQI, PrologThread

with PrologMQI() as swipl:
  with swipl.create_thread() as swipl_thread:
    swipl_thread.query("use_module(library(scasp)).")
    swipl_thread.query("assert(mortal(X) :- man(X)).")
    swipl_thread.query("assert(man(socrates)).")
    answer = swipl_thread.query("scasp(mortal(X)).")
    print(answer)

returns

[{'X': 'socrates'}]

Right now there is an error being thrown in the scasp justification result if I use swipl in the REPL, but that’s a different problem, I suspect. :slight_smile:

2

You need to use scasp_assert(...) instead of assert/1; however there is still a problem with the justification:

1 ?- use_module(library(scasp)).
true.
2 ?- scasp_assert(mortal(s)).
true.
3 ?- scasp(mortal(X)).
X = s,
% s(CASP) model
{ mortal(s)
},
% s(CASP) justification
    [[ EXCEPTION while printing message '~W'
       with arguments [scasp_show_stack(user:'tmp-1-1089847277363607218':[[],[],o_nmr_check,[],'user:mortal'(...)],[unicode(true)]),[priority(999),quoted(true),portray(true),max_depth(10),spacing(next_argument)]]:
       raised: existence_error(procedure,'tmp-1-1089847277363607218':pr_user_predicate/1)
    ]]
.
3

Should all work fine again. Please let me know otherwise.

4

The scasp api is in flux, so don’t expect this to be permanent, but this is how you can get the output:


1 ?- use_module(library(scasp)).
true.

2 ?- scasp_assert((mortal(X) :- man(X))).
true.

3 ?- scasp_assert(man(socrates)).
true.

4 ?- scasp(mortal(X)),scasp_embed:scasp_justification(J,[]),with_output_to(string(JOut) , human_justification_tree(J,[])).
Correct to: "scasp_just_human:human_justification_tree(J,[])"? yes
X = socrates,
J = query-[(user:mortal(socrates))-[(user:man(socrates))-[]]],
JOut = "   mortal holds for socrates, because\n      man holds for socrates\n   ∎\n",
% s(CASP) model
{ man(socrates),     mortal(socrates)
},
% s(CASP) justification
query ←
   mortal(socrates) ←
      man(socrates).

Now you have the human justification in JOut and the prolog justification term in J. You can use with_output_to/2 with any goal that prints to current_output (usually stdout).

5

With the exception that the correction can’t happen through the MQI, that has solved my problem, thank you!

How would I look at the output of scasp_json_results in this method? My first few guesses are off the mark.