序言可以用来确定无效推理吗？

Question

如果我有两个前提如下：

a -> c（a 表示 c）
b -> c（b 表示 c）

以及得出的结论：

a -> b（a 因此意味着 b），

那么结论可以证明是无效的，因为：

a -> c 在 a 为真且 c 为真时对语句 #1 有效，并且当 b 为假且 c 为真时，b -> c 对语句 #2 有效。当 a 为真 b 为假时，这导致 a -> b，这与语句 #3 直接矛盾。

或者，每个证明 table 包含前提为真但结论为假的行：

Truth Table with true premises and false conclusion

我的问题是："Is there a way to use prolog to show that the assertions of statements #1 and #2 contradict the conclusion of statement #3? If so, what is a clear and concise way to do so?"

Answer 1

你可以使用 library(clpb):

首先将你的表达式赋值给一个变量 Expr:

Expr = ((A + ~C)*(B + ~C)+(~(A + ~B)).

注意：

'+'代表逻辑或
'*' 逻辑与
'~' 逻辑非 A->B 也等同于 A+(~B)。所以上面的表达式等同于 ((A->C),(B->C))-> (A->C) 我们用 +,~ 和 ',' 和 *.

'->'

现在如果我们查询：

?-  use_module(library(clpb)).
true.
?- Expr=((A + ~C)*(B + ~C))+(~(A + ~B)),taut(Expr,T).
false.

Predicate taut/2 将 clpb 表达式作为输入，如果是重言式 returns T=1，如果不能满足表达式则 T=0 并失败在任何其他情况下。所以上面查询失败的事实意味着 Expr 也不是重言式 neither 不能被满足，这意味着它可以被满足。

同样通过查询：

?- Expr=((A + ~C)*(B + ~C))+(~(A + ~B)),sat(Expr).
Expr = (A+ ~C)* (B+ ~C)+ ~ (A+ ~B),
sat(1#C#C*B),
sat(A=:=A).

Predicate sat/1 returns 真当且仅当布尔表达式是可满足的并且给出上述表达式可满足的答案时：

sat(1#C#C*B),
sat(A=:=A).

其中 '#' 是 exclusive OR，这意味着当 1#C#C*B 满足时，您的表达式（我们从 taut/2 知道它是可满足的）也满足。

另一种不使用库的解决方案可能是：

truth(X):-member(X,[true,false]).

test_truth(A,B,C):-
  truth(A),
  truth(B),
  truth(C),
  ((A->C),(B->C)->(A->C)).

示例：

?- test_truth(A,B,C).
A = B, B = C, C = true ;
false.

此外，如果我从你的评论中理解正确，要收集所有可能的解决方案，你可以写：

?- findall([A,B,C],test_truth(A,B,C),L).
L = [[true, true, true]].

它给出了一个列表列表，其中内部列表在上面的示例中具有 [true,true,true] 的形式，这意味着解决方案是 A=true,B=true,C=true 并且在上述情况下它只有一个解决方案。

找出所有你能写的矛盾：

 truth(X):-member(X,[true,false]).

    test_truth(A,B,C):-
      truth(A),
      truth(B),
      truth(C),
    not( (\+ ((\+A; C),(\+B ; C)) ; (\+A ; B)) ).

最后一行也可以写成：

not( ( (A->C;true),(B->C;true) ) -> (A->B;true) ;true ).

示例：

  ?- findall([A,B,C],test_truth(A,B,C),L).
L = [[true, false, true]].

Answer 2

@coder 已经给出了很好的答案，使用 clpb 约束。

我想展示一种稍微不同的方式来证明结论不是从前提得出的，同样使用 CLP(B)。

主要区别是我post个人sat/1约束每个前提，然后用taut/2看是否从前提得出结论。

第一个前提是：

a → c

在 CLP(B) 中，您可以将其表示为：

sat(A =< C)

第二个前提，即b → c、变为：

sat(B =< C)

如果一个→ b 遵循这些前提，然后 taut/2 将成功并且 T = 1 in:

?- sat(A =< C), sat(B =< C), taut(A =< B, T).
false.

既然不成立，我们就知道结论不是从前提得出的。

我们可以要求 CLP(B) 显示一个反例，即，将真值赋给变量，其中 a → c 和 b 右箭头; c 都成立，a 右箭头; b 不成立：

?- sat(A =< C), sat(B =< C), sat(~(A =< B)).
A = C, C = 1,
B = 0.

只需 post 约束 就足以 显示在这种情况下存在的唯一反例。如果反例不是唯一的，我们可以使用 labeling/1 来生成基础实例，例如：labeling([A,B,C]).

为了比较，考虑例如：

?- sat(A =< B), sat(B =< C), taut(A =< C, T).
T = 1,
sat(A=:=A*B),
sat(B=:=B*C).

这表明一个 → c 源自 a → b ∧ b 右箭头; c.

序言可以用来确定无效推理吗？

Can prolog be used to determine invalid inference?

logic

boolean-logic

prolog

clpb