Using constraints over finite domain

The abductive system allows finite domain constraints to be used in the abductive theory, and uses the library(clpfd) module of SICStus for solving the constraints during abductive inference. The syntax of finite domain arithmetic expressions can be found from the SICStus documentation ¹. We include it here for your reference:

$$\small \begin{array}{ll} N & ::= integer \\ \\ LinExpr & ::... ... {=}{<}}\mid{\tt\char93 {>}{=}}\mid{\tt\char93 {>}} \end{array}$$

In addition, the finite domain membership constraint X in Min..Max can also be used. For example, the SEC axioms can be encoded using finite domain constraints as:

 
time(T) :- T in 0..8.          % specifying the range of time

holds(F, T) :-
  time(T1), time(T), 0 #< T1, T1 #< T,
  happens(A, T1), initiates(A, F, T1), \+ clipped(T1, F, T). 

clipped(T1, F, T) :-
  time(T1), time(T), time(T2), T1 #< T2, T2 #< T,
  happens(A, T2), terminates(A, F, T2).