🗊Презентация Логика предикатов

§4. ЛОГИКА ПРЕДИКАТОВ

4.1 ОСНОВНЫЕ ПОНЯТИЯ ЛОГИКИ ПРЕДИКАТОВ

В алгебре логики высказывания рассматриваются как единый объект с точки зрения истинности или ложности. Структура и содержание высказываний не рассматриваются. Однако на практике для построения полноценного логического вывода важно иметь представление о структуре и содержании используемых в выводе высказываний. Поэтому логика предикатов является, по сути, расширением логики высказывания, которую включает в себя в качестве составной части.

Определение. Одноместным предикатом P(x) называется произвольная функция переменной x, определенная на множестве М и принимающая значение из множества .

Определение. Предикатом Р называется n-местная функция, определенная на производном множестве М и принимающая в качестве значений элементы из двухэлементного множества , где 0 и 1 интерпретируются как ложь и истина соответственно. Выражение вида можно трактовать так, что переменные связаны отношением Р.

Используя функциональную форму записи для предикатов, можно сказать, что предикатом Р(х1, х2, …, хn) называется функция Р:Мn→ В , где В – двоичное множество, а М – произвольное множество.

Таким образом, n-местный предикат,  это двузначная функция от n аргументов, определенная на произвольном множестве М, принимающая значение 0 или 1 (которые интерпретируются как ложь и истина соответственно). Область определения М называется предметной областью предиката, а х1, х2, …, хn – предметными переменными.

Возможность описывать с помощью предикатов не только функции, но и отношения, определяется следующим: Возможность описывать с помощью предикатов не только функции, но и отношения, определяется следующим: а) если а1, а2, …, аn – элементы множества М, то каждому n - местному отношению R соответствует предикат Р такой, что Р (а1, а2, …, аn)=1 тогда и только тогда, когда (а1, а2, …, аn)  R ; б) всякий предикат Р(х1, х2, … хn) определяет отношение R, такое, что (а1,а2…аn)R, если и только если Р(а1, а2, … аn) = 1. При этом R задает область истинности предиката Р.

Предикат можно поставить в соответствие и непрерывной функции типа F:Мn→М. Такой функции можно поставить в соответствие (n + 1) - местный предикат Р такой, что Р(а1,а2,…,аn,аn+1)=1, если и только если f(а1,а2,…,аn)=аn+1 .

Таким образом, в общем случае предикат Р – двоичная переменная, то есть переменное высказывание, истинность которого определяется значениями аргументов (х1, х2, …, хn) , а аргументы хi – чаще нелогические переменные. После подстановки вместо хi конкретных элементов множества М предикат Р(а1,а2,…,аn) перестает быть переменной и принимает одно из двух возможных значений (0 или 1).

Примеры. 1.Рассмотрим утверждение «x – целое число». Введем предикат I, обозначающий отношение «быть целым числом», тогда в виде предикатного выражения утверждение может быть записано так : I(x). 2. Рассмотрим утверждение x < y. Введем предикат S с двумя аргументами, первый из которых меньше второго, тогда S(x,y) соответствует введенному утверждению.

3. Элементы хi множества М – города. Предикат Р(х) устанавливается таким образом: «х – это столица Франции». Тогда Р(Воронеж)=0, а Р(Париж)=1. 4. Задана функция z=х+у, где х, у, z – действительные числа. Пусть предикат Р(х,у,z) соответствует этой функции. Тогда Р(2, 3, 5)=1, а Р(7, 3, 8)=0.

Если вместо переменных в предикат подставить объекты , где М – множество, на котором определено Р, то значение можно рассматривать как истинное или ложное.

Пример(для предикатов определенных в предыдущем примере). Пусть в обоих случаях предикаты определены на множестве R – действительных чисел. Тогда 1) если x = 5, то предикат I(5) = 1; если x = 7.3; то I(7.3) = 0; 2) если x = 5; y = 10.5, то S(5; 10.5) = 1; если x = 27.1; y = 4.3, то S(27.1; 4.3) = 0.

Определение. Для предиката можно выделить множество наборов таких, что , которые, будучи подставленными в предикат P, приводят его к значению истина. Объединение всех этих наборов называется множеством истинных наборов предиката Р, обозначим его Ip .

Пример. Для предиката , определенного ранее, множество Ip может быть определено следующим образом:

