关于使用解决方案来查找某些条款的驳斥的问题

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）结束。我也尝试先用unifier 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是多余的。伊莎贝尔可以证明使用sledgehammer很快就能证明存在证据。花了一点时间和一些试验和错误来取消自动证明中的解释性Isar证明。

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