Using inequality over logical terms

The abductive system allows inequality over logical terms to be used in the abductive theory, and has a built-in inequality solver to handling the reasoning. An inequality over two terms is written as T1 =/= T2, where T1 and T2 are Prolog terms. The semantics of =/= can be described as follows:

• Let $a$ and $b$ be constants, $a$=/=$b$ holds if and only if $a$ and $b$ are not equal;
• Let $f^{a}(T^{a}_{1},\ldots,T^{a}_{n})$ and $f^{b}(T^{b}_{1},\ldots, T^{b}_{m})$ be two terms, $f^{a}(T^{a}_{1},\ldots,T^{a}_{n})$=/= $f^{b}(T^{b}_{1},\ldots, T^{b}_{m})$ holds if and only if one of the following holds:
  • $f^{a}$=/=$f^{b}$;
  • $n \neq m$;
  • $n = m \wedge \exists i . 0 \leq i \leq n \wedge T^{a}_{i}$=/=$T^{b}_{i}$

For example, an action effect condition of goto and the integrity constraint of ``no two action can be performed as the same time'' can be encoded as a rule using inequality:

terminates(goto(X), at(Y), T) :- X =/= Y.

ic :- happens(E1, T), happens(E2, T), E1 =/= E2.