Определение. Предикат называется тождественно истинным, если его множество Ip образуют все возможные наборы, которые можно определить на множестве М.

Определение. Предикат называется тождественно ложным, если его множество Т.к. результат предикатного выражения это значение истина или ложь, то к ним могут быть применены логические операции

Пример. Рассмотрим предикаты I(x) и S(x,y) из предыдущих примеров. Пусть I и S определены на множестве R, тогда: 1) при x = 3, y =10 : I(3) = 1, S(3, 10) = 1, имеем I(3)&S(3, 10) = 1&1 = 1, S(3, 10)  I(3) = 1  1 = 1; 2) при x=7.5, y=11: I(7.5)=0, S(7.5,11)=1, имеем I(7.5)&S(7.5,11)=0&1=0, I(7.5)  S(7.5, 11) = 0  1 = 1;

3) задана вычислительная процедура: «Повторять цикл, пока переменные х и у не станут равными, либо прекратить вычисления после 100 повторений». Область определения: х и у – действительные числа; i – целое число, которое в каждом шаге увеличивается на единицу. Предикат Р задается условием: (x/=y)  (i<100) При этом процедура может задаваться условием: «Повторять цикл, если Р=1» .

Квантор всеобщности (). Пусть P(x) это предикат, определенный на множестве М. Тогда под выражением  понимается высказывание, которое истинно для любого элемента . Соответствующее этому высказыванию предложение можно сформулировать так: «Для любого х выражение Р(х) истинно».

Квантор существования (). Пусть Р(х) это предикат, определенный на множестве М. Тогда под выражением понимается высказывание, которое истинно, если существует элемент , для которого Р(х) истинно, и ложно в противном случае. Соответствующее ему предложение: «Существует х, при котором значение Р(х) истинно».

Пример. Пусть предикат - определен на множестве N.

Входящие в предикатное выражение переменные могут быть связанными или свободными и это зависит от того, каким образом определена область действия квантора, входящего в формулу.

Пример. Для выражения вида область действия кванторов определена следующим образом: для квантора  , для квантора  , для квантора  .

Определение. Вхождение переменной x в формулу называется связанным , тогда и только тогда, когда оно совпадает с вхождением в квантор (x) или (y) и находится в области действия квантора. Вхождение переменной в формулу свободно , тогда и только тогда, когда оно не является связанным.

Определение. Переменная свободна в формуле, если хотя бы одно ее вхождение в эту формулу свободно. Отметим, что переменная в формуле может быть свободной и связанной одновременно.

Определение. Переменная называется квантифицированной , если она используема в кванторных операциях, т.е. или .

Пример. Р(х)  х свободная;  х связанная;  х связанная, y свободная;  х и y связанные.

4.2 Логика предикатов как формальная система

Алфавит. Правила построения формул. Аксиомы. Правила вывода.

1. Алфавит. предметные переменные  x, y, z и т.п., которые принимают значение из множества М; индивидные константы  a, b, c и т.п., то есть нульместные функциональные константы или константы предметной области; функциональные константы  f, g, h и т.п., используются для обозначения функций; высказывания  p, q, r и т.п.; предикатные константы  P, R, H, Q и т.п.; символы логических операций  &, , и т.д.; символы кванторных операций  ; вспомогательные символы  ( , ).

2. Правила построения формул. Термом является всякая переменная и всякая функциональная форма. Функциональная форма  это функциональная константа, соединенная с некоторым числом термов. Если f  функциональная константа (n-местная) и - термы, то соответствующая форма записывается так Если n=0, то f превращается в индивидную константу.

Предикатная форма  это предикатная константа, соединенная с соответствующим числом термов. Если Р  предикатная константа (m-местная константа) и  термы, то соответствующая форма записывается так . Если m = 0, то пишут Р, т.е.предикатная форма превращается в высказывание

Атом  это предикатная форма или некоторое равенство (выражение вида s=t, где s и t  термы). Для равенства характерно то же, что и для предикатной формы, т.е. о нем можно сказать, что оно истинно или ложно.

Определение понятия формулы 1. Атом есть формула. 2. Если А  формула, то  формула. 3. Если А и В  формулы, то , (А&В), (А~В)  формулы. 4. Если А  формула и х  переменная, то  формулы.

