Prolog 中 SAT 求解器的否定谓词 not/2

Negation predicate not/2 for SAT Solver in Prolog

我正在用 Prolog 编写 SAT 求解器。到目前为止,这是我能想到的:

cst(true).
cst(false).

is_true(cst(true)).
is_false(cst(false)).

and(A,B) :- 
    is_true(A),
    is_true(B).

or(A,B) :-
    is_true(A),
    is_false(B).
or(A,B) :-
    is_false(A),
    is_true(B).
or(A,B) :-
    and(A,B).

% not(A) :-  

我卡在 not/1 上了。谁能给我一个线索?

请注意,我没有使用 Prolog 的否定来解释逻辑否定。所以我改为实现了第二个谓词 is_false(+F),如果公式 F 为假,则为真。

编辑:我的意思是标题中的 not/1,而不是 not/2!

所以你的想法很好,但不可能嵌套你的条款。解决方案是在形式逻辑中使用像“解释”这样的谓词:将 is_trueis_false 拖到整个术语中:

is_true(cst(true)).
is_true(and(A,B)) :-
    is_true(A),
    is_true(B).
is_true(or(A,B)) :-
    is_true(A),
    is_false(B).
is_true(or(A,B)) :-
    is_false(A),
    is_true(B).
is_true(or(A,B)) :-
    is_true(A),
    is_true(B).
is_true(not(A)) :-
    is_false(A).

is_false(cst(false)).
is_false(and(A,B)) :-
    is_true(A),
    is_false(B).
is_false(and(A,B)) :-
    is_false(A),
    is_true(B).
is_false(and(A,B)) :-
    is_false(A),
    is_false(B).
is_false(or(A,B)):-
    is_false(A),
    is_false(B).   
is_false(not(A)) :-
    is_true(A).
    
?- is_true( or(not(and(cst(true), cst(false))), cst(false)) ).
true.

?- is_true( or(not(and(cst(true), cst(true))), cst(false)) ).
false.    

?- is_false( or(not(and(cst(true), cst(true))), cst(false)) ).
true.

?- is_false( or(not(and(cst(true), cst(false))), cst(false)) ).
false.