SWI-Prolog port (swipl branch)

This is a fork from https://gitlab.software.imdea.org/ciao-lang/sCASP. It provides a port of s(CASP) to SWI-Prolog.

About the SWI-Prolog port

The SWI-Prolog port is fully functional and from the solver prespective fully compatible with the Ciao original. The SWI-Prolog port provides two significant optimizations: (1) a more low level implementation for the term copying required for forall constructs that result from dual rules for clauses that introduce variables in the body as well as for global constraint and (2) an index to speedup finding loops and already proved literals. This often leads to about 10 times better performance.

Running requires SWI-Prolog 8.5.6 or later. The scasp executable can be build on POSIX systems by running make in the toplevel of the sCASP directory. On Windows

• Add the bin directory of SWI-Prolog to %PATH%, so you can run swipl.exe and the swipl DLLs can be found.

• run this to create scasp.exe

  swipl.exe --no-pce --undefined=error -O -o scasp -c prolog/scasp/main.pl

The command line arguments are similar, but with small differences due to the use of SWI-Prolog's commandline parser. Run scasp -h for details. The output is different, using Unicode and, if possible, color to simplify reading the model and justification.

The pack also provides scasp as a SWI-Prolog app. After installing the pack, scasp can be executed as below, i.e., replacing scasp with swipl scasp.

swipl scasp [option ...] file ...

Using scasp as an app is more portable, but as the app needs to load sCASP at runtime, it starts considerably slower than the executable generated above.

Using s(CASP) as a Prolog library

Next to using the s(CASP) executable, s(CASP) can be used as a library. For this, activate the sCASP directory as a SWI-Prolog add on by starting SWI-Prolog in the top directory and run

?- pack_install(.).

Now you can load scasp using

:- use_module(library(scasp)).

Running s(CASP) queries take a normal Prolog program that can be made available in the usual way: by consulting a file, asserting, etc. The program must respect the sCASP restrictions. Using any built-in or control structure that is not known to s(CASP) results in an error.

From the toplevel REPL loop, s(CASP) queries are executed by prefixing them with one of the 7 operators below.

| Op | Description | |------|-----------------------------------------------| | ?-- | Prove and only show the bindings | | ?+- | Prove, show bindings and model | | ?-+ | Prove, show bindings and justification (tree) | | ?++ | Prove, show bindings model and justification) | | ??+- | As above, but using human language output | | ??-+ | | | ??++ | |

? and ?? are backward compatible aliases for ?+- and ?++. For example, this shows the model.

?- ? p(X).

The predicate scasp/2 can be used to get access to the model and tree to reason about them. For example, this returns the model as a list of terms and the justification as a tree structure.

?- scasp(goal(X), [model(M), tree(T)]).

SWI-Prolog s(CASP) can also be used in your browser using SWISH.

Finally, there is a simple web server. This server can also be deployed locally using the command below. Add -h for options.

swipl examples/dyncall/http.pl

The web server lets you post s(CASP) programs and get their results as HTML or JSON. See Help for details.

Calling Prolog from s(CASP)

The SWI-Prolog port allows sCASP to call out to Prolog. This is achieved by declaring a predicate as prolog. Prolog code may be executed in two modes:

• justified (default) <br> In this case the predicate is handled by a meta-interpreter that extends the sCASP justification tree. The meta interpreter can deal with cuts, (If->Then;Else), disjunctions, and =>/2 rules.
• opaque <br> Call as native Prolog goal. On success only the called Prolog goal appears in the justification.

Some example declarations:

:- prolog p/2.
:- prolog (p/2, q/1) as opaque.

If the Prolog call appears in a s(CASP) negation, the following takes place:

• If the Prolog call is ground, use Prolog \+ Goal. This is a case of non-floundering negation and thus safe.
• If the Prolog call is not ground, call findall/3 to find all solutions to the goal. If there are none, the negation is true. Otherwise, disequality constraints are created that prevent the variables to match a result. The generated pattern of partial bindings and constraints is the same as s(CASP) calling not Goal where the predicate is defined as a set of facts.

