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

Пример. Пусть имеем формулу \fx3y3z(]P(x,y)&R{x,z)v S(x^,z)). Приведем матрицу формулы к к.н.ф.:УхЭуЗг (1 (x^)vS{x,y,z))&(R(x,z) vS(x,y,z)). Затем введем функцииДл:), g(x): Vx(] P{xJ{x))v S(xJ{x),gixy)&{R{x,g{xy)v S{x/(x),g(xy)). Полученная формула является стандартной формой исходной формулы. Элементарную формулу или ее отрицание называют литералом (литерой) в логике предикатов. Дизъюнктом в логике предикатов называют дизъюнкцию лите­ ралов. Иногда литералы или дизъюнкты называют клаузами (clause - предлонсение, являющееся, частью сложного предложения). Пусть формула А приведена в предваренную нормальную фор­ му, а ее матрица представлена в к.н.ф., т.е. A={Q\X\Q2X2...Q,^^B= { Q ] X ] Q 2 X 2... Q ^ „) D i& D i&,„& D ,„, где (QiXiQjXj-.-Qr^n)-префикс фор­ мулы А, а - дизъюнкты. Положим, что стандартная форма для А равна As={Q\X]Q2X i . . .Q, ; x , ^ .&C „ i , где в префиксе опущены кванторы существования, а Q получены из Di{l<i<m) введе­ нием скояемовских функций вместо переменных кванторов существо­ вания. Отметим, что стандартная форма А^ формулы А определяется не единственным образом, ибо сколемовские функции можно вводить неоднозначно. Имеет место следующая теорема. Теорема 3.8. Формула Л является противоречием тогда и только тогда, когда ее стандартная форма А^ является противоре­ чием. Доказательство. Приведем А в предваренную нормальную форму: ^4= 61^:1 q.2x2 105