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

b^i Vx2... Vxk (Ci V C2 V ... V C „), где Ci , \ <i <n - литералы, a Xi, X2, Xk все переменные встречающиеся в Ci, С2, Сп- При и =О получим пустой дизъюнкт, который обозначается симво­ лом => Таким образом, дизъюнкт содержит кванторы общности по всем пе­ ременным, которые имеются во всех литерах Ci,С 2 , , С„. Рассмотрим процедуру получения дизъюнктов. Для заданной замкнутой формулы вынесем кванторы за скобки, т.е. получим предваренную нормальную форму: А ~ QjXj Q2X2...QnX „B, здесь В - матрица формулы, а QiXiQ2X2...QnX „- префикс. Будем считать, что матрица приведена к конъюнктивной нормальной форме. Далее проведём исключение кванторов существования введением сколе- мовских функций (Skolem Т) следующим образом. Пусть А= Q1X1Q2X2... Qn^nB, где QjXj, Q2X2,Qn^n - кванторы всеобщности или существования. Положим, что QrXr - квантор существования в префиксе Q i ^ i Q2^2- - QnXn, п. Если никакой квантор всеобщности не стоит в префиксе левее то выбираем новую предметную постоянную с, отличную от всех предметных постоянных в Д и заменяем все х^, встречающиеся вв , на с и вы­ черкиваем из префикса. Покажем это на примере. Пусть имеем формулу Зс Vy(Pl (x,y)^>Q \ (х,а)). Тогда для исключения квантора Вх введем постоянную с. В результате получим формулу: Vy(Pl (c,y)^>Ql (с,а)). Рассмотрим другой пример. Пусть имеем формулу 3x3yVz(P\(x,y,z)^>Ql(a,b,x,y)). Тогда, исключая кванторы существования, по­ лучим: Vz(P\(c,d,z)^Q\ (a,b,c,d)). Если Qxsj, Qxs^, -, - список всех кванторов всеобщности, встречаю­ щихся левее квантора существования QrXr^, 1< Si< S2<... < s „< п, то выберем но­ вую m - местную функциональную букву/", отличную от функциональных букв из В, заменим все ХгВ В Haf"{xsj,xs2' ••• '^sj и вычеркнем Q,Xr из префикса. Пример. Пусть имеем фотрмуяу\/х^(Р(х,у)^^(/1(а),у)). Введя функцию/2, с аргументом х и исключая импликацию, получим: Vx(-^(x, f2(x)) vQ(fi(a), f2(x))). Пример. Пусть имеем формулу: VxVy3z(P(x,y)^ R(x,z,fi(x ),f2(f3 (z)))). Вводя необходимую функцию и исключая импликацию, получим: VxVy( —P(x,y)v R(x,f4(x,y),fi(x),f2(f3(f4(x,y))))). Проводим описанную процедуру до тех пор, пока не исключим все кван­ торы существования. Полученная в результате формула есть сколемовская стандартная форма, кратко - стандартная форма формулы А. Константы и 70