在运行时定义CHR约束

Question

我正在尝试编写一个在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约束的方法吗？

Answer 1

可以通过定义is_true/2谓词来解决此问题。该谓词可以在运行时使用谓词进行更改assertz/1。这不是一个理想的解决方案，但它在这种特殊情况下有效。

\n\n

现在我可以这样编写程序：

\n\n

:- use_module(library(chr)).\n:- chr_constraint is_true/1.\n\nis_true(A) ==> is_true(A,B) | is_true(B).\nis_true([A,means,B]) ==> assertz(is_true(A,B)).\nis_true([],[]).\n

\n\n

并以这种方式在运行时添加新约束：

\n\n

\xcc\x80?- is_true([[A,implies,B],means,[A,means,B]]).\nis_true([[A, implies, B], means, [A, means, B]]).\n\n?- is_true([A>B,implies,B<A]).\nis_true([A>B, means, B<A]),\nis_true([A>B, implies, B<A]).\n\n?- is_true(A>B).\nis_true(B<A),\nis_true(A>B).\n

\n\n

相反，为 CHR 编写一个“元解释器”可能更有用：

\n\n

:- initialization(main).\n:- set_prolog_flag(\'double_quotes\',\'chars\').\n:- use_module(library(chr)).\n:- chr_constraint is_true/1.\n\nis_true(X) \\ is_true(X) <=> true.\nis_true(X ==> Y),is_true(X1) ==> copy_term((X -> Y),(X2 -> Y1)),(X2=X1,(is_true(X1)->is_true(Y1));X2\\=X1),writeln(Y).\nis_true((X;Y)) ==> is_true(X);is_true(Y).\nis_true((X,Y)) ==> is_true(X),is_true(Y).\nis_true(is_true(X)) ==> is_true(X).\nis_true(X),is_true(\\+X) ==> false.\n\n\nmain :-\n    is_true(is_person(A)==>is_mammal(A)),\n    is_true(is_mammal(A)==>is_animal(A)),\n    is_true(is_person(sue)),is_true(is_person(bob)).\n

\n