假设我有以下布尔逻辑：
Z = (A or B) and (A or C)
是否有可能使用prolog（可能与某些库一起）来弄清楚为什么Z是假的并以下列格式返回答案：
同样的问题，当Z =真时，一切都反过来。
或者这些问题不适合prolog，我应该看一些SAT求解器或其他东西？
我的目标是分析程序的数据流并计算答案问题。我希望这是真/假，但它不是，它可能是什么？
我不得不说这是一个很酷的问题。
我看到两种基本方法，其中一种方法是使用Prolog的read_term/2来获得一个术语以及术语中使用的变量名称，它们看起来像这样：
?- read_term(T, [variable_names(Names)]).
|: X and Y or Z and Q.
T = _5700 and _5702 or _5706 and _5708,
Names = ['X'=_5700, 'Y'=_5702, 'Z'=_5706, 'Q'=_5708].
给它一些想法，似乎这会比我的价值更麻烦，所以我想我会说明一个“更简单”的版本，我们没有真正的变量，只是原子和一个单独的变量列表值。你可能可以在不需要大量工作的情况下将下面的那个调整到上面那个，但它似乎没有必要解决问题。
首先，我们需要支持这些运营商：
:- op(500, yfx, or).
:- op(400, yfx, and).
我继续前进并分别给出了与+和*相同的优先级，这对我来说似乎很直观。
我将有一个变量和分配列表，如[x=true, y=false]。我创建了一个谓词来管理它，但我最终认为它更好并删除它，但让我们注意到我们在这里做出了这个决定。
现在我的计划是创建一个评估谓词，它将采用表达式和变量值赋值。它将为所提供的表达式和“原因”生成一个布尔值。我要在这里作弊并使用“is”操作符，但我只是这样做，因为它对我来说很好看。最基本的术语是
evaluate(X, Assignments, Value, X is Value) :-
atom(X), memberchk(X=Value, Assignments).
所以我们现在可以支持像x这样的表达式：
?- evaluate(x, [x=true], V, R).
V = true,
R = (x is true).
?- evaluate(x, [x=false], V, R).
V = false,
R = (x is false).
这有点像重言式;如果x = true，则表达式“x”为真，因为x = true。同样是假的。但我们有理由，这就是你所追求的。那么让我们处理“或”下一步：
evaluate(X or _, Assignments, true, Reason) :-
evaluate(X, Assignments, true, Reason).
evaluate(_ or Y, Assignments, true, Reason) :-
evaluate(Y, Assignments, true, Reason).
所以现在我们应该处理其中一个是真的情况：
?- evaluate(x or y, [x=true,y=false], V, R).
V = true,
R = (x is true) ;
false.
?- evaluate(x or y, [x=false,y=true], V, R).
V = true,
R = (y is true) ;
false.
如果我们给它x = true和y = true，我们将得到两个解，一个用于x，一个用于y。但我们还需要一个针对虚假案例的规则：
evaluate(X or Y, Assignments, false, R1 and R2) :-
evaluate(X, Assignments, false, R1),
evaluate(Y, Assignments, false, R2).
因此，这里的想法是注意“或”的两边都是假的，然后将原因与“和”结合起来。这样我们得到这个：
?- evaluate(x or y, [x=false,y=false], V, R).
V = false,
R = (x is false)and(y is false).
因为我们委托双方，我们现在可以看到大而复杂的“或”序列应该起作用：
?- evaluate(a or b or c or d or e, [a=false,b=false,c=false,d=true,e=false], V, R).
V = true,
R = (d is true) ;
false.
你可以推断我们为“和”为“和”所做的事情，其中我们基本上有两个错误案例和一个真实案例，而不是两个真实案例和一个虚假案例：
evaluate(X and Y, Assignments, true, R1 and R2) :-
evaluate(X, Assignments, true, R1),
evaluate(Y, Assignments, true, R2).
evaluate(X and _, Assignments, false, Reason) :-
evaluate(X, Assignments, false, Reason).
evaluate(_ and Y, Assignments, false, Reason) :-
evaluate(Y, Assignments, false, Reason).
这适用于您可能期望的一些有趣案例：
?- evaluate(x and y or z, [x=true, y=true, z=false], V, R).
V = true,
R = (x is true)and(y is true) ;
false.
?- evaluate(x and y or z, [x=false, y=false, z=true], V, R).
V = true,
R = (z is true) ;
false.
在某些情况下，这不是非常有用的，例如：
?- evaluate((a or b) and (a or c), [a=true,b=false,c=false], V, R).
V = true,
R = (a is true)and(a is true) ;
false.
正如你所看到的，第一个解决方案不是超级信息，因为我们已经说过关于a的一些内容;也许我们可以通过更聪明地结合儿童的答案来找到简化答案的方法。另一方面，在这种情况下，它更有帮助：
?- evaluate((a or b) and (a or c), [a=false,b=false,c=false], V, R).
V = false,
R = (a is false)and(b is false) ;
V = false,
R = (a is false)and(c is false).
?- evaluate((a or b) and (a or c), [a=false,b=true,c=true], V, R).
V = true,
R = (b is true)and(c is true) ;
false.
真正需要更改以处理未定义值的唯一部分是atom(X)分支，应该替换为：
evaluate(X, Assignments, Value, X is Value) :-
atom(X),
( memberchk(X=V, Assignments) ->
Value = V
; member(Value, [true,false])
).
当a=false出现在绑定列表中时，它将被使用;如果它没有出现，那么将生成a=false和a=true。这似乎涵盖了您的其他用例，从完全一般的开始：
?- evaluate((a or b) and (a or c), [a=false], V, Reason).
V = true,
Reason = (b is true)and(c is true) ;
V = false,
Reason = (a is false)and(b is false) ;
V = false,
Reason = (a is false)and(c is false).
您可以将搜索限制为产生您感兴趣的值的案例：
?- evaluate((a or b) and (a or c), [a=false], false, Reason).
Reason = (a is false)and(b is false) ;
Reason = (a is false)and(c is false).
当然，Prolog在这里并没有做任何特别聪明的事情;它不是试图倒退来弄清楚b和c会导致什么样的错误，它只是产生了所有的可能性并试图用false统一他们的评价。因此，您添加到表达式中的每个未定义变量将使搜索空间加倍。如果这是你担心的低效率，这对你来说可能不是一个理想的解决方案（或者，可能没问题，你可以尝试一下，看看它是否可以忍受）。
如果你主要关心的是表现，我想你可能想看看SAT求解器，虽然我不知道他们是否有能力为你的推论提供“理由”。