使用 prolog 显示布尔逻辑失败的原因 [英] Use prolog to show cause of boolean logic failure

问题描述

假设我有以下布尔逻辑:

Suppose i have the following boolean logic:

Z = (A or B) and (A or C)

是否可以使用 prolog(可能与某些库一起使用)来找出 Z 为假的原因并以以下格式返回答案:

Is it possible to use prolog possibly (maybe together with some library) to figure out why Z is false and to return the answer in the following formats:

1. Z 是假的，因为 A 或 (b 和 c) 是假的
2. 如果我替换一些已知值(或全部)，比如 (c = true)，它会说:Z 是假的，因为 A 是假的
3. 它可以告诉我是哪个规则或规则的哪一部分导致了这个问题:Z 是错误的，因为 A 在Z = (A 或 B) 和 (A 或 C) 的 (A 或 B)?" 中是错误的?

1. Z is false because A or (b and c) are false
2. If i substitute some known values (or all) like (c = true) that it will say: Z is false because A is false
3. It can tell me which rule or which part of the rule causes this problem: Z is false because A is false in (A or B) of "Z = (A or B) and (A or C)?

同样的问题，当 Z = true 时，一切都相反.

Same questions again for when Z = true with everything in reverse.

或者这些问题不适合prolog，我应该看看一些SAT求解器或其他什么?

Or are these kind of questions not suitable for prolog and i should look at some SAT solver or something else?

我的目标是分析程序的数据流并回答诸如此类的问题.我希望这是真/假，但事实并非如此，这可能是什么?

My goal is to analyze dataflow of a program and figure answer questions like. I expect this to be true/false but it's not, what could it be?

推荐答案

不得不说这是一个很酷的问题.

I have to say this is kind of a cool problem.

我看到了两种基本方法，一种是使用 Prolog 的 read_term/2 来获取术语以及该术语中使用的变量名称，如下所示:

I see two fundamental approaches, one in which you use Prolog's read_term/2 to obtain a term along with the variable names used in the term, which would look something like this:

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

仔细想想，这对我来说似乎比它值得的麻烦更多，所以我想我会说明一个更简单"的版本，我们没有真正的变量，只有原子和一个单独的变量值列表.您可能可以在不做大量工作的情况下将下面的一个调整为上面的一个，但这似乎并不是解决问题的必要条件.

Giving it some thought, it seemed like this would be more trouble than it would be worth for me, so I thought I'll illustrate a "simpler" version where we don't really have variables, just atoms and a separate list of variable values. You probably could adapt the one below to the one above without a huge amount of work though, it just didn't seem really necessary to solving the problem.

首先我们需要支持这些操作符:

First we need to support these operators:

:- op(500, yfx, or).
:- op(400, yfx, and).

我继续并分别赋予这些与 + 和 * 相同的优先级，这对我来说似乎很直观.

I went ahead and gave these the same precedence as + and * respectively, that just seemed intuitive to me.

我将有一个变量和赋值的列表，例如 [x=true, y=false].我创建了一个谓词来管理它，但我最终认为它更好并删除了它，但请注意，我们在这里做出了这个决定.

I'm going to have a list of variables and assignments, like [x=true, y=false]. I created a predicate to manage that, but I thought the better of it eventually and removed it, but let's note that we made this decision here.

现在我的计划是创建一个评估谓词，该谓词将采用表达式和变量值赋值.它将为提供的表达式生成一个布尔值和一个原因".我将在这里作弊并使用is"运算符，但我这样做只是因为它对我来说很好读.最基本的一种术语是

Now my plan is to create an evaluation predicate that is going to take an expression and the variable-value assignments. It's going to produce a boolean for the supplied expression and a "reason". I'm going to cheat here and use the "is" operator, but I'm only doing this because it reads nicely to me. The most basic kind of term is

evaluate(X, Assignments, Value, X is Value) :-
    atom(X), memberchk(X=Value, Assignments).

所以我们现在可以支持像 x 这样的表达式:

So we can now support expressions like 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.假的也一样.但我们有理由，这就是你所追求的.那么接下来让我们处理或":

These are sort of like tautologies; if x=true, then the expression "x" is true because x=true. Likewise for false. But we have the reason there, which is what you're after. So let's handle "or" next:

evaluate(X or _, Assignments, true, Reason) :-
    evaluate(X,  Assignments, true, Reason).
evaluate(_ or Y, Assignments, true, Reason) :-
    evaluate(Y,  Assignments, true, Reason).

所以现在我们应该处理两者之一为真的情况:

So now we should handle the case where one of the two is true:

?- 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.但是我们还需要一个规则来处理错误的情况:

If we give it x=true and y=true, we will get two solutions, one for x and one for y. But we need one more rule for the false case:

evaluate(X or Y, Assignments, false, R1 and R2) :-
    evaluate(X,  Assignments, false, R1),
    evaluate(Y,  Assignments, false, R2).

所以这里的思路是注意or"两边都是假的，然后用and"结合原因.这样我们就得到了:

So the idea here is to notice that both sides of the "or" are false and then combine the reasons with "and". This way we get this:

?- evaluate(x or y, [x=false,y=false], V, R).
V = false,
R =  (x is false)and(y is false).

因为我们委派了双方，我们现在可以看到大而复杂的或"序列应该可以工作:

Because we delegate the sides, we can now see that large and complex "or" sequences should work:

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

您可以推断我们为或"所做的和"，其中我们基本上有两个错误案例和一个真实案例，而不是两个真实案例和一个错误案例:

You can extrapolate what we did for "or" for "and", where we basically have two false cases and one true case instead of two true cases and one false case:

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

这适用于您可能期望的一些有趣情况:

This works for some interesting cases you might expect:

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

在某些情况下这不是很有用，例如这种情况:

There are some situations where this isn't super useful, such as this one:

?- 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 的内容；也许我们可以找到一种方法，通过更聪明地结合孩子们的答案来简化答案.另一方面，它在这种情况下更有帮助:

As you can see the first solution is not super informative because we have already said something about a; maybe we could find a way to simplify the answer by combining the answers from the children more intelligently. On the other hand, it is somewhat more helpful in this case:

?- 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) 分支，应将其替换为:

Handling undefined values

The only piece that really needs to be changed to handle undefined values is the atom(X) branch, which should be replaced with this:

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 都会被生成.这似乎涵盖了您的其他用例，从完全通用的开始:

When a=false appears in the binding list, it will be used; if it doesn't appear, then both a=false and a=true will be generated. This appears to cover your other use cases, starting with the completely general:

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

并且您可以将搜索限制为产生您感兴趣的值的案例:

And you can restrict the search to cases that produce the value you're interested in:

?- 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.因此，您添加到表达式中的每个未定义变量都会使搜索空间加倍.如果这就是您所担心的低效率，那么这对您来说可能不是一个理想的解决方案(或者，它可能没问题，您可以尝试一下，看看它是否可以忍受).

Of course, Prolog isn't doing anything especially smart here; it isn't trying to work backwards to figure out what values of b and c are going to lead to false, it's just generating all the possibilities and trying to unify their evaluation with false. So each undefined variable you add to the expression is going to double the search space. If this is the inefficiency you're worried about, this may not be an ideal solution for you (or, it might be fine, you might try it and see if it's tolerable).

如果您主要关心的是性能，我认为您可能想要研究 SAT 求解器，尽管我不知道他们是否能够为您的推理提供理由".

I think you might want to look into SAT solvers if your primary concern is performance, although I don't know offhand if they are capable of giving you "reasons" back for their inferences.

这篇关于使用 prolog 显示布尔逻辑失败的原因的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！