Вопрос об использовании разрешения, чтобы найти опровержение о некоторых пунктах - PullRequest
Новая
       11

Вопрос об использовании разрешения, чтобы найти опровержение о некоторых пунктах

0 голосов
/ 03 апреля 2019

Я делаю домашнее задание по курсу искусственного интеллекта, и в настоящее время я застрял в вопросе о поиске опровержения по некоторым пунктам.

Однако я попытался найти много способов найти опровержение по этим пунктам., он либо заканчивался тем же предложением цели, которое я пытался найти, либо заканчивал все большим и большим количеством предложений.

Вот предложения, написанные в формате Пролога: 

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

Если у вас есть идеи, пожалуйста, помогите мне, большое спасибо!

Редактировать:

Я хотел показать вам свои попытки, но это было написано от руки, и их сложно напечатать,По сути, я сначала попытался разрешить A8 и A51 с помощью унификатора e1 = [U / b, Z / a, W / c], и в итоге получился ключ -i (b, a, c).Я также попытался сначала разрешить A1 и A51 с помощью объединителя e2 = [U / e, Z / X, W / X], и в итоге получились все возможные комбинации -i (M, M, M), где M принадлежит {a, b, c, e} например: -i (b, b, a)

1 Ответ

0 голосов
/ 08 апреля 2019

Я не очень хорош в Прологе, но вот доказательство опровержения Изабель (ради интереса). 

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

(Жаль, что нет подсветки синтаксиса для прекрасного языка Изара ...)

A2, A3 и A4 являются избыточными. Изабель может показать, что доказательство существует очень быстро, используя sledgehammer. Потребовалось немного больше времени и проб и ошибок, чтобы дразнить объяснение Изара из автоматического доказательства.

Для Пролога вам, вероятно, нужно исключить лемму swap путем исключения срезов.

...