Представление логических дизъюнкций в правилах обработки ограничений
Я пишу решатель ограничений в Прологе, который реализует простую логическую формулу:
"(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
все еще не связан, вы можете сказать, что оба значения истинности все еще допустимы.