Представление логических дизъюнкций в правилах обработки ограничений

Я пишу решатель ограничений в Прологе, который реализует простую логическую формулу:

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

Я нашел один способ реализовать его в правилах обработки ограничений, но он гораздо более многословен, чем исходная формула:

:- 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)).

Возможно ли реализовать эту формулу, используя один оператор вместо нескольких избыточных операторов?

1 ответ

Решение

Это не прямой ответ на ваш буквальный вопрос. Однако я все же хотел бы указать на альтернативное решение в целом: по крайней мере, в этом конкретном случае все утверждения являются пропозициональными утверждениями, и поэтому вы можете смоделировать все предложение как булево ограничение над предложениями.

Например, используя CLP (B):

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

Если вы сейчас создадите экземпляр какой-либо из переменных, решатель ограничений автоматически распространит все, что может. Например:

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

Из того что Alive_A все еще не связан, вы можете сказать, что оба значения истинности все еще допустимы.

Другие вопросы по тегам