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

во такое, что S выполнимо тогда и только тогда, когда 5"* выполнимо (ис­ пользуйте результаты упражнений 9-12): a)S={Av^B, Bv^C, CvD, Av^D); Q)S= [AvBvC, ^B, Av^CvD, BvD, Av^D); b)8= {AvBvCvD, ^BvCvD, -AvCvD, BvD, -AvD}; T )S={^ V B, B V C V D, -A V ^B V C V D, -A, B). 14. С помощью метода резолюций доказать, что следующее множество дизъюнктов невыполнимо: 2i){^Pv^QvR, PvR, QvR, -.R]; 6){^v5, -^BvC, -nCvA, AvC, -Av^Cj; 15. Методом резолюций, используя метод исчерпания уровней, доказать, что следующее множество дизъюнктов невыполнимо: Si){PvQvR, -^vR, ^Q, ^R; 6)PvQ, -^QvR, ^PvQ, ^R}. 16. Пусть S ={P,Q,R,W, -nP V —iQ V—iRv—iW}. Сколько резольвент будет по­ рождено из S методом насыщения уровня до того, как будет получен пустой дизъюнкт? 17. Для S ={P,Q,R,W, -nPv —iQv—iRv—iW} получить пустой дизъюнкт, ис­ пользуя лок-резолюцию. 18. Для S ={ PvQvR, -^PvR, —ig, —li?} получить пустой дизъюнкт, ис­ пользуя лок-резолюцию. 19. Используя метод резолюций, докажите, что: а) [А^В, C^D, D^B, BvCvD) |= А&В; б) {А&В^С,А^В] 1= А ^ С ; в) {А vB, А^ С, B^D}\= С vD. 20. Решите задачу 5 данной главы, используя метод резолюций. 21. Найти сколемовские стандартные формы для следующих формул: 2i)3xVy Vz(P(x,y) =^(x,z)); б) ЗхЗу Vz(P(x,y) =^(x,z)); в) Vx3y Vz(P(x,y) =^2(x,z)); г) \/x Vy3z(P(x,y) =^(x,z)). 22. Найти сколемовские стандартные формы для следующих формул: д) 3x3y(VzP(x,y) ^Q(x,z)): б) VxQ(x) ^ЗхР(х); в) VxVy(3z(P(x,y)&P(y,z)) ^3vQ(x,y,v)); г) Vx(P(x) ^3yQ(x,y)); д) Зх(Р(х) => VyQ(x,y)); е) Зх( 1(ЗуР(х,у)) ^(3zQ(z) =>R(x))); ж) Vx3y(VzP(x,y,z)&(3uQ(x,u) =^3vQ(y,v))). 23. Определить, унифицируемо ли каждое ли из следующих множеств: г){Р(а),Р(Ь)}; 6) {Р(х), P(f(x))}; в) {Р(а), P(f(x))}; г) {Р(а,х), Р(а,а)}; Д) {P(a,f(x)), Р(х,у)}; е) {Q(f(a),g(x)), Q(y,y)y, ж) {P(x,z,y), P(w,u,w), Р(а,и,и)]. 24. Определить, унифицируемо ли каждое ли из следующих множеств: 94