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

【问题标题】：Negation predicate not/2 for SAT Solver in PrologProlog中SAT求解器的否定谓词not/2
【发布时间】：2020-11-16 13:46:11
【问题描述】：

我正在用 Prolog 编写一个 SAT Solver。到目前为止，这是我能想到的：

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！

【问题讨论】：

SWISH 告诉我“head_build_in”，所以我不能使用 'not' 作为名称？
啊是的，not 是关键字，你必须为谓词使用另一个名称
好的，该程序似乎运行良好。谢谢！
你打算运行类似and(A,or(B,nott(C)))的东西吗？
在示例中，他们提出查询：?- is_true( or(not(and(cst(true), cst(false))), cst(false)) )。并得到真实。我用自己的程序弄错了。我是不是在什么地方搞砸了？我想我有点误解了这个任务。显然 is_true(F) 是他们想要的。

标签： prolog logic sat negation

【解决方案1】：

所以你的想法很好，但不可能嵌套你的条款。解决方案是在形式逻辑中使用诸如“解释”之类的谓词：将is_true 或is_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.

【讨论】：

感谢您的回复。我不太明白为什么我的代码不能嵌套。我想我错过了一些核心的序言想法。
你有像讲座这样的逻辑背景还是你在为学校做这个？