Определение. Формула G имеет сколемовскую нормальную форму (сокращенно: СНФ), если G=("x)…("xn)H,
где формула Н не содержит кванторов и имеет конъюнктивную нормальную форму.
Например, формула ("x)[P(x)Ú(P(y)&Q(x,y)] имеет сколемовскую нормальную форму, а формулы ("x)($y)Q(x,y), ("x)[P(x)&(P(y)ÚQ(x,y)] не имеют.В отличие от предыдущего случая предваренной нормальной формы мы здесь вначале рассмотрим алгоритм приведения к СНФ, а затем сформулируем теорему.
Алгоритм приведения к сколемовской нормальной форме
Шаг 1 – Шаг 3 – те же, что и в предыдущем алгоритме.
Шаг 4. Бескванторную часть привести к конъюнктивной нормальной форме (алгоритм описан в §5 темы 1). Шаг 5. Исключить кванторы существования. Этот шаг изложим на примере. Пусть после выполнения четвертого шага имеем формулу F=($x)("y)($z)("u)($v)H(x,y,z,u,v),
где Н – не содержит кванторов. Предположим, что формула не содержит константы с, символов одноместной функции f и двухместной функции g. Тогда в формуле Н заменим х на с, z – на f(y), v заменим на g(y,u). Все кванторы существования вычеркнем. Получим формулу
G=("y)("u)H(c,y,f(y),u,g(g,u)).
Это и есть результат выполнения шага 5. Приведем пример приведения к СНФ. Пусть
F=($x)("y)[P(x,y)®($z)(Q(x,z)&R(y))].
Применяя законы 20 и 23, получаем формулу
F1=($x)("y))($z)[ØP(x,y)Ú(Q(x,z)&R(y))].
Она имеет предваренную нормальную форму. Используя закон 12 приводим бескванторную часть к КНФ:
F2=($x)("y))($z)[ØP(x,y)Ú(Q(x,z)&(ØP(x,y)Ú(R(y))].
Сделаем подстановку x=a, z=f(y), получим искомую формулу
G=("y)[(ØP(a,y)ÚQ(a, f(y)))&(ØP(a,y))ÚR(y))].
Метод резолюции
Доказательство теорем сводится к доказательству того, что некоторая формула 
(гипотеза теоремы) является логическим следствием множества формул 
(допущений). Т.е. сама теорема может быть сформулирована следующим образом: "если истинны, то истинна и ". Такой метод доказательства теорем называется методом резолюций.
Для доказательства того, что формула G является логическим следствием множества формул , метод резолюций применяется следующим образом. Сначала составляется множество формул 
. Затем каждая из этих формул приводится к КНФ (конъюнкция дизъюнктов) и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов S. И, наконец, ищется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул . Если из S нельзя вывести #, то G не является логическим следствием формул .
Рассмотрим пример доказательства методом резолюций. Пусть у нас есть следующие утверждения:
Машина Тьюринга
1)Маши́на Тью́ринга (МТ) — абстрактный исполнитель (абстрактная вычислительная машина). Была предложена Аланом Тьюрингом в 1936 году для формализации понятия алгоритма.
Машина Тьюринга является расширением конечного автомата и, согласно тезису Чёрча — Тьюринга, способна имитировать все другие исполнители (с помощью задания правил перехода), каким-либо образом реализующие процесс пошагового вычисления, в котором каждый шаг вычисления достаточно элементарен. В состав машины Тьюринга входит бесконечная в обе стороны лента (возможны машины Тьюринга, которые имеют несколько бесконечных лент), разделённая на ячейки, и управляющее устройство, способное находиться в одном из множества состояний. Число возможных состояний управляющего устройства конечно и точно задано.
2) Операции над машинами Тьюринга
Сочетания алгоритмов [Математическая,1977,т.1] - это название, установившееся за рядом конкретных способов конструирования новых алгоритмов из нескольких заданных.
Теоремы о сочетаниях алгоритмов составляют важный раздел общей теории алгоритмов. Будучи доказанными однажды, они позволяют в дальнейшем убеждаться в осуществимости сложных и громоздких алгоритмов без фактического выписывания определяющих их схем.
Сочетания алгоритмов для машины Тьюринга описываются операциями над машинами Тьюринга.
1. Операция композиции.
Пусть M1 и M2 - машины Тьюринга, имеющие одинаковый внешний алфавит A«{a0,a1,...,ap}. Обозначим множества их состояний соответственно Q1«{q0,q1,...,qn} и Q2«{q0',q1',...,qm'}.
4) Частично рекурсивная функция определяется аналогично примитивно рекурсивной, только к двум операторам суперпозиции и примитивной рекурсии добавляется ещё третий оператор — минимизации аргумента.
- Оператор минимизации аргумента. Пусть f — функция от n натуральных переменных. Тогда результатом применения оператора минимума аргумента к функции f называется функция h от n − 1 переменной, задаваемая следующим определением:
, при условии 
То есть функция h возвращает минимальное значение последнего аргумента функции f, при котором её значение равно 0.
В терминах императивного программирования — примитивно рекурсивные функции соответствуют программным блокам, в которых используется только арифметические операции, а также условный оператор и оператор арифметического цикла (оператор цикла, в котором число итераций известно на момент начала цикла). Если же программист начинает использовать оператор цикла while, в котором число итераций заранее неизвестно и, в принципе, может быть бесконечным, то он переходит в класс частично рекурсивных функций.
Частично рекурсивные функции для некоторых значений аргумента могут быть не определены, так как оператор минимизации аргумента не всегда корректно определён, так как функция f может быть не равной нулю ни при каких значениях аргументов. С точки зрения императивного программирования, результатом частично рекурсивной функции может быть не только число, но и исключение или уход в бесконечный цикл, соответствующие неопределённому значению.