Как работает сколемизация отдельных пунктов EXISTS?

Question

Если у меня есть формула как:

FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y))

(FA = для всех / E = существует)

Правила сколемизации гласят:

1. если E находится вне FA, заменить на константу или
2. если E находится внутри FA, заменить на новую функцию, содержащую все переменные вне FA в качестве аргументов.

Так что мне делать в этом случае? Могу ли я просто удалить квантификатор Exists или заменить его константой?

Спасибо!

Answer 1

Сначала напишите это, используя стандартную запись:

∀x∀y(∃z(!A(x,z)∨!A(y,z))∨B(x,y))

Теперь, применяя ваше второе правило сколемизации:

∀x∀y((!A(x,f(x,y))∨!A(y,f(x,y)))∨B(x,y))

Итак, я заменил ∃z на функцию, содержащую все переменные извне.

Теперь, это все еще не в нормальной форме Сколема, потому что это не в конъюнктивной предын нормальной форме: в формулах все еще используется множество дизъюнкций (∨). Удаление их остается за вами.