Access sCASP output through MQI/swiplserver

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("assert(mortal(X) :- man(X)).")
    answer = swipl_thread.query("scasp(mortal(X)).")


[{'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:

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

1 ?- use_module(library(scasp)).
2 ?- scasp_assert(mortal(s)).
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)
1 Like

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


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)).

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

3 ?- scasp_assert(man(socrates)).

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) ←

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).

1 Like

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.