Сколемизация формул. Метод резолюций для ИП.

Функции A.6) называются сколемовскими (разрешающими) в
интерпретации М, если формула ) истинна в М. Очевидно,
что формулаистинна в М тогда и только тогда, когда

M|=A_s

Теорема 1.6 (Эрбран). Формула А имеет модель М тогда и
только тогда, когда для нее существуют сколемовские функции.