0

如果我有两个前提如下：

  1. a -> c (a 暗示 c)
  2. b -> c (b 暗示 c)

并得出一个结论：

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

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

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

或者，每个带有真值表的证明，该真值表包含一条表示前提为真但结论为假的行：

具有真前提和假结论的真值表

我的问题是：“有没有办法使用 prolog 来证明陈述 #1 和 #2 的断言与陈述 #3 的结论相矛盾？如果是这样，那么有什么清晰简洁的方法可以做到这一点？”

4

2 回答 2

2

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

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

主要区别在于我为每个前提发布了单独 sat/1的约束，然后用于taut/2查看结论是否来自前提。

第一个前提是：

a → c

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

sat(A =< C)

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

sat(B =< C)

如果 a → b 从这些前提出发，那么taut/2将成功T = 1：

?- sat(A =< C), sat(B =< C), taut(A =< B, T)。
假的。

既然没有，我们就知道结论不是从前提中得出的。

我们可以要求 CLP(B) 给出一个反例，即将真值分配给 a → c 和 b → c 都成立，而 a → b 不成立的变量：

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

简单地发布约束就足以显示在这种情况下存在的唯一反例。如果反例不是唯一的，我们可以使用labeling/1生成地面实例，例如：labeling([A,B,C]).

为了比较，例如考虑：

?- sat(A =< B), sat(B =< C), taut(A =< C, T)。
T = 1 ,
坐（A=:=A*B），
坐（B=:=B*C）。

这表明 a → c 遵循 a → b ∧ b → c。

于 2016-10-15T07:46:21.197 回答
1

您可以使用 library(clpb)：

首先将表达式分配给变量 Expr：

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

注意：

  • '+' 代表逻辑或

  • '*' 表示逻辑与

  • '~' 表示逻辑 NOT 也A->B等同于A+(~B). 所以上面的表达式等价于((A->C),(B->C))-> (A->C)我们写'->'using+,~和','with 的地方*。

现在如果我们查询：

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

谓词taut/2将 clpb 表达式作为输入，如果它重言式则返回 T=1，如果表达式不能满足并且在任何其他情况下失败，则返回 T=0。因此，上述查询失败的事实意味着 Expr 不是重言式，既不能满足，也意味着可以满足。

也可以通过查询：

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

Predicatesat/1返回 True 如果布尔表达式是可满足的，并且在以下情况下给出上述表达式可满足的答案：

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

哪里'#'是，exclusive OR这意味着你的表达（我们从 taut/2 知道是可满足的）在满足时1#C#C*B得到满足。

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

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]].
于 2016-10-15T07:04:08.060 回答