About s(CASP)

The s(CASP) system is a top-down interpreter for ASP programs with constraints.

This work was presented at ICLP'18 (Arias et al. 2018), also available here.

And extended description of the justification trees was presented at ICLP'20 (Arias et al. 2020).

Introduction

s(CASP) by Joaquin Arias, is based on s(ASP) by Kyle Marple.

s(CASP) is an implementation of the stable model semantics of constraint logic programming. Unlike similar systems, it does not employ any form of grounding. This allows s(CASP) to execute programs that are not finitely groundable, including those which make use of lists and terms.

Usage of s(CASP)

Usage:

scasp [options] InputFile(s)

• General Options:

  -h, -?, --help        Print this help message and terminate.
  --help_all            Print extended help.
  -i, --interactive     Run in interactive mode (REP loop).
  -a, --auto            Run in batch mode (no user interaction).
  -sN, -nN              Compute N answer sets, where N >= 0. N = 0 means 'all'.
  -d, --plaindual       Generate dual program with single-goal clauses
                        (for propositional programs).
  -r[=d]                Output rational numbers as real numbers.
                        [d] determines precision. Defaults to d = 5.

  --code                Print program with dual clauses and exit.
  --tree                Print justification tree for each answer (if any).

  --plain               Output code / justification tree as literals (default).
  --human               Output code / justification tree in natural language.

  --long                Output long version of justification.
  --mid                 Output mid-sized version of justification (default) .
  --short               Short version of justification.

  --pos                 Only display the selected literals in the justification.
  --neg                 Add the negated literals in the justification (default).

  --html[=name]         Generate HTML file for the justification. [name]:
                        use 'name.html'. Default: first InputFile name.

  -v, --verbose         Enable verbose progress messages.
  -f, --tracefails      Trace user-predicate failures.
  --update              Automatically update s(CASP).
  --version             Output the current version of s(CASP)

  --all_c_forall        Exhaustive evaluation of c_forall/2.
  --prev_forall         Deprecated evaluation of forall/2.

Using the principal options

Let us consider the program test.pl:

p(A) :- not q(A).
q(A) :- not p(A).
?- p(A).

• To obtain the models one by one:

$ scasp test.pl
Answer 1	(in 0.09 ms):
p(A) ,  not q(A)

 ? ;

for this example there is only one model so when we ask for more models (introducing ; after the ?) the evaluation finishes.

• To obtain all the models automatically use the option -sn with n=0:

$ scasp -s0 test.pl

• To obtain a specific number of models, e.g., 5, invoke:

$ scasp -s5 test.pl

• To use scasp with its iterative mode invoke s(CASP) with -i, and introduce the query after ?-:

$ scasp -i test.pl
?- q(A).
Answer 1	(in 0.228 ms):
q(A) ,  not p(A)
 ?

Explanation and debugging

• To print the "translation" of the code (with duals predicates and check-rules) use --code:

$ scasp --code test.pl

• To obtain the justification tree for each model use --tree.

$ scasp --tree test.pl

To generate the code/justification tree in English use --human and to control which literals should appear check the instructions in the following paper: (Arias et al. 2020).

Examples & Benchmarks & Event Calculus

Examples

There are some examples, most of them available in the distribution of s(ASP). Check them here and in your local installation (the default folder is ~/.ciao/sCASP).

Towers of Hanoi

s(CASP) vs Clingo standard vs Clingo incremental.

See more details here.

Stream data reasoning

Let us assume that we deal with series of data items, some of which may be contradictory. Moreover, different sources may give data a different degree of trustworthiness which can make some pieces of inconsistent data to be preferred. Lets us assume that p(A) and q(A) are contradictory and we receive, from source S1, p(A) and, from source S2, q(a). We may decide that: (i) p(A) is true because S1 is more realiable; (ii) or if S2 is more realiable, q(a) is true, and any value not a (i.e., X = a) p(A) is also true; (iii