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

функции, используемые для замены переменных квантора существования, на­ зываются сколемовскими функциями. Пример. Пусть имеем формулу Vx3yBz( —iP(x,y)&R(x,z)vS(x,y,z)). Приведём матрицу формулы к Vx3y3z( —iP(x,y)vS(x,y,z))&(R(x,z) vS(x,y,z)). Затем введём функции f(x), g(x): Vx(^(x,f(x)) vS(x,f(x),g(x))&(R(x,g(x)) vS(x,f(x),g(x))). Полученная формула является стандартной формой исходной формулы. Процесс «сколемизации» формулы (как уже указано, имеем дело с замкну­ той формулой) представляется в следующем виде. а) на входе исходная (замкнутая) формула/!; б) переименовываем переменные (если это нужно); в) переносим отрицания через кванторы вправо доводя их до элементар­ ных формул; г) выносим все кванторы за скобки; д) приводим матрицу к к.н.ф.; е) удаляем кванторы существования, вводя в матрицу сколемовские функции. В результате получим сколемовскую стандартную форму. Рассмотрим пример. а) исходная формула: В = Зх Vy(P(x) V -Q(y))^ -пБу VxR(x,y); б) переименовываем переменные: В = Зх Vy(P(x) V —Q(y))^ —,3z VwR (z,w); в) переносим отрицание: В = Зх Vy(P(x)v —Q(y))^ Vz3w—iR(z,w); г) выносим все кванторы за скобки: В= Vx3yVz3w((P(x)v 4Q(y))^ —R(z,w))\ д) приводим матрицу к к.н.ф.: В = Vx3yVz3w(( —P(x)v—R(z,w))& (Q(y)v —R(z,w)))\ е) удаляем кванторы существования, вводя в матрицу сколемовские функции Bs= Vx Vz((^(x)v^R(z,g(x,z))&(Q(f(x))v^(z, g(x,z)))). В результате получили сколемовскую стандартную форму. Эта форма име­ ет два дизъюнкта: VxVz( —P(x)v—R(z,g(x,z)) и VxVz(Q(f(x))v —iR(z,g(x,z))). Так как каждый дизъюнкт, в частности и приведенные, имеет кванторы общности по всем переменным, содержащимся в них, то для краткости кванто­ ры общности не записывают. Тогда можно написать, что формула Bs имеет дизъюнкты: -пР (х) V -nR (z,g(x,z) и Q(f(x)) V -nR (z, g(x,z)). 71