Математическая логика и теория алгоритмов

(i),)B = Р{а) V Q{a) , {D2), = 1 Р{а) v Т{у). Отбрасываем литеры Р (а),1 Р (а) и получим бинарную резольвенту: Л =2 (ci)vT(y). Пусть имеем Di= 1 Р(х) v Q(x), =1 Q{x) v T(x). Тогда ^ = 1 6(У) V Г(у) и Л = 1P (у) V r (у). Резольвентой дизъюнктов - посылок i>i и D2 - называется одна из следующих бинарных резольвент: 1) бинарная резольвента Di и Di, 2) бинарная резольвента JDI И склейки D2, 3) бинарная резольвента D2 и склейки Di, 4) бинарная резольвента склейки D\ и склейки D2. Применение описанных резольвент к множеству дизъюнктов и называется методом резолюций. Можно доказать следующую важную теорему. Теорема 3.10. (полнота метода резолюций). Множество S дизъюнктов невыполнимо тогда и только тогда, когда существует вы­ вод пустого дизъюнкта из S. \ Проблема дедукции логики предикатов состоит, как и в логике высказываний, в выяснении: будет ли формула В логическим следст­ вием формулЛь Л2, Теоремы 3.1—3.4, доказанные для логики высказываний, молено распространить и для логики предикатов, записывая всюду вместо слова «тавтология» слова «логически общезначимая формула». Из изложенного можно получить следующую последователь­ ность действий для выяснения; будет ли формула В логическим след­ ствием формул 1,^2) 1. Строим конъюнкцию С = AiSiAiSc ...Sc Л„.8с]В. Отметим, что требуемое следствие (заключение) взято с отрицанием. 112