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

Перемещение кванторов влево. После предыдущего шага, в результате которого каждый квантор использует свои связанные переменные, обозначения которых не совпадают с переменными других кванторов, все кванторы перемешаем влево. Так, например, простая формула -,avVxp(x) после перемещения квантора влево примет вид V х -, a v p (х). Сколемнзация. Сколемизацией называется специфический прием удаления кванторов существования. В простейшем случае — это замена формулы 3 у Р(у) на формулу Р(/1), где Л является константой, ранее не встречавшейся. В общем случае, когда переменная, связываемая квантором существования, встречается в каком-либо литерале вместе с переменными, связанными