标签: constraint-handling-rules

我正在尝试编写一个在SWI-Prolog中在运行时生成新约束的程序.is_true([A,means,B])旨在在运行时生成另一个约束:

:- use_module(library(chr)).
:- chr_constraint is_true/1.

is_true([A,means,B]) ==> (is_true(A) ==> is_true(B),writeln('asserted')).
is_true([[A,is,true],means,[A,is,not,false]]).
is_true([something,is,true]).

但是当我输入这些查询时,is_true约束似乎没有效果.is_true([something, is, not, false])不归还true:

?- is_true([something,is,true]).
true .

?- is_true([something,is,not,false]).
is_true([something, is, not, false]).

在控制台中断言约束似乎没有任何影响:

?- asserta(is_true(A>B)==>(is_true(B<A),writeln("asserted"))).
true.

?- is_true(4>3).
is_true(4>3).

还有另一种在运行时定义新CHR约束的方法吗？

我正在仔细研究约束处理规则(CHR)，看看我是否能理解它们（从某种意义上说，这里计算的是什么以及经典逻辑甚至线性逻辑如何适合于此）并可能应用它们。

Thom Frühwirth 2009 年的书讨论了 CHR 的原则，但实施当然可能有所不同。

在这种情况下，我使用CHR的SWI Prolog 实现。

如果我理解得很好：

1. CHR 的实现将提供至少一个“约束存储”来表达“计算状态”。约束存储仅包含基础原子（即正文字）。
2. 在典型的 CHR 会话中，首先使用初始状态设置约束存储。一种编写包含 CHR 规则的 CHR 程序。然后以约束存储作为参数运行 CHR 程序。重复应用前向链 CHR 规则直到不再适用任何规则，这将迭代地（并且破坏性地）将约束存储从其初始状态转换为某个最终状态。然后可以检查约束存储以找到所需的答案。
3. 在这种情况下，只考虑不关心非确定性（“承诺选择非确定性”）：当多个规则适用于任何中间状态时，采用任何规则。
4. “不知道”不确定性与回溯到后来失败的情况下，选择点是不考虑-这是留给实施，以一种方式或其他提供这一点，如果需要的话。

作为练习，使用欧几里德算法计算 GCD 并保留操作日志的最简单程序：

% Constraint `logg(Ti,Msg)` retains the log message `Msg` at step `Ti`
% (which increases monotonically)
% Constraint `gcdpool(X)` denotes a "GCD pool member". At each step, we want
% to compute the GCD of all the X for which …