3. Определение аксиом. Выбор системы аксиом в исчислении предикатов может быть осуществлен по-разному. Один из наиболее простых способов состоит в том, что берутся уже ранее определенные аксиомы из исчисления высказываний и дополняются еще двумя, связанными с использованием кванторов:

4. Правила вывода. Правила вывода также полностью заимствуются из логики высказываний, кроме того, к ним добавляются еще два правила следующего вида: - правило введения квантора существования: - правило введения квантора общности:

Примеры. 1. Утверждение: «Все слоны серые». Вводимые предикаты: слон(x) – «x – слон»; цвет(x,y) – «x цвета y». Предикатное выражение:

2. Утверждение: «Для любого множества x существует множество y такое, что мощность y больше, чем мощность x». Вводимые предикаты: множество(x) – «x – множество»; мощность(x,u) – «мощность множества x равна u»; больше(x,u) – «значение x больше значения u». Предикатное выражение:

3. Утверждение: «Все кубики, находящиеся на кубиках, которые были сдвинуты или были скреплены с кубиками, которые сдвигались, тоже будут сдвинуты». 3. Утверждение: «Все кубики, находящиеся на кубиках, которые были сдвинуты или были скреплены с кубиками, которые сдвигались, тоже будут сдвинуты». Вводимые предикаты: куб (x)– «x – куб»; сверху (x,y) – «x расположен сверху y»; скреплен (x,y) – «x скреплен с y»; сдвинут (x) – «x – сдвинут». Предикатное выражение:

4.3 Определение значения истинности предикатных формул

Определение. Две формулы логики предикатов считаются равносильными в области М, если они принимают одинаковые логические значения при всех входящих в них переменных, отнесенных к области М. Определение. Две формулы логики предикатов называются равносильными, если они равносильны на всякой области.

Пусть А(х), А(x,y) и В(х) – предикаты, р – высказывание, тогда правила имеют следующий вид:

Пример. Доказать тождественную истинность заданного предикатного выражения Пример. Доказать тождественную истинность заданного предикатного выражения

Пример. Доказать тождественную ложность заданного предикатного выражения

4.4 Метод резолюций для логики предикатов

Так как анализ выражений в формальных системах осуществляется в чисто синтаксической форме, без учета семантики, то возникает необходимость приведения отдельных выражений к единой форме. Эти приведения базируются на использовании унификации.

8888888888888888888888888888888888888888888888888888887 Например, для создания из и необходимо найти подстановку «A вместо x», которая сделает идентичными W1(A) и W1(x). Поиск подстановок термов на место переменных называется унификацией. Унификация основывается на другом понятии – подстановка.

Определение. Подстановочным частным случаем называется подстановка в некоторое выражение термов вместо переменных.

Пример. Для выражения P(x, f(y), B) имеется четыре частных случая подстановки: P(z, f(ω), B) – алфавитная, просто замена одних переменных на другие; P(x, f(A), B) – константу подставили в функцию f; P(g(z), f(A), B) – функциональное выражение вместо переменной x; P(C, f(A), B) – основной частный случай, т.к. везде подставлены константы вместо переменных.

Любую подстановку можно представить с помощью множества упорядоченных пар вида S = {t1/v1, t2/v2, …, tn/vn}, где пара ti/vi означает, что переменная vi заменяется на терм ti.

При выполнении подстановки должны соблюдаться два правила: каждое вхождение переменной заменяется на один и тот же терм; переменную нельзя заменить на терм, содержащий ту же самую переменную.

Для предыдущего примера подстановки описанные с помощью введенного формализма, имеют следующий вид: 1) S1 = {z/x, ω/y}; 2) S2 = {A/y}; 3) S3 = {g(z)/x, A/y}; 4) S4 = {C/x, A/y}.

Для обозначения подстановки часто используется следующая запись. Если S – подстановка, а E – выражение, к которому она применяется, то пишут ES . Если подстановка S применяется к каждому элементу некоторого множества {Ei}, то множество подстановочных примеров обозначается {Ei}S.

Определение. Говорят, что множество E={E1, E2 , …, En } унифицируемо, если существует такая подстановка S, что E1S = E2S = … =EnS. В этом случае подстановка S называется унификатором для множества E, т.к. после ее применения множество склеивается в один элемент.

Пример. Пусть A={P(x, f(y), B), P(x, f(B), B)}, рассмотрим подстановку S={C/x, B/y} , унифицируем и получаем A = {P(A, f(B), B)} (в подстановке C необходимости не было).

