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

значение И, тогда 1 Р=Л, поэтому должно быть Вг*=И, следователь­ но, Di*vD2*=if. Таким образом, из истинности D\ и D: получили истинность D\*wDi*. В случае, если на к-ш наборе Р~Л, то В\*=И и вновь полу­ чаем, что из истинности Di и Вг следует истинность DiVD^*. В силу произвольности выбранного набора получаем, что из истинности А и Di следует истинность для D1VD2*, что и требовалось доказать. Следует поставить перед собой цепь изыскать способ решения всех задач ... одним и притом простым способом. Дапамбер § 3. Метод резолюций в логике высказываний Рассмотрим задачу выяснения, будет ли В логическим следствием т.е. истинна ли следующая запись: j=-S. В § 1 данной главы показано, что эта задача сводится к выясне­ нию невыполнимости формы С =А 1&Л2&... &Ат&~\ в. Найдем для формулы С ее к.н.ф., то есть получим конъюнкцию дизъюнктов: C=Di&.Di&...&Dk. Множество дизъюнктов {DbD:,...,!)*} считается невыполнимым тогда и только тогда, когда формула С невыполнима. Методом резолюций называется последовательное получение бинарных резольвент из данных дизъюнктов и вновь получаемых дизъюнктов. Пусть, например, даны дизъюнкты D,=Pvr, D2=1Pv7', 1)л=1Г. Используя Di и D2, затем Di и D3 , получим резольвенты D^^T, Ds=P, затем из D3 и D4 - пустой дизъюнкт, который будем обозначать через •. Можно доказать следующую теорему. 93