如何使用if_/3消除三值逻辑or/3谓词的选择点？

我需要实现一个三值逻辑的or/3谓词，规则是：

• 前两个参数是逻辑变量，第三个参数只能取true或u（未知）
• 当第三个参数为false时，谓词直接失败
• 现有实现能正常运行，但会产生多余选择点，比如查询or(A,false,C)返回两个结果后会出现false
• 尝试用if_/3和reif包实现or3/3，也试过直接用=/3和;/3，但都还有无用选择点，请问问题出在哪？

原简单实现代码 #

or(A,B,true) :-
    A = true, B = true ; A = true, B = false ; A = false, B = true.
or(A,B,u) :-
    A = u, B = u; A = u, B = false ; A = false, B = u.

查询结果 #

?- or(A,false,C).      
A = C, C = true ;
A = C, C = u ;
false.

尝试的if_/3实现代码 #

or3(A, B, C) :-
    if_( C = u
       , if_( A = u
            , ( B = u ; B = false)
            , ( A = false, B = u )
            ),
    if_( C = true
       , if_( A = true
            , ( B = true ; B = false)
            , ( A = false, B = true )
            )
       , false
       )
    ).

查询结果 #

?- or3(A,false,C). 
Correct to: "tri_logic:or3(A,false,C)"? yes
A = C, C = u ;
A = C, C = true ;
false.

另一种实现代码 #

or3(A,B,C) :-
    =( C, true, T),
    ;( ( A = true, B = true ), ( A = true, B = false ), T1 ),
    ;( T1=true, ( A = false, B = true), T).

查询结果 #

?- or3(A,false,C). 
Correct to: "tri_logic:or3(A,false,C)"? yes
A = C, C = u ;
A = C, C = true ;
false.

问题原因与解决方案 #

为什么会有多余选择点？ #

当前实现存在非确定性分支，比如在if_/3的分支里用了;/2（B = u ; B = false），这会直接创建选择点；另外，当变量未绑定时，Prolog无法确定是否还有其他可能的匹配，所以会留下选择点等待回溯。

要完全消除选择点，必须让谓词的所有分支互斥且覆盖所有合法情况，并且使用确定性的具体化谓词（比如reif库的if_/3、=/3、(\=)/3）来避免非确定性分支。

正确的无选择点实现 #

先明确三值逻辑OR的真值表：

根据真值表，用具体化谓词实现，确保每个条件互斥且确定性：

or3(A, B, C) :-
    if_( A = true,
         C = true,  % A为true时，结果一定是true
         if_( B = true,
              C = true,  % B为true时，结果一定是true
              if_( (A = false, B = false),
                   false,  % 两者都是false，结果为false，直接失败
                   if_( (A = false, B = u),
                        C = u,
                        if_( (A = u, B = false),
                             C = u,
                             (A = u, B = u, C = u)
                        )
                   )
              )
         )
    ).

或者更简洁的版本：

or3(A, B, C) :-
    (   A = true -> C = true
    ;   B = true -> C = true
    ;   A = false, B = false -> false
    ;   (A = false, B = u ; A = u, B = false ; A = u, B = u) -> C = u
    ).

验证查询结果 #

现在查询or3(A,false,C)，会得到：

?- or3(A,false,C).
A = true, C = true ;
A = u, C = u.

没有多余的false选择点，因为所有分支互斥且覆盖所有情况，Prolog能确定没有更多解。

关键要点 #

1. 避免非确定性分支：不要在if_/3的分支里用;/2，把每个可能的情况拆成互斥的确定性条件。
2. 覆盖所有合法情况：确保所有符合三值逻辑OR规则的输入都被覆盖，同时排除结果为false的情况。
3. 使用确定性谓词：用->/2（cut）或者reif库的具体化谓词，确保每个条件判断后不会留下选择点。

内容的提问来源于stack exchange，提问作者Luiz