Hợp nhất Boolean trong Prolog?

Question

Tôi đang đấu tranh với alreay trong một thời gian dài với vấn đề sau đây. Tôi muốn làm cho sự hợp nhất thông thường của Prolog trở nên thông minh hơn.

Về cơ bản, tôi muốn rằng các biến nhất định hiểu rằng ví dụ 0 = ~ 1 và 1 = ~ 0. Điều này không hoạt động bình thường:

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

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

Tôi biết rằng CLP (B) có thể làm được:

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.

Nhưng tôi yêu cầu một thứ gì đó nhẹ hơn tải một thư viện CLP (B) đầy đủ. Có ý kiến ​​gì không?

Answer 1

Có vẻ như SWI-Prologs khi / 2 thực hiện công việc. Tôi đang sử dụng thuật toán Quine từ đây để đánh giá một phần biểu thức boolean. Sau đó, tôi có thể xác định một vị từ let / 2 Boolean:

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).

Vị từ trên sẽ đánh giá lại biểu thức được gán cho biến X khi một số biến bên trong biểu thức thay đổi. Biểu thức được kết hợp với biến X thông qua khi / 2. Vì chúng tôi thấy khi nào / 2 ở cấp cao nhất, chúng tôi thấy biểu thức được liên kết:

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

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

Và chúng tôi cũng có thể thực hiện trường hợp sử dụng của mình và thậm chí hơn thế nữa:

?- 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