Доказательство резолюцией - Искусственный интеллект

Question

Я работаю с упражнением, где мне нужно показать, что KB |= ~D,

И я знаю, что База знаний это:

 - (B v ¬C) => ¬A
 - (¬A v D) => B
 - A ∧ C

После преобразования в CNF:

A ∧ C ∧ (¬A v ¬B) ∧ (¬A v C) ∧ (A v B) ∧ (B v ¬D)

Так что теперь я перешел на CNF, но оттуда я не знаю, как идти дальше. Буду признателен за любую помощь. Спасибо!

Answer 1

Общее правило разрешения таково, что для любых двух предложений (то есть, дизъюнкций литералов)

P_1 v ... v P_n

а также

Q_1 v ... v Q_m

в вашем CNF, так что есть i и j, где P_i и Q_j являются отрицанием друг друга, вы можете добавить новое предложение

P_1 v ... v P_{i-1} v P_{i+1} ... v P_n v Q_1 v ... v Q_{j-1} v Q_{j+1} ... v Q_m

Это просто строгий способ сказать, что вы можете сформировать новое предложение, соединив два из них, за исключением литерала с противоположными "знаками" в каждом.

Например

(A v ¬B)∧(B v ¬C)

эквивалентно

(A v ¬B)∧(B v ¬C)∧(A v ¬C),

присоединившись к двум пунктам при удалении противоположностей B а также ¬B, получение A v ¬C,

Другой пример

A∧(¬A v ¬C)

что эквивалентно

A∧(¬A v ¬C) ∧ ¬C.

поскольку A считается как предложение с одним литералом (A сам). Таким образом, эти два пункта объединены, в то время как A а также ¬A удаляются, давая новый пункт ¬C,

Применяя это к вашей проблеме, мы можем решить A а также ¬A v ¬B, получение ¬B, Затем мы решаем этот новый пункт ¬B с B v ¬D, получение ¬D,

Поскольку CNF является соединением, тот факт, что он имеет место, означает, что каждое предложение в нем выполняется. То есть CNF подразумевает все его пункты. поскольку ¬D является одним из его пунктов, ¬D подразумевается CNF. Поскольку CNF эквивалентен исходному KB, KB подразумевает ¬D,