关于使用解析对某些子句进行反驳的问题

Question

我正在为人工智能课程做作业，目前我遇到了一个问题，即要找到对某些条款的反驳。

我尝试了很多方法来找到关于这些子句的反驳，但是，它要么以我试图找到的相同目标子句结束，要么以越来越多的子句结束。

下面是用 Prolog 格式编写的子句：

% A1
i(e, X, X).

% A2
i(X, e, X).

% A3
i(comp(X), X, e).

% A4
i(X, comp(X), e).

% A51
i(U, Z, W) :- i(X, Y, U), i(Y, Z, V), i(X, V, W).

% A52
i(X, V, W) :- i(X, Y, U), i(Y, Z, V), i(U, Z, W).

% A6
i(X, X, e).

% A7
i(a, b, c).

% A8
-i(b, a, c)

如果你有任何想法，请帮助我，非常感谢！

编辑：

我想向您展示我的尝试，但它是手写的，很难打出来。基本上，我首先尝试使用 unifier e1 = [U/b, Z/a, W/c] 解析 A8 和 A51，最后得到 -i(b, a, c)。我还尝试首先使用统一器 e2 = [U/e, Z/X, W/X] 解析 A1 和 A51，最终得到 -i(M, M, M) 的所有可能组合，其中 M 属于 {a , b, c, e} 例如：-i(b, b, a)

Answer 1

我不太擅长 Prolog，但这里有一个 Isabelle 的反驳证明（为了好玩）。

lemma so55485292:
  fixes i a b c e
  assumes A1:  "⋀X. i(e, X, X)"
      and A51: "⋀U V W X Y Z. ⟦ i(X, Y, U); i(Y, Z, V); i(X, V, W) ⟧ ⟹ i(U, Z, W)"
      and A52: "⋀U V W X Y Z. ⟦ i(X, Y, U); i(Y, Z, V); i(U, Z, W) ⟧ ⟹ i(X, V, W)"
      and A6:  "⋀X. i(X, X, e)"
      and A7:  "i(a, b, c)"
      and A8:  "¬i(b, a, c)"
    shows False
proof -
  have swap: "⋀s t u. i(s, t, u) ⟹ i (u, t, s)"
  proof -
    fix s t u
    assume "i(s, t, u)"
    moreover have "i(t, t, e)" by (rule A6)
    moreover have "i(s, e, s)"
    proof (rule A52)
      show "i(s, s, e)" by (rule A6)
      show "i(s, s, e)" by (rule A6)
      show "i(e, s, s)" by (rule A1)
    qed
    ultimately show "i(u, t, s)" by (rule A51)
  qed

  have "i (a, c, b)"
  proof (rule A52)
    show "i(a, a, e)" by (rule A6)
    show "i(a, b, c)" by (rule A7)
    show "i(e, b, b)" by (rule A1)
  qed
  from this have "i (b, c, a)" by (rule swap)
  moreover have "i(c, b, a)" using A7 by (rule swap)
  ultimately have "i(b, a, c)" using A7 by (rule A52)

  from A8 and this show ?thesis ..
qed

（很遗憾，美丽的 Isar 语言没有语法高亮显示……）

A2、A3 和 A4 是多余的。 Isabelle 可以使用sledgehammer 很快证明存在证明。从自动证明中挑出一个解释性 Isar 证明需要更长的时间和一些反复试验。

对于 Prolog，您可能需要通过削减消除来消除 swap 引理。