Унификация производится при следующих условиях: 1. Если термы – константы, то они унифицируемы тогда и только тогда, когда они совпадают. 2. Если в первом дизъюнкте терм – переменная, а во втором – константа, то они унифицируемы, при этом вместо переменной подставляется константа. 3. Если терм в первом дизъюнкте – переменная и во втором дизъюнкте терм тоже переменная, то они унифицируемы. 4. Если в первом дизъюнкте терм – переменная, а во втором – употребление функции, то они унифицируемы, при этом вместо переменной подставляется употребление функции. 5. Унифицируются между собой термы, стоящие на одинаковых местах в одинаковых предикатах.

Пример. Рассмотрим дизъюнкты: 1) Q(a, b, c) и Q(a, d, l). Дизъюнкты не унифицируемы. 2) Q(a, b, c) и Q(x, y, z). Дизъюнкты унифицируемы. Унификатор – S=(a/x,b/y,c/z).

Если необходимо последовательно выполнить несколько подстановок: S1, S2, то можно записать На этом действии базируется такое понятие, как композиция подстановок.

Если S и S' являются двумя множествами подстановок, то их композиция S и S' (пишется S S' ) получается после применения S' к элементам S и добавления результата к S. Композиция подстановок – это метод, с помощью которого объединяются подстановки унификации.

Определение. Композиция подстановок g и s есть функция gs, определяемая следующим образом: (gs) [t]=g[ s[t]], где t – терм, g и s – подстановки, а s[t] – терм, который получается из t путем применения к нему подстановки s.

Пример. Пусть задана последовательность подстановок {x/y,w/z}, {v/x}, {A/v, f(B)/w}, они эквивалентны одной подстановке {A/y,f(B)/z}. Последняя подстановка была выведена путем компоновки {x/y,w/z} и {v/x} для получения {v/y,w/z} и компоновки результата с {A/v, f(B)/w} для получения {A/y,f(B)/z}.

Основное требование алгоритма унификации состоит в том, что унификатор должен быть максимально общим, т.е. для любых двух выражений должен быть найден наиболее общий унификатор (НОУ).

Определение. Если s – произвольный унификатор выражения E, а g – наиболее общий унификатор этого набора выражений, то в случае применения s к E будет существовать еще один унификатор s' такой, что Es= Egs', где g и s', – композиции унификация, примененные к выражению E.

Определение. Множество рассогласований непустого множества дизъюнктов {E1,…, En} получается путем выявления первой (слева) позиции, на которой не для всех дизъюнктов из E стоит один и тот же символ, и выписывания из каждого дизъюнкта терма, который начинается с символа, занимающего данную позицию. Множество термов и есть множество рассогласований в E.

Пример. Рассмотрим дизъюнкты: {P(x, f(y, z)), P(x, a), P(x, g(h(k(x))))}. Множество рассогласований состоит из термов, которые начинаются с пятой позиции, и представляет собой множество {f(x, y), a, g(h(k(x)))}.

Алгоритм унификации Пусть E – множество дизъюнктов, D – множество рассогласований, k – номер итерации, gk – наиболее общий унификатор на k-й итерации.

Шаг 1. Пусть k=0, gk=e (пустой унификатор), Ek=E.

Шаг 2. Если для Ek не существует множества рассогласований Dk, то алгоритм завершает работу и gk – наиболее общий унификатор для E. Иначе найдем множество рассогласований Dk.

Шаг 3. Если существуют такие элементы vk и tk в Dk, что vk – переменная, не входящая в терм tk, то перейдем к шагу 4. В противном случае алгоритм завершает работу и E не унифицируемо.

Шаг 4. Пусть gk+1=gk { tk / vk}, заменим во всех дизъюнктах Ek переменную vk. на терм tk

Шаг 5. k=k+1. Перейти к шагу 2.

Пример. Рассмотрим дизъюнкты: E={P(f(a), g(x)), P(y, y)}. Итерация 1. Шаг 1. E0=E, k=0, g0=e. Шаг 2. D0={f(a),y}. Шаг 3. v0=y, t0=f(a). Шаг 4. g1={f(a)/y}, E1={P(f(a), g(x)), P(f(a), f(a))}. Переход на шаг 2.

Итерация 2. Шаг 2. D1={g(x),f(a)}. Шаг 3. Так как нет переменной в множестве рассогласований D1, то, следовательно, алгоритм унификации завершается, множество E – не унифицируемо.

Обычно унификацию используют для приведения в соответствие различных выражений. Если в одном из выражений подставлены вместо переменных константы, а другие выражения приводятся в соответствие с ним, то это называется сравнением с образом.

Как отмечалось ранее, метод резолюций применим к множеству дизъюнктов. Поэтому рассмотрим последовательность действий, которую необходимо реализовать, для приведения любой формулы логики предикатов к множеству дизъюнктов.

Пусть задано следующее предикатное выражение: Его следует привести к множеству предложений. На каждом шаге будем приводить пример, который демонстрирует результат применения действий соответствующего шага к заданному выражению.

Шаг 1. Используя правила эквивалентных преобразований, в исходном выражении все логические операции записывают через операции дизъюнкции, конъюнкции и отрицания. То есть результат будет записан как выражение, определенное в рамках следующей функционально полной системы логических функций Пример.

Шаг 2. Используя правила де Моргана, выполняют преобразования, обеспечивающие применение операции отрицания только к литералам. Пример.

Шаг 3. Разделение переменных. Так как в пределах области действия квантора можно заменить любую переменную на другую и от этого значение истинности формулы не изменится, можно преобразовать формулу так, чтобы каждый квантор имел свою собственную переменную, например вместо Пример.

Шаг 4. Исключение кванторов существования. Рассмотрим формулу В этой формуле получается, что все выражение выполняется для любого y и некоторого x, который, возможно, зависит от y. Эту зависимость можно обозначить явно с помощью некоторой функции g(y), отображающей каждое значение y в то x, которое существует. Такая функция называется сколемовской функцией.

Если заменить на эту формулу переменную x, то квантор существования можно убрать и переписать выражение в новом виде

Пример. Привести к сколемовской форме следующую формулу: можно заменить переменную x на константу a, переменную u  на двухместную f(y, z), переменную w  на трехместную функцию g(y, z, v). Таким образом, получаем следующую форму:

Шаг 5. Преобразование выражения в предваренную (префиксную) форму. Так как в формуле кванторы существования отсутствуют, то все кванторы общности можно переместить в начало формулы. Формула в таком виде называется формулой в предварительной форме, цепочка кванторов перед ней  префиксом, а следующее за ним бескванторное выражение – матрицей. Пример.

Шаг 6. Приведение матрицы выражения к форме КНФ. Известно, что любая логическая функция может быть представлена в форме КНФ. Для этого чаще всего используется метод эквивалентных преобразований. Пример. Из алгебры логики известны следующие равенства

Применим их к полученному после шага 5 выражению:

Шаг 7. Исключение кванторов общности. Так как в выражении остались кванторы общности, а их порядок несущественен, то можно эти кванторы опустить, то есть удалить у формулы префикс. Пример.

Шаг 8. Переход от выражения в виде КНФ к множеству предложений. Для этого требуется убрать все операции конъюнкции, а каждый дизъюнкт представить как отдельное предложение, т.е. перейти от выражения вида к выражению , в котором каждый элемент  предложение. Пример.

Шаг 9. Переименование переменных. Символы переменных должны быть изменены так, чтобы каждый появлялся не более чем в одном предложении. Этот процесс называется разделением переменных. Пример.

При построении вывода с помощью метода резолюций следует учитывать следующее: При построении вывода с помощью метода резолюций следует учитывать следующее: 1. Если во множестве присутствуют только предложения, содержащие предикаты без переменных, то вывод строится, как и в случае с высказываниями, т.к. логика высказываний – это частный случай логики предикатов. 2. Для того чтобы применить резолюцию к предложениям, содержащим переменные, необходимо иметь возможность найти такую подстановку, которая, будучи применена к родительским предложениям, приведет к тому, что они будут содержать дополнительные литералы.

Пример. Рассмотрим дизъюнкты: C1: P(x) Q(x), C2: Так как аргументы предиката Р в C1 и C2. различны, то невозможно построить на их основе резольвенту, но если подставить f(a) вместо x в C1 и a вместо x в C2, то исходные дизъюнкты примут вид. C1’: P(f(a)) Q(f(a)), C2’:

Следовательно, можно получить резольвенту Следовательно, можно получить резольвенту C3’: Q(f(a)) R(a). В общем случае, подставив f(x) вместо x в C1, получим C1’’: P(f(x)) Q(f(x)). Предикат P(f(x)) в C1’’ и предикат в C2 позволяют получить резольвенту C3: Q(f(x)) R(x).

Определение. Если два или более предиката (с одинаковым знаком) дизъюнкта C имеют наиболее общий унификатор g, то Cg  называется склейкой C.

Пример. Рассмотрим дизъюнкт C= P(x)  P(f(y))  В этом дизъюнкте первый и второй предикаты имеют наиболее общий унификатор g={f(y)/x}. Следовательно, Cg=P(f(y))  есть склейка C.

Определение. Пусть C1 и C2 – два дизъюнкта, которые не имеют никаких общих переменных. Пусть L1 и L2 – два предиката в C1 и C2. Если L1 и L2 имеют наиболее общий унификатор g, то дизъюнкт (C1g\L1g)  (C2g\L2g) называется резольвентой C1 и C2.

Пример. Пусть C1= P(x)  Q(x) и C2=  R(x). Так как x входит в C1 и C2, то заменим переменную в C2 и пусть C2=  R(y). Выбираем L1= P(x) и L2= L1 и L2 имеют наиболее общий унификатор g={a/x}. Следовательно, Q(a)  R(y) – резольвента C1 и C2.

Пример.

Переформулируем теперь уже известный алгоритм метода резолюций применительно к логике предикатов.

Шаг 1. Если в S есть пустой дизъюнкт, то множество S не выполнимо и алгоритм завершает работу, иначе переходим к шагу 2.

Шаг 2. Найти в исходном множестве S такие дизъюнкты или склейки дизъюнктов C1 и C2, которые содержат унифицируемые литералы L1C1 и L2C2. Если таких дизъюнктов нет, то исходное множество выполнимо и алгоритм завершает работу, иначе переходим к шагу 3.

Шаг 3. Вычислить резольвенту C1 и C2, добавить ее в множество S и перейти к шагу 1.

Пример 1. Докажем с помощью метода резолюций справедливость следующих рассуждений. Каждый член демократической партии голосует за президента и не любит коммунистов. Некоторые демократы являются предпринимателями. Следовательно, существуют предприниматели, которые не любят коммунистов

Введем следующие предикаты: C(x) – "x – член демократической партии"; W(x) – "x – голосует за президента "; R(x) - "x – не любит коммунистов "; P(x) – "x – является предпринимателем". h1 = x(C(x)W(x)&R(x)), h2 = x(C(x)&P(x)), S = x(P(x)&R(x)).

Решение:

Пример 2. Докажем с помощью метода резолюций справедливость следующих рассуждений. Некоторые руководители с уважением относятся ко всем программистам. Ни один руководитель не уважает бездельников. Следовательно, ни один программист не является бездельником.

Введем следующие предикаты: C(x) – "x – руководитель"; P(x) – "x – программист"; B(x) – "x – бездельник"; U(x,y) – "x уважает y".

Тогда посылки, записанные в виде предикатных выражений будут выглядеть так: Заключение примет следующий вид:

Преобразовав посылки и следствие, которое надо взять с отрицанием, в совокупность дизъюнктов, получим множество предложений, невыполнимость которого докажем, используя метод резолюций.

Пример 3. Докажем с помощью метода резолюций справедливость следующих рассуждений. Если родитель мужчина, то это отец. Если ребёнок мужчина, то это сын. Иван мужчина. Сидор мужчина. Иван родитель Сидора. Следовательно, Иван отец и Сидор сын

Введем следующие предикаты: C(x) – "x – сын"; О(x) – "x – отец "; R(x,y) - "x – родитель y "; M(x) – "x – мужчина". Константы: D – Иван, B – Сидор. h1 = xy(R(x, y)&M(x)O(x)), h2 = xy(R(x, y)&M(y)C(y)), h3 = M(D), h4 = M(B), h5 = R(D,B), S = O(D)&C(B)).

Решение:

Определение. Сколемовской формой предикатного выражения называется формула логики предикатов, в которой все вхождения переменных, у которых кванторы существования находятся в области действия кванторов общности, заменены на сколемовские функции.

Определение. Клаузальной формой называется такая сколемовская форма, матрица которой имеет вид КНФ. Любая сколемовская форма допускает эквивалентную ей клаузальную форму.