在约束处理规则中表示逻辑分离 [英] Representing logical disjunctions in Constraint Handling Rules

问题描述

我正在 Prolog 中编写一个约束求解器，它实现了一个简单的逻辑公式:

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

我在约束处理规则中找到了一种实现它的方法，但它比原始公式要冗长得多:

:- use_module(library(chr)).:- chr_constraint is_true/1.is_true(A) \ is_true(A) <=>真的.is_true(alive(A)),is_true(animal(A)) ==>is_true(清醒(A));is_true(睡着(A)).is_true(清醒(A)) ==>is_true(动物(A)),is_true(活着的(A)).is_true(睡着(A)) ==>is_true(动物(A)),is_true(活着的(A)).

是否可以使用单个语句而不是多个冗余语句来实现此公式?

解决方案

这不是对您的字面问题的直接回答.但是，我仍然想指出一个替代解决方案:至少在这个具体案例中，所有陈述都是命题陈述，因此您可以将整个句子建模为布尔约束超过命题.

例如，使用 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，sat(Alive_A=:=Alive_A).

从 Alive_A 仍未绑定的事实来看，您可以看出这两个真值仍然可以接受.

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?

解决方案

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.

这篇关于在约束处理规则中表示逻辑分离的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！