Представление и обработка знаний

57 Если формула находится в предваренной нормальной форме и при этом из префикса удалены все кванторы существования, пе- ременные, находившиеся под действием этих кванторов, заменены в матрице символами констант или функциональными символами, а сама матрица находится в КНФ, то говорят, что она представлена в сколемовской стандартной форме. Удаление кванторов существования и замена переменных осуществляется согласно следующему правилу: 1. Если левее удаляемого квантора существования нет ни од- ного квантора всеобщности, то переменная, относящаяся к этому квантору, заменяется на символ константы, отличный от символов констант, имеющихся в матрице. 2. Если левее удаляемого квантора существования имеется n кванторов всеобщности, то переменная, относящаяся к этому кван- тору, заменяется на n -местный функциональный символ, отличный от функциональных символов, уже имеющихся в матрице, аргу- ментами которого будут переменные при кванторах всеобщности, стоящих левее удаляемого квантора существования. Например, формула (  x ) (  y ) (  z ) (  u ) P ( x , y , z , u ) в сколе- мовской стандартной форме имеет вид (  y ) (  z ) P ( a , y , z , f ( y , z )), т.е. кванторы существования удалены, а символы переменных x и u заменены на символ константы a и функциональный символ f ( y , z ). Символы констант и функциональные символы, которые исполь- зуются для замены переменных, называются сколемовскими кон- стантами и функциями. Выполним преобразование исходной формулы предыдущего примера (  x ) (  y ) (  z ) (  u ) P ( x , y , z , u ) по шагам: Шаг 1. Результат приведения: (  y ) (  z ) (  u ) P ( a , y , z , u ), Шаг 2. Результат приведения: (  y ) (  z ) P ( a , y , z , f ( y , z )). Рассмотрим еще несколько примеров такого преобразова- ния.