Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

тарную сумму Ck, 1 <к <т, в дальнейшем рассматриваем как краткую запись дизъюнкта, зная, что по каждой переменной из Ck приписан квантор общности, находящийся в префиксе формулы С^. 3. Для множества дизъюнктов S = {Cj, С2 Ся} применяем метод резо­ люций. В логике предикатов можно реализовывать методы резолюций, использо­ вавшиеся в логике высказываний, естественно, включая в них необходимую унификацию. Важно реализовывать метод резолюций по четко определенной процедуре, иначе можно получить неверный результат. Рассмотрим следующий пример. Пусть дано множество дизъюнктов S, которые запишем для реализации метода резолюций (^ = S): \) ^(х,у) V Q (x,y) 2) -^{x,z) V ^Qiz,y) V Q{x,y) 3)P{b,b) 4) -nQ(y,b)v^Q{b,z) Начнем реализовывать метод исчерпания уровня, т. е. построение множе­ ства S^, и так далее: S^: 5) —J^{x,y) V -LP(X ', Х) V Q{X ',y') из 1), 2) 6)Q{b,b) из1), 3) 7) -^{x ,b) V -nQ{b ,z) из 1), 4) 8) -^{b,y) V -^Qiyb) из 1), 4) 9) -^Q{b,y) V -^Q{b,y) из 2), 3) 10) -^P{x,z) V -^Q{z,b) V -^Q{b,z') из 2), 4) 11) -^P{b,z) V -^Q{z,y) V -^Qiy ',b) из 2), 4) Теперь при построении множества S получим некоторые дизъюнкты, сре­ ди которых из 4) и 6) получим: к) -.Q{b,z) л Далее, при построении S из 6) и к) получим пустой дизъюнкт => Следова­ тельно, рассматриваемое множество дизъюнктов S невыполнимо (противоречиво). Для того же множества дизъюнктов S поступим следующим образом. Ис­ ходя из ^ (^ = S), сначала построим резольвенту дизъюнктов 2) и 4) выбирая в 4) самую правую литеру, затем будем строить резольвенты для последнего по­ лученного дизъюнкта (выбирая ее самую правую литеру) и дизъюнкта 2). В ре­ зультате имеем: 5) -^(b,z) V ^Q(z,y) V ^Q(y ',b) из 4), 2) 6) -^{x,z) V -nQ {z,b) V -^{b,z') V -nQ(z ',x) из 5), 2 ) 7) -nP (x,z) V -nQ(z,y) V -nF(x,z'') v -nQ (z ",b )v -^P{b ,x) из 6), 2) и так далее. Этот процесс будет бесконечным. Из этого примера и некото­ рых других рассуждений сделаем следующее важное замечание. 78