规范化布尔表达式（使用 Prolog）答案

【问题标题】：Normalizing boolean expressions (using Prolog)规范化布尔表达式（使用 Prolog）
【发布时间】：2014-12-18 18:59:49
【问题描述】：

我无法规范化一系列逻辑谓词

假设我们有两个不重叠的时间段：

......ta1_____ta2.....tb1______tb2......

为了使时间段合法、不重叠且有序 a->b，可以观察到以下事实：
ta1 待定1

ta2 ta2

但是，很容易看到一个事实就足够了：
ta2

是否有一种数学结构可以将所有已知事实归一化为单个充分事实？

最终我想在 Prolog 中编写这种推理，所以任何指向这个方向的指针都会很棒！

【问题讨论】：

是否只给出了小于（或等于）谓词？因为通常标准化程序是无法确定的......
还有更多是必要的：您还需要验证 ta1 < ta2 和 tb1 < tb2... 您只是假设这是可能的。
你是对的：ta1
没有必要：您可以将它们设置为先决条件。（额外的前提是TA1 < TB1...我回答了这种算法的大纲。这就足够了吗？
也许你可以看看约束处理规则。

标签： prolog

【解决方案1】：

为了对此进行规范化，您需要一组小于（或等于）元组以及一组您视为假设的此类约束：应该保持但不需要检查的约束。

这意味着输入应该是这样的：

normalize([TA1<TA2,TB1<TB2,TA1<TB1,TA1<TB2,TA2<=TB1,TA2<TB2],[TA1<TA2,TB1<TB2,TA1<TB1],L).

首先规范化不等式：

如果A > B 替换为B < A；和
如果A >= B 替换为B <= A。

然后你能做的就是打破假设：

如果A<B和B<C，则添加A<C；
如果A<=B和B<=C，则添加A<C；
如果A<B和B<C，则添加A<C；和
如果A<=B和B<=C，则添加A<=C。

最后，您从约束列表中删除发现的关系。因此：

如果给定A <= B，则删除A <= B；
如果给定A < B，则删除A <= B；
如果给定A < B，则删除A < B；和
如果给定了A < B，则在A=B 中替换A <= B。

最后去掉多余的约束：

A<B 和 A<B 到 A<B;
A<=B 和 A<=B 到 A<=B;
A<B 和 A<=B 到 A<B；和（@Patrick J.S.）
A<=B 和 B<=A 到 A=B。

【讨论】：

这看起来很棒！谢谢！
你能详细说明你的第三个块（删除/替换块）吗？我不确定是否有错误，或者我只是不明白。尤其是第二个和最后一个列表项对我来说似乎是矛盾的。也可能有一个额外的“替代A=B 为A<=B 和B<=A 给出。
@PatrickJ.S.：添加了你的替换，我不明白为什么？你用两个约束换一个，所以我猜没有太大的矛盾？
谢谢，现在知道了，根据您放置该子句的位置。我不确定我误解了什么。

【解决方案2】：

以下是您可以使用 SWI-Prolog 和 CHR 做什么的示例：

:- use_module(library(chr)).

:- op(700,xfx,before).

:- chr_constraint before/2, t/2, clean/0.

% X before Y means variable X is less-or-equal to variable Y
% 
transitivity @ X before Y, Y before Z ==> X \= Y, Y \= Z | X before Z.
idempotence  @ X before Y \ X before Y <=> true.

irreflexivity @ t(N,_) before t(M, _), t(M,_) before t(N, _) <=> fail.

generation @ t(N,X) before t(M, M1) ==> member(X, [1,2]),
                                  member(Y, [1,2]),
                                  X \= Y,
                                  M \= N | t(N,Y) before t(M, M1).

generation @ t(N,N1) before t(M, X) ==> member(X, [1,2]),
                                  member(Y, [1,2]),
                                  X \= Y,
                                  M \= N | t(N,N1) before t(M, Y).

% if task N is before task M keep only relevant before
clean_1 @ t(N,N1) before t(M,M1) \ t(N,N2) before t(M,M2) <=> N2 < N1, M1 =< M2 | true.
clean_1 @ t(N,N1) before t(M,M1) \ t(N,N2) before t(M,M2) <=> N2 =< N1, M1 < M2 | true.

%if task N is before task M,  suppress unnecessary t(N, _) before t(N,_)
clean_2 @ t(N, _) before t(M,_)\ t(N, _) before t(N, _) <=> N \= M | true.

% if task N is before task M suppress unnecessary t(M, _) before t(M,_)
clean_3 @ t(N, _) before t(M,_)\ t(M, _) before t(M, _) <=> N \= M  | true.

% if tasks are chained, suppress unnecessary t(First,_) before t(Last,_)
clean_4 @ t(N,_) before t(M,_), t(M,_) before t(P,_) \ t(N,_)  before t(P,_) <=> N \= M, N \= P, M \= P
                                         | true.

% when program is finished clear the set of constraints
clean @ clean \ _ before _  <=> true.
clean @ true \ clean <=> true.


go :-
        % ta1 < ta2
    t(1,1) before t(1,2),
    % tb1 < tb2
    t(2,1) before t(2,2),
    % ta1 < tb1
    t(1,1) before t(2,1),
    % ta1 < tb2
    t(1,1) before t(2,2),
    % ta2 <= tb1
    t(1,2) before t(2,1),
    % ta2 < tb2
    t(1,2) before t(2,2),
    setof(X before Y, find_chr_constraint(X before Y) , Lt),
    writeln(Lt),
    clean.

你得到：

 ?- go.
[t(1,2)before t(2,1)]
true ;
false.

【讨论】：