Искусственный интеллект

102 Вопросы и упражнения квантором общности, приходится, чтобы избавиться от квантора общности, вводить специальную функцию, зависящую от переменных, связанных квантором общности, вместо переменной, связанной квантором существования. Так, если имеем формулу ¦nVxaWDBj' (Р0>) v у(х, у)), то здесь литерал РОО может означать, например, наличие некоторого свойства, именуемого предикатным символом р, у объекта, именуемого переменной у, а атом у (х, у) задает отношение между объектами х, у. Объект, обозначенный переменной у, определяется в этом случае значением переменной х и может быть заменен на ранее не встречавшуюся функцию F(x), называемую обычно функцией Сколема. После такой замены квантор существования может быть удалён, а формула приобретает вид