Я работаю над упражнением, в котором мне нужно показать, что 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, но оттуда я не знаю, как идти дальше. Был бы признателен за любую помощь. Спасибо!
Общее правило разрешения состоит в том, что для любых двух предложений (то есть дизъюнкций литералов)
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.
