prologclpconstraint-handling-rules

Representing logical disjunctions in Constraint Handling Rules


I am writing a constraint solver in Prolog that implements a simple logical formula:

"(alive(A) and animal(A)) iff (awake(A) or asleep(A))".

I found one way to implement it in Constraint Handling Rules, but it is much more verbose than the original formula:

:- use_module(library(chr)).

:- chr_constraint is_true/1.
is_true(A) \ is_true(A) <=> true.

is_true(alive(A)),is_true(animal(A)) ==> is_true(awake(A));is_true(asleep(A)).
is_true(awake(A)) ==> is_true(animal(A)),is_true(alive(A)).
is_true(asleep(A)) ==> is_true(animal(A)),is_true(alive(A)).

Would it be possible to implement this formula using a single statement instead of multiple redundant statements?


Solution

  • This is not a direct answer to your literal question. However, I would still like to point out an alternative solution altogether: At least in this concrete case, all statements are propositional statements, and so you can model the whole sentence as a Boolean constraint over the propositions.

    For example, using CLP(B):

    ?- sat((Alive_A * Animal_A) =:= (Awake_A + Asleep_A)).
    

    If you now instantiate any of the variables, the constraint solver automatically propagates everything it can. For example:

    ?- sat((Alive_A * Animal_A) =:= (Awake_A + Asleep_A)),
       Animal_A = 0.
    Animal_A = Awake_A, Awake_A = Asleep_A, Asleep_A = 0,
    sat(Alive_A=:=Alive_A).
    

    From the fact that Alive_A is still unbound, you can tell that both truth values are still admissible.