s(CASP) is related to ASP. Unlike ASP, which is traditionally solved using grounding and a SAT solver, s(CASP) is solved using top-down goal directed search without grounding. This allows s(CASP) to solve problems that cannot be grounded, while the generated proof tree is a good basis for giving a justification for the answer. s(CASP) supports both negation as failure (NAF) and classical negation. These features make s(CASP) particularly suitable for commonsense reasoning tasks that require a justification of the answer. Currently, scasp is an executable generated using Ciao. We ported s(CASP) to SWI-Prolog. The primary aim of this is to provide s(CASP) as a library that allows for embedding and managing multiple s(CASP) programs from multiple threads. Here, 'Managing' means being able to construct and modify an s(CASP) program dynamically and dynamically run queries against s(CASP) programs.
in legal or medical domains. s(CASP) is claimed to be suitable for Commonsense Reasoning.2
As the family of ASP languages is purely declarative without any side efects the solvers require some other language that prepares the ASP program, runs the solver and takes action depending on the output of the solver. Prolog is an ideal language for embedding ASP systems because manipulating clauses, handling bindings to logical variables, reasoning about the model and interpreting the justification all fit perfectly with Prolog. In our case, the s(CASP) implementation is already in Prolog and produces possible bindings, models and justifications on backtracking.
This article explains our port of s(CASP) to SWI-Prolog and discusses several alternatives to making s(CASP) accessible from Prolog. We report on unfinished work. This article is primarily input for discussion.
The GIT repository https://gitlab.software.imdea.org/ciao-lang/sCASP provides the source for s(CASP) for Ciao. The source reuses the compiler of s(ASP) by Kyle Marple [4]. Operation between variables in the s(ASP) implementation are handled ‘manually’. The s(ASP) execution maintains a mapping between variables names and their current bindings (values as well as disequality constraints). The s(CASP) execution lets Prolog take care of all operations that it can handle natively, instead of interpreting them. Therefore, a large part of the environment for the s(CASP) program is carried implicitly in the Prolog environment. Since s(CASP) and Prolog shared many characteristics (e.g., the behavior of variables), this results in flexibility of implementation and gives a large performance improvement. [3]
We ported s(CASP) to SWI-Prolog. The aim of this project is twofold: (
We realised two changes in the design of s(CASP) to better facilitate embedding in Prolog. First of all, we replaced the DCG (Prolog grammar rules) based parser by the Prolog parser. This is possible by defining an adequate set of Prolog operators. 3 The terms read are validated to satisfy the restrictions imposed by s(CASP) and converted into the same format that was emitted by the original parser. Second, where the original implementation generated the justification directly from the resulting s(CASP) solver’s stack, the current implementation creates a Prolog representation from the stack that naturally represents the justification while hiding the internals of the solver.
2See https://personal.utdallas.edu/~gupta/csg/ 3s(ASP) allows for predicate names that start with an underscore, as in _p(X). This can be handled in SWIProlog, but not in standard ISO Prolog. ?- p(X). sCASP model: [p(X),not q(X)], sCASP justification query p(X) not q(X)
chs(p(X)) ∧
o_nmr_check ;
X = 1,
sCASP model: [p(
Currently, s(CASP) programs can be embedded into Prolog using two directives that create a block. The opening directive changes the Prolog operator tables and activates rules for term_expansion/2 that validate the s(CASP) terms and does some simple transformations that avoid conflicts with Prolog. The closing directive reverts the changes to the operator table, compiles the loaded terms into the internal s(CASP) representation and creates wrappers that make the exported s(CASP) predicates accessible as normal Prolog predicates from the enclosing Prolog module. :- begin_scasp(Unit, Exports). <sCASP program> :- end_scasp.
We give a minimal example below.
:- use_module(library(scasp/embed)).
:- begin_scasp(qp, [p/1]).
p(X) :- not q(X).
p(
After loading this Prolog program, p/1 is made available as a normal Prolog predicate as shown in figure 1. Calling this predicate makes the bindings available as normal Prolog bindings while alternative solutions are made available through Prolog backtracking. The model and justification are stored in backtrackable global variables as provided by b_setval/2 in SWIProlog. By using backtrackable global variables we can provide access to these extensions to the normal Prolog answer (only the bindings) while full sharing of variables and constraints are retained.
The model is represented as a list of Prolog terms, where each term may be nested as not(Term) (not provable), -(Term) (false) or not(-(Term)) (not provable that Term is false). The justification is a tree represented as a term -(Term, ListOfChildren). Here ListOfChildren is the empty list for facts and a list of -/2 terms otherwise. In addition to the negation symbols, terms may be nested in one of the terms below.
• proved(Term) Term was already proved. • chs(Term) Term is assumed because it appears in a loop with an even number of negations • assume(Term) Marks the loop detected by chs(Term)
The model is made available by scasp_model/1 and the justification tree using scasp_justification/2 , where the second argument is an option list that may be used to adjust the level of detail in the tree.
The SWI-Prolog toplevel displays answers to a query as a valid Prolog body term. For traditional Prolog this is a conjunction of unification (=/2) calls that establish the binding or true if no variables are bound. If some of the variables are subject to constraints the constraints are reified using copy_term/3 and added as goals to the answer, for example, using clp(fd) we may get: ?- A #> 2, A #< 5.
A in 3..4.
To accommodate CHR, which has a notion of a global constraint store, SWI-Prolog provides a hook that can be used to add additional goals to the answer. This hook is used to make the model and justification visible in the toplevel. This is not entirely satisfactory because the printed output is no longer valid Prolog input that has the same efect as the original query.
The current codebase is SWI-Prolog specific. While many Prolog implementations have some way to embed code by temporarily changing the operator table and doing macro expansion, there is no standard. The same applies for integrating the model and justification into the Prolog REPL loop.
Ideally the data representations such as the program representation going into the s(CASP) compilation phase, the s(CASP) intermediate program representation, the model and justification are synchronised between (Prolog) s(CASP) implementations. That allows for sharing the program transformation and solver code as well as code using the output of the embedded s(CASP) system.
When porting s(CASP) to SWI-Prolog we set ourselves the following goals: (
The current implementation has no interface for composing s(CASP) programs dynamically. This is a vital feature for Inductive Logic Programming (ILP) as well as for assembling a suitable program based on currently known case data.
Another approach to execute a goal using s(CASP) semantics would be to automatically re-interpret a Prolog program under s(CASP) semantics. One way to do that would be to declare predicates as s(CASP) predicates using e.g., :- scasp p/1, q/2.. Alternatively we could define a predicate scasp(Goal). Both approaches would need to establish the reachable program, verify it satisfies the limitations imposed by s(CASP), compile the program to the s(CASP) intermediate representation and run the s(CASP) solver. This approach provides a trivial API for manipulating the s(CASP) program using assert/1 and retract/1. It is not clear how s(CASP) global constraints fit into this picture.
We also plan to support embedding s(CASP) into SWISH, providing an online environment for teaching and exchanging ideas.