Список клауз (дизъюнктов): 1.¬P∨Q 2.¬Q∨¬R 3.P∨S 4.¬S∨¬R 5.R∨T 6.¬T (отрицание заключения) — задача №575922

Для того чтобы доказать, что заключение является логическим следствием данных посылок, мы воспользуемся методом резолюций. Согласно этому методу, если множество дизъюнктов (клауз) противоречиво (приводит к пустой клаузе $\square$), то исходное утверждение является истинным.

Дано (список клауз):

1. $C_1: \neg P \lor Q$
2. $C_2: \neg Q \lor \neg R$
3. $C_3: P \lor S$
4. $C_4: \neg S \lor \neg R$
5. $C_5: R \lor T$
6. $C_6: \neg T$ (отрицание заключения)

Найти:

Доказать, что из посылок $C_1, C_2, C_3, C_4, C_5$ следует заключение, которое при отрицании дает $C_6$.

Решение:...