Explainable AI and Computational Law with s(CASP)

As artificial intelligence systems are increasingly deployed to automate administrative and legal decisions, the field of Computational Law (often called “Rules as Code”) has gained significant traction. This field aims to draft legislation, tax codes, corporate policies, and safety standards directly as computer-executable logic.

However, executing rules is only half the battle. In regulated domains, we cannot rely on black-box predictions. If an AI system denies a citizen a government benefit, rejects a travel expense reimbursement, or flags a financial transaction for compliance auditing, the system must be able to explain why it made that decision.

Traditional machine learning algorithms cannot provide these explanations. Standard Prolog engines can produce proof trees, but they struggle with negation-as-failure under complex constraints.

s(CASP) (Goal-Directed Answer Set Programming) solves this. It compiles logic rules and evaluates queries by generating a mathematical justification tree. Instead of returning a simple true or false, s(CASP) explains the exact chain of rules, facts, and lack of contradictory evidence that led to its conclusion.

Architecture diagram for the s(CASP) Compliance example
Figure 12. Architecture diagram for the s(CASP) Compliance example

What is s(CASP)?

s(CASP) is a first-order logic programming system that combines features of constraint logic programming and Answer Set Programming:

  • Goal-Directed: Unlike traditional ASP solvers that must compute all possible stable models (which is computationally expensive for large systems), s(CASP) evaluates specific queries on demand, similar to standard Prolog.
  • Justification Trees: It constructs a step-by-step trace of which rules were satisfied and which negative constraints were successfully avoided.
  • Predicates for Natural Language: It allows developers to define #pred templates that translate raw logic terms into human-readable sentences, generating explanations directly from the justification tree.
* * *

Implementing Compliance Rules

We will model a corporate travel expense reimbursement policy. Under this policy, a person is eligible for reimbursement if:

  1. They are an employee.
  2. The travel was for business purposes.
  3. The travel was not for personal reasons.
  4. They did not exceed their expense limit of $500.

Here is the implementation in source-code/scasp_compliance/compliance_check.pl:

 1 :- module(compliance_check, [
 2     eligible_for_reimbursement/1,
 3     run_compliance_check/1
 4 ]).
 5 
 6 :- use_module(library(scasp)).
 7 :- use_module(library(scasp/human)).
 8 
 9 :- discontiguous employee/1.
10 :- discontiguous business_travel/1.
11 :- discontiguous expense_amount/2.
12 
13 %% Policy Rules
14 eligible_for_reimbursement(Person) :-
15     employee(Person),
16     business_travel(Person),
17     not personal_travel(Person),
18     not travel_limit_exceeded(Person).
19 
20 travel_limit_exceeded(Person) :-
21     expense_amount(Person, Amount),
22     Amount > 500.
23 
24 %% Facts
25 employee(alice).
26 business_travel(alice).
27 expense_amount(alice, 350).
28 
29 employee(bob).
30 business_travel(bob).
31 expense_amount(bob, 650).
32 
33 employee(charlie).
34 business_travel(charlie).
35 personal_travel(charlie).
36 expense_amount(charlie, 150).
37 
38 %% s(CASP) Explanations/Translations
39 #pred eligible_for_reimbursement(Person) ::
40     '@(Person) is eligible for travel reimbursement'.
41 #pred employee(Person) :: '@(Person) is a registered employee'.
42 #pred business_travel(Person) :: '@(Person)\'s trip was for business
43     purposes'.
44 #pred personal_travel(Person) :: '@(Person)\'s trip was for personal
45     reasons'.
46 #pred travel_limit_exceeded(Person) ::
47     '@(Person) has exceeded the travel expense limit of $500'.
48 #pred expense_amount(Person, Amount) :: '@(Person)\'s travel expense
49     amount is $ @(Amount)'.
50 
51 %% Helper to run and output the explanation
52 run_compliance_check(Person) :-
53     (   scasp(eligible_for_reimbursement(Person), [tree(Tree)])
54     ->  format('~w is eligible.~n~n', [Person]),
55         writeln('Justification Tree:'),
56         human_justification_tree(Tree, [])
57     ;   format('~w is NOT eligible or compliance check failed.~n',
58         [Person])
59     ).

Note how the #pred declarations use the @(Variable) syntax to map variables to their text representations. The not prefix represents default negation, meaning the rule succeeds if no evidence exists to prove the negative case.

* * *

Running the Compliance Check

To evaluate travel eligibility and generate explanations, load the file into SWI-Prolog:

1 $ swipl compliance_check.pl

Query the compliance checker for alice:

1 ?- run_compliance_check(alice).

s(CASP) evaluates the logic, confirms alice is eligible, and outputs a natural language justification tree explaining its reasoning:

 1 alice is eligible.
 2 
 3 Justification Tree:
 4    alice is eligible for travel reimbursement, because
 5       alice is a registered employee, and
 6       alice's trip was for business purposes, and
 7       there is no evidence that alice's trip was for personal reasons, and
 8       there is no evidence that alice has exceeded the travel expense limit of $500, because
 9          there is no evidence that alice's travel expense amount is $ any number not [350], and
10          alice's travel expense amount is $ 350, and
11          350 is less than or equal to 500

If you run the query for bob or charlie, the check fails and outputs that they are not eligible. Bob’s expense ($650) exceeds the $500 travel limit, while Charlie’s trip was for personal travel, violating the compliance constraints.

* * *

Key Design Decisions

Why s(CASP) over regular Prolog? Traditional Prolog handles negation using negation-as-failure (\+). However, regular Prolog cannot easily reason about negative constraints or construct explicit justification trees for negative constraints (e.g. proving that “there is no evidence that Alice’s trip was for personal reasons”). s(CASP) handles stable model semantics and goal-directed Answer Set Programming, allowing it to mathematically prove that a negative condition is not met and represent that proof step in the justification output.

Rules as Code movement. Writing policies directly in executable code eliminates the translation gap between the legal draft of a policy and the software implementation. Government bodies and large enterprises are adopting this approach to ensure that business logic is auditable, self-documenting, and provably compliant.

Up next

Constraint Logic Programming