This paper presents a short tutorial on s(CASP), highlighting some of the novel aspects and the reasons for its design. The most important aspect of s(CASP) is its goal-directed top-down execution model that implements Constraints Answer Set Programming. The execution strategy of s(CAPS) avoids the grounding phase, present in most ASP systems, and can constraint variables that, as in CLP, are kept during the execution and in the answer sets. Additionally, s(CASP) generates a human-understandable justifications (in natural language) of the resulting answer sets. s(CASP) is implemented in Prolog (currently available for Ciao and SWI Prolog) and has been used in several applications, including medical advisors, avionic, legal reasoner, XAI, and natural language processing.
1. Introduction
• An automated reasoner that uses Event Calculus (EC) [
In addition, in January 2021, during the HackReason3 at UT Dallas, 17 teams developed applications that rely on simulating human-style commonsense reasoning using s(CASP).
This tutoral provides a brief description of s(CASP). Section 2 describes the installation process. Section 3 presents the language supported by s(CASP). Section 4 provides some ticks to tune the size, and/or the number of resulting answer sets and to adjust the constraint’s accuracy. Section 5 gives a brief description of the available flags to generate justifications and/or encoding (in natural language) with diferent levels of detail. In Section 6 we present the Dynamic Consistency Check (DCC), still a work in progress, and how can be activated for testing. Finally, in Section 7 we propose some ideas for improving s(CASP). 2. s(CASP) Installation on Ciao or SWI-Prolog As we mentioned before, s(CASP) is currently available to be executed under Ciao http:// ciao-lang.org/, or SWI-Prolog https://www.swi-prolog.org/. The s(CASP) source code for Ciao is available at https://gitlab.software.imdea.org/ciao-lang/sCASP and for SWI-Prolog, thanks to Jan Wielemaker, at https://github.com/JanWielemaker/sCASP.
1https://cs.utdallas.edu/computer-scientists-enhance-alexas-small-talk-skills/ 2https://github.com/smucclaw/r34_sCASP 3https://hackreason.aisutd.org/ Installation on Ciao Ciao is a programming language that is builds from a logic-based simple kernel and is designed to be extensible and modular. The system implements some advanced features such as separate and incremental compilation, global program analysis and static debugging and optimization (via source to source program transformation, CiaoPP preprocessor), a build automation system, documentation generator, debugger, and (Emacsbased) development environment.
The installation of Ciao can be done using an interactive assistant from the command line in three steps: first, we run the interactive assistant 4, then, we activate the added Ciao path, and ifnally, we install s(CASP) as a bundle: curl https://ciao-lang.org/boot -sSfL | sh source ~/.washrag ciao get gitlab.software.imdea.org/ciao-lang/sCASP
When the installation succeeds, a folder with the source code and s(CASP) examples is created in the ciao workspace (the default path is ~/.ciao/sCASP/). The --help_all flag generates the list of all available flags 5 to consult and/or adapt s(CASP) behavior.
Installation on SWI-Prolog SWI-Prolog ofers a comprehensive free Prolog environment. Since its start in 1987, SWI-Prolog development has been driven by the needs of real-world applications. SWI-Prolog is widely used in research and education as well as commercial applications. Additionally, it ofers SWISH (https://swish.swi-prolog.org/), an online environment for teaching and exchanging ideas. Therefore, thanks to Jan Wielemaker, we can not only generate a standalone file, but also we have the opportunity to use s(CASP) directly in SWISH.
To generate the standalone file we have to use the latest development release version of SWIProlog available at https://www.swi-prolog.org/download/devel – there are already compiled SWI-Prolog binaries for Linux, Windows, and MacOS. Then, to generate the executable file of s(CASP), we just need to run the make file available in the corresponding s(CASP) repository for SWI-Prolog (https://github.com/JanWielemaker/sCASP). 3. Getting started s(CASP) extends the expressiveness of Answer Set Programming systems by featuring predicates, constraints among non-ground variables, uninterpreted functions, and, most importantly, a top-down, query-driven execution strategy. These features make it possible to return answers with non-ground variables (possibly including constraints among them) and to compute partial models by returning only the fragment of a stable model that is necessary to support the answer to a given query.
In s(CASP), and unlike Prolog’s negation as failure and ASP default negation, not p(X) can return bindings for X on success, i.e., bindings for which the call p(X) would have failed. 4For Linux and MacOS use the sh-terminal, for Windows the “Windows Subsystem for Linux” is required. 5For the reader’s convenience the help_all output is available in Appendix A.
Example 1. Considering the program p.pl6 1 p(a). let’s run s(CASP) in the iterative mode by invoking scasp -i p.pl.
Then, we introduce the query ?- not p(X). and s(CASP) would return the binding X \= a, where \= is a disequality constraint meaning ̸= , and the model {not p(X |{X \= a})} that represents the set of ( ) can be proven only when ̸= .7
Thanks to the interface of s(CASP) with constraint solvers, sound non-monotonic reasoning with constraints is possible.
1 p(X):- X > 0. which for the same query as above, returns the model {not p(X | {X ≤ 0})}.
As we mentioned before, s(CASP) supports uninterpreted functions (with the same conventions as Prolog), e.g., [f(a)|Rest] denotes a list with head f(a) and tail Rest. While in conventional ASP implementations this could give rise to an infinite grounded program, the s(CASP) execution model can deal with them similarly to Prolog, with the added power of the using constructive negation in the execution and returned models.
Example 3. For the program member.pl
1 member(X, [X|Xs]).
2 member(X, [_|Xs]):- member(X, Xs).
3
4 list([
Since we include the query as part of the program, invoking s(CASP) in automatic mode8 it
returns the following model and binding:
{ list([
7Uniqueness of names is assumed for constants and function names: any two constants or functions with diferent names represent diferent objects.
8The automatic mode is selected by default so the flag -a or --auto can be omitted, i.e., scasp member.pl.
A = [
models that on Saturday, Bob either goes to the opera or stays home and on Sunday he has dinner. The top-down evaluation of the non-stratified negation in lines 1-2 makes a loop with an even number of intervening negations (even loop). When the s(CASP) metainterpreter detects an even loop, the truth/falsehood of the atoms involved is assumed to generate diferent models, the consistency of which is subsequently checked. In this example, there are two possible models, and given a query s(CASP) returns (if exists) the relevant partial model for the query: ?- opera(saturday) ?- home(saturday) ?- dinner(sunday) ?- opera(saturday),home(saturday) returns {opera(saturday),not home(saturday)}. returns {home(saturday),not opera(saturday)}.
returns {dinner(sunday)}.
returns no models.
In addition to default negation, s(CASP) supports classical negation (using the prefix ’ -’) to capture the explicit evidence that a literal is false, e.g. not opera(saturday) means that we have no evidence that Bob goes to the opera (we can not prove it), and -opera(saturday) means that we have explicit evidence that Bob does not go to the opera (there is a proof for it). 4. Tuning of the Partial Answer Sets Output In this section, we describe directives and flags that can be used to tune the output of s(CASP) to select the atoms that appear in the partial model, avoid consistency checks, generate a specific number of answers, and/or determine the accuracy of the real numbers.
Select the atoms that appear in the partial model: The directive #show can be used to select which atoms should appear in the partial models.
to the program in Example 4. Now, in the partial models returned by s(CASP) only positive atoms appear, so for the query ?- opera(saturday) it returns {opera(saturday}.
Negated atoms can also be selected, e.g., #show not home/1,-opera/1 is also valid. 1 opera(D) :- not home(D). 2 home(D) :- not opera(D). 3 home(monday). 4 5 :- baby(D), opera(D). 6 7 baby(tuesday). 8 9 ?- opera(D). Denials: In ASP, denials are constructions of the form :- p, q, i.e., rules without head, and are used to express that the conjunction of atoms p ∧ q cannot be true: either p, q, or both, have to be false in any stable model. Additionally, the s(CASP) compiler also detects statically rules of the form r:- q,not r., called olon rules, and introduces denials to ensure that models satisfy ¬ ∨ even if the atoms r or q are not needed to solve the query. Let us look at two examples.
1 p :- not q.
2 q :- not p.
3 r :- not r. the compiler introduces the denial :- not r which is checked for consistency after any given query. Therefore, s(CASP) returns no models, regardless of the initial query.
simultaneously true for any value of D. Thus for the query in line 9 the resulting partial model is: { opera(D | {D \= monday,D \= tuesday}), not home(D | {D \= monday,D \= tuesday}), not baby(Var1 | {Var1 \= tuesday}), baby(tuesday), not opera(tuesday), home(tuesday) } where the atom opera({D |{D \= monday,D \= tuesday}) means that Bob can go to the opera any day except on Monday or Tuesday.
For debugging purposes, s(CASP) provides flags to disable consistency checks: (i) --no_olon disables the consistency check of denials introduced by the compiler due to olon rules but checks the user-defined denials; (ii) --no_nmr disables consistency check of all non-monotonic rules. In Example 6, runing s(CASP) by invoking scasp --no_nmr -i olon.pl, for the query ?- p returns the model {p,not q} which may be useful for debugging.
Since consistency checks are evaluated when a tentative partial model is encountered, they
introduce a run-time penalty. To reduce this overhead we propose a Dynamic Consistency
Check (DCC) [
The -sN or -nN flag can be used to specify the number N of answer sets that s(CASP) should return in automated mode, and by adding the -s0 or -n0 flag s(CASP) would return all the possible answers sets.
Constraint precision: The s(CASP) system has a generic interface to enable plugging in
constraint solvers. s(CASP) currently includes the CLP(Q) linear constraints solver [
1 s(X,Y) :- X #= Y * 7/53.
the query ?- s(X,4.35) returns the binding X=609/1060, invoking s(CASP) without flags, and
returns the binding X=0.574 invoking scasp -r=3 rationals.pl.
5. Justification and encoding (in natural language)
In the context of the European Union approved the General Data Protection Regulation
(GDPR) [
Justifications: s(CASP) uses top-down evaluation trees to generate minimal justifications in which it is possible to control which literals should appear.
JUSTIFICATION_TREE: we assume that Bob goes to the opera on a day D not equal monday, nor tuesday, because
Bob does not stay at home on D not equal monday, nor tuesday.
The global constraints hold, because the global constraint number 1 holds, because there is no evidence that 'baby' holds (for Var1), with Var1 not equal tuesday, and 'baby' holds (for tuesday), and we assume that there is no evidence that Bob goes to the opera on the day tuesday, because 'home' holds (for tuesday).
D \= tuesday}) is assumed to holds, and this assumption is consistent with the denial. To check the denial, i.e., that the conjunction of atoms baby(D) ∧
opera(D) is not simultaneously true for any value of D, s(CASP) checks that ∀ D ( not baby(D) ∨ (baby(D) ∧ not opera(D)) ).
appear in the justification are: (i) mid, used by default, which only displays the user-defined predicates; (ii) long that displays all predicates, including auxiliary predicates such as the forall/2 used to check this denial; and (iii) short which only displays the annotated literals. Additionally, the flag neg, used by default, includes the default-negated version of the annotated/selected predicates, whereas the flag pos does not.
The s(CASP) justification framework provides a mechanism for presenting natural language justifications using a generic translation and the possibility of customize it with directives that provide translation patterns. Both plain text and expandable, user-friendly HTML files can be generated.
When executed s(CASP) by invoking scasp --tree --human opera.pl opera.pred, the natural language justification is obtained (Figure 3). Note that lines 1, 2, and 7 follow the translation patterns defined in opera.pred.
Additionally, adding the --html=bob flag, s(CASP) generates the HTML file bob.html, which includes the query, the bindings and an expandable justification tree that can be expanded and/or collapsed to facilitate its analysis.
Compiled code: Given an ASP program, a dual program compiled by s(CASP) will include
the rules that express the constructive negation of the predicates in the original ASP program [
During the generation of the duals, for each clause, the compiler generates independent clauses with the “negated” literals in its body, and to avoid redundant answers, every ℎ clause for a negated literal includes calls to any ℎ literal with < .
Example 12. For the clause h(X,Y):- r(X),not s(X,Y),q(Y), its dual is: 1 not h(X,Y) :- not r(X). 2 not h(X,Y) :- r(X), s(X,Y). 3 not h(X,Y) :- r(X), not s(X,Y), not q(Y).
When we want to modify the dual program, we can use the --code9 flag to output the dual program, and then load an updated version with the -c or --compiled flag.
Additionally, translation patterns can be used to display the compiled program in natural language, thereby making it easier for experts without a programming background to understand both the program and the results of its execution.
6. Dynamic Consistency Check (Work in Progress) As we mentioned before, the denials are evaluated after the query, ensuring that the tentative partial model is consistent with them. In cases where this evaluation fails the execution backtracks to check other alternatives. The goal of the Dynamic Consistency Check (DCC) is to check the denials as soon as atoms involved are added to the tentative partial model.
Our proposal is based on the constraint propagation algorithm, which, when the domain of a decision variable is modified, examines the constraints containing that variable to determine whether any values in the domains of other decision variables are now inconsistent. During ASP program evaluation, when an atom is added to the tentative partial model, the denials containing that atom are examined to determine if the presence of other atoms makes the tentative partial model inconsistent. In this case, the evaluation fails and is immediately backtracked to avoid computational waste. We believe that the benefits of the denial propagation in detecting 9By adding the --raw flag, the system prints the clauses in the same order as the compiler does. 1 % Graph 2 vertex(a). 3 vertex(b). 4 vertex(c). 5 vertex(d). inconsistencies as early as possible outweigh the overhead introduced (i) during compilation to generate the DCC rules used to trigger denials involving specific atoms, and (ii) due to the extra work done to check denials when there are no inconsistencies.
Example 14. Consider the standard ASP code for the Hamiltonian problem, in hamiltonian.pl 1 #show chosen/2. 2 reachable(V) :- chosen(V, a). 3 reachable(V) :- chosen(V,U), reachable(U). 4 % Choose or not an edge of the graph. 5 chosen(U,V) :- edge(U,V), not other(U,V). 6 other(U,V) :- edge(U,V), not chosen(U,V). 7 % Every vertex must be reachable. 8 :- vertex(U), not reachable(U). 9 % Do not choose edges to/from the same vertex 10 :- chosen(U,W), U \= V, chosen(V,W). 11 :- chosen(W,U), U \= V, chosen(W,V). 12 ?- reachable(a). where the denials in lines 10-11 are used to discard those tentative models that have chosen edges violating the properties of the Hamiltonian cycle. For the query in line 12, using the graph in Fig. 4 there are three stable models, one for each Hamiltonian cycle: 1 { chosen(a,c), chosen(c,d), chosen(d,b), chosen(b,a),. . . } 2 { chosen(a,b), chosen(b,c), chosen(c,d), chosen(d,a),. . . } 3 { chosen(a,d), chosen(d,b), chosen(b,c), chosen(c,a),. . . }
Evaluation: We compared the performance of s(CASP) with and without DCC using a MacOS
11.5.2 Intel Core i7 at 2.6GHz. We observe that using DCC, for the evaluation of the Hamiltonian
problem (Example 14) with the graph in Figure 4, we obtain a speedup of 6.8:
• Without DCC: invoking scasp --prev_forall -n0 hamiltonian.pl
graph.pl.10 the evaluation of the three models takes 8.266s.
• With DCC: invoking scasp --prev_forall -n0 --dcc hamiltonian.pl
graph.pl hamiltonian_dcc.pl,11 the evaluation, using this preliminary DCC
implementation, takes only 1.215s.
10Note that we are using a specific forall/2 implementation to run this example (more details in Section 7).
11Note that the DCC implementation is unfinished and the DCC rules for the denials in lines 10-11 are included
manually in hamiltonian_dcc.pl. In the future, they will be compiled automatically.
7. Future Work
As already mentioned, the implementation has been improved in several aspect but can still be
substantially improved, and in particular we are planning to:
• Finish the DCC implementation and work on using analysis to optimize the compilation
of the DCC rules, being able to interleave their execution with the top-down strategy to
discard models as soon as they are shown to be inconsistent.
• Use dependency analysis to improve the generation of the dual programs.
• Apply partial evaluation and better compilation techniques to remove (part of) the
overhead brought about by the interpreting approach.
• Optimize the implementation of the c-forall algorithm using tabling [
Print this help message and terminate.
Print extended help.
Run in interactive mode (REP loop).
Run in batch mode (no user interaction).
Compute N answer sets, where N >= 0. N = 0 means ’all’.
Load compiled files (e.g. extracted using --code).
Generate dual program with single-goal clauses (for propositional programs).
Output rational numbers as real numbers. [d] determines precision. Defaults to d = 5.
Print program with dual clauses and exit.
Print justification tree for each answer (if any).
Output code / justification tree as literals (default).
Output code / justification tree in natural language.
Output long version of justification.
Output mid-sized version of justification (default) .
Short version of justification.
Only display the selected literals in the justification.
Add the negated literals in the justification (default).
Generate HTML file for the justification. [name]: use ’name.html’. Default: first InputFile name.
Trace user-predicate calls.
Trace user-predicate calls (show tree).
Trace user-predicate failures.
Trace user-predicate failures (show tree).
Automatically update s(CASP).
Output the current version of s(CASP) Activate the Dynamic Consistency Check.
Exhaustive evaluation of c_forall/2.
Deprecated evaluation of forall/2.
Deprecated evaluation of forall/2.
Do not compile olon rules (for debugging purposes).
Do not compile NMR checks (for debugging purposes).
Enable warning messages (failures in variant loops / disequality).
Do not fail in the presence of variant loops.
Collect only the minimal models (TABLING required).
Sort the clauses as s(ASP) does (use with --code).