Prolog中的布尔合一？

Question

我已经为以下问题挣扎了很长一段时间。我想让通常的Prolog统一更加智能。

基本上，我希望某些变量能够理解，例如0= ~1和1= ~0。这不能正常工作：

?- op(300, fy, ~).
true.

?- X = ~Y, Y = 0.
X = ~0,
Y = 0.

我知道中电(B)是可以做到的：

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)

:- use_module(library(clpb)).
true.

?- sat(X=:= ~Y), Y = 0.
X = 1,
Y = 0.

但是我需要比加载一个完整的CLP(B)库更轻量级的东西。有什么想法吗？

Answer 1

似乎SWI-Prologs when/2可以完成这项工作。我正在使用here的Quine算法对布尔表达式进行部分求值。然后我可以定义一个布尔值let/2谓词：

let(X, Y) :-
   eval(Y, H),
   term_variables(H, L),
   ( L== [] -> X = H;
      cond(L, R),
      when(R, let(X, H))).

cond([X], nonvar(X)) :- !.
cond([X,Y|Z], (nonvar(X);T)) :-
   cond([Y|Z], T).

当表达式中的某些变量发生变化时，上面的谓词将重新计算赋值给变量X的表达式。该表达式与变量X到when/2相关联。因为我们在顶层看到的是when/2，所以我们看到的是关联的表达式：

?- let(X, ~Y).
when(nonvar(Y), let(X, ~Y))

?- let(X, Y+Z).
when((nonvar(Y); nonvar(Z)), let(X, Y+Z))

我们还可以做我们的用例，甚至更多：

?- let(X, ~Y), Y = 0.
X = 1,
Y = 0.

?- let(X, Y+Z), Y = 0.
Y = 0,
when(nonvar(Z), let(X, Z))

?- let(X, Y+Z), Y = 0, Z = 1.
X = 1,
Y = 0,
Z = 1