Дискретка. Метод резолюции. Опции

[HelpPliz]

2) Методом резолюции доказать, что

{A-->B, C-->D, D-->B, B v C v D} |- B v C

кто поможет большое спасибо...

[Michael_Rybak]

{A-->B, C-->D, D-->B, B v C v D} |- B v C

добавляем отрицание результата

{A-->B, C-->D, D-->B, B v C v D, not (B v C)} |- 0

отбрасываем первые два конъюнкта

{D-->B, B v C v D, not (B v C)} |- 0

добавляем резольвенту первого и второго конъюнктов: (D->B) and (B or C or D) => B or C (доказать)

{D-->B, B v C v D, (B v C), not (B v C)} |- 0

оставляем резольвенту последних двух:

0 |- 0