В общем случае для построения атомов разрешается использовать следующие четыре типа символов:

(I) Индивидные символы или константы. Это обычно имена объектов такие, как Лена, Петя и 5.

(II) Символы предметных переменных. Это обычно строчные буквы х, у, z,..., возможно, с индексами.

(III) Функциональные символы. Это обычно строчные буквы f,g,h,... или осмысленные слова из строчных букв такие, как отец и плюс.

(IV) Предикатные символы. Это обычно прописные буквы Р, Q, R, ... или осмысленные слова из прописных букв такие, как БОЛЬШЕ или ЛЮБИТ.

Всякая функция или предикатный символ имеет определенное число аргументов. Если функциональный символ f имеет n аргументов, то f называется n - местным функциональным символом. Индивидный символ или константа может рассматриваться как функциональный символ без аргументов. Аналогично, если предикатный символ Р имеет n аргументов, то Р называется n- местным предикатным символом. Например, отец - одноместный  функциональный символ, а БОЛЬШЕ и ЛЮБИТ - двухместные предикатные символы.

Функция есть отображение, которое отображает список констант в данную константу. Например, отец - функция, которая отображает человека по имени Петя в человека, который есть отец Пети. Следовательно, отец(Петя) представляет человека, даже если его имя неизвестно. В логике первого порядка выражение отец(Петя) называется термом.

Термы определяются рекурсивно следующим образом:

(I) Константа есть терм.

(II) Переменная есть терм.

(III) Если f есть n- местный функциональный символ и t₁......, t_­n - термы, то f(t₁,...,t_n) - терм.

(IV) Никаких термов, кроме порожденных применением указанных выше правил, нет.

Если Р - n- местный предикатный символ и t₁,..., t_n- термы, то Р (t₁,..., t_n) - атом.

Символы " и $ называются соответственно кванторами общности и существования. Если х - переменная, то ("х) читается как «для всех х», «для каждого х» или «для вcякого х», тогда как ($х) читается «существует х», «для некоторых х» или  «по крайней мере для одного х». Вхождение переменной х в формулу называется связанным тогда и только тогда, когда оно совпадает с вхождением в кванторный комплекс ("х) или ($х) или находится в области действия такого комплекса. Вхождение переменной в формулу свободно тогда и только тогда, когда оно не является связанным. Переменная свободна в формуле, если хотя бы одно ее вхождение в эту формулу свободно. Переменная связана в формуле, если хотя бы одно ее вхождение в эту формулу связано. В формуле ("х) Р(х, у) переменная х связана, так как вхождение х связано. Однако переменная у свободна, так как единственное вхождение у свободно. Отметим, что переменная в формуле может быть свободной и связанной одновременно. Например, у и свободна и связана в формуле ("х)Р(х, у)&("y)Q(y).

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

(I) Атом есть формула.

(II) Если F и G - формулы, то (F), (FG), (F&G), (F®G), (F«G)- формулы.

(III) Если F - формула, а х - свободная переменная в F, то ("х)F и ($х)F - формулы.

(IV) Формулы порождаются только конечным числом применений правил (I), II) и (III).

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

Интерпретация формулы F логики первого порядка состоит из непустой (предметной) области D и указания «оценки» (значения) всех констант, функциональных символов и предикатных символов, встречающихся в F:

1. Каждой константе ставится в соответствие некоторый элемент из D.

2. Каждому n- местному функциональному символу ставится в соответствие отображение из Dⁿ в D. (Заметим, что Dⁿ ={(х₁,..,х_n) ç х₁ Î D,..., х_n Î D}.).

3. Каждому n- местному предикатному символу ставится в соответствие отображение Dⁿ в (И, Л).

Иногда, чтобы акцентировать внимание на области D, говорят об интерпретации формулы на D. Когда мы ищем «оценку», т. е. определяем истинностное значение формулы в интерпретации на области D, ("х) будет интерпретироваться как «для всех элементов х из D» и ($х) - как «существует элемент х из D». Для каждой интерпретации формулы на области D формула может получить истинностное значение И или Л согласно следующим правилам:

1. Если заданы значения формул G и H, то истинностные значения формул (G), (GH), (G&H), (G®H), (G«H) получаются на основе таблицы истинности⁶.

2. ("х)G получает значение И, если G получает значение И для каждого х из D; в противном случае она получает значение Л.

3. ($х)G получает значение И, если G получает значение И хотя бы для одного х из D; в противном случае она получает значение Л.

Формула G непротиворечива (выполнима) тогда и только тогда, когда существует такая интерпретация I, что G имеет значение И в I. Если формула G есть И в интерпретации I, то говорят, что I есть модель формулы G и I удовлетворяет G.

Формула G противоречива (невыполнима) тогда и только тогда, когда не существует интерпретации, которая удовлетворяет G.

Формула G общезначима тогда и только тогда, когда не существует никакой интерпретации, которая не удовлетворяет формуле G.

Формула G есть логическое следствие формул F₁,F₂,..,F_n тогда и только тогда, когда для каждой интерпретации I, если F₁&... &F_n истинна в I, то G также истинна в I.

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

В логике первого порядка имеется нормальная форма называемая предваренной нормальной формой. Эта форма применяется в логике для упрощения процедуры доказательства.

Говорят, что формула F находится в предваренной нормальной форме²⁷, когда F имеет вид: Q₁X₁...Q_nX_nM, "Q_iX_i (i=1,n). Запись Q_iX_i    означает квантификатор "Х_i или $Q_i; М- не содержит кванторов; запись до М называется префикс, а М - матрицей формулы F. Для преобразования произвольной формулы в предваренную формулу используются следующие записи правила:

G«H=(GH)&(HG);

G®H=GH;

(F)=F;

("xF(x))=$x(F(x));

($xF(x))="x(F(x));

xF(x)&xH(x)=x(F(x)&H(x));

xF(x)xH(x)= x(F(x)H(x)).

Алгоритм преобразования в предваренную форму.

1). Исключить связи эквивалентности и импликации в соответствии с таблицей 1⁵.

2). Использовать последовательно законы (F)=F, (FG)=F&G, (F&G)=FG, ("xF(x))=$x(F(x)), ($xF(x))="x(F(x)) чтобы пронести знак отрицания внутрь формулы.

3). Переименовать связанные переменные таким образом, чтобы ни какая переменная не имела бы одновременно свободных и связанных вхождений.

4). Удалить те квантификации, область действия которых не содержит вхождений квантификационных переменных.

5). Переместить все квантификации в начало формул, используя правила:

Q(x)F(x)G=Q(x)(F(x)G);

Q(x)F(x)&G=Q(x)(F(x)&G);

"xF(x)&"xH(x)="x(F(x)&H(x));

xF(x)xH(x)=x(F(x)H(x));

Q₁(x)F(x)Q₂(x)G(x)=Q₁(x)Q₂(z)(F(x)G).

Пример 6. Приведем формулу xP(x)xQ(x) к предваренной нормальной форме.

 xP(x)xQ(x)= (xP(x))xQ(x)= x(P(x))xQ(x)= x(P(x) Q(x)).

Пусть формула F находится в предваренной нормальной форме, где матрица М есть коньюнктивная нормальная форма. Положим, что Q_r есть квантор существования в префиксе. Если ни какой квантор всеобщности не стоит в префиксе левее Q_r, то выберем новую константу С отличную от других констант входящих в М. Заменим все Х_r встречающиеся в М на С и вычеркнем квантор Q_rX_r из префикса. Если Q_s1,..., Q_sm список всех кванторов всеобщности встречающиеся левее Q_r, то выберем новый m-местный функциональный символ f, отличный от других функциональных символов m, заменим X_r в М на f(x,....x) и выберем Q_r и X_r из префикса, затем весь этот процесс применим для всех кванторов существования в префиксе. Последняя из полученных формул после преобразования называется скулемовской или стандартной нормальной формой. Константы и функции применяются для замены переменных квантора существования, называются скулемовскими функциями.

Пример 7. Пусть требуется получить стандартную форму формулы

xyzuvwP(x, y, z, u, v, w).

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

yzvP(a, y, z, f(y, z), v, g(y, z, v)).

Рассмотрим применение метода резолюций для логики предикатов первого порядка.

Пусть S - множество дизъюнктов, которые представляют стандартную форму формулы F, тогда F противоречиво в том и только в том случае если S противоречиво.

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

Подстановкой²⁹ называется конечное множество вида {t₁/J₁,...,t_n/J_n}, где каждое J_i , i=1, это переменная, а каждый t_i  - терм, причём все J_i различны. Подстановка, которая не имеет элементов, называется пустой и обозначается e. Пусть Q={t₁/J₁,...,t_n/J_n} - подстановка, а Е - выражение, тогда запись ЕQ означает выражение, полученное из Е заменой одновременно всех вхождений переменной J_i на терм t_i. Это выражение называется примером Е.

Пример 8. Пусть Q={a/x, f(b)/y, c/z}, E=P(x, y, z). Тогда EQ=P(a, f(b), c)

Пусть Q={t₁/x₁, …, t_n/x_n}, ={u₁/y_{1, …,} u_m/y_m} - две подстановки. Тогда композиция Q и  (обозначается Q) есть подстановка, которая получается из множества {t₁/x₁, …, t_n/x_n, u₁/y₁, …, u_m/y_m} вычеркиванием всех элементов t_j/x_j, для которых t_j=x_j, и всех элементов u_i/y_i таких, что y_i{x_1, x₂, …, x_n}.

Пример 9. Пусть Q={t₁/x₁, t₂/x₂}={f(y)/x, z/y}, ={u₁/y_1, u₂/y₂, u₃/y₃}={a/x, b/y, y/z}.

Тогда {t₁/x₁, t₂/x₂, u₁/y₁, u₂/y₂, u₃/y₃}={f(b)/x, y/y, a/x, b/y, y/z }. Так как t₂=x₂, то t₂/x₂, т.е. y/y, должно быть вычеркнуто из множества. Кроме того, так как y₁ и y₂ содержатся среди элементов {x₁, x₂, x₃}, то u₁/y₁  и u₂/y₂ (т.е. a/x, b/y) должны быть вычеркнуты. Таким образом Q={f(b)/x, y/z}.

Подстановка Q называется унификатором для множества {E₁,...,E_k} тогда и только тогда, когда выполняется условие E₁Q=E₂Q=...=E_kQ. Говорят, что предыдущее множество унифицируемо, если для него существует унификатор. Унификатор s³⁴ для множества {E₁,...,E_k} будет наиболее общим унификатором тогда и только тогда когда для каждого унификатора s этого множества существует подстановка l так что Q=s _° l.

Алгоритм унификации³¹ заключается в выполнении следующих шагов:

1). K=0, W_k=W, s_k=e.

2). Если W_k - единственный дизъюнкт, то конец алгоритма и s_k наиболее общий унификатор для W, а он равен пустому множеству, иначе отыщем множество W_k рассогласований для D­_k.

3). Если существуют такие элементы J_k /t_k в D_k , что  J_k переменная не входящая в t_k то перейти к 4-му шагу, в противном случае окончание алгоритма и W не унифицируемо.

4). s_k+1=s_k{ t_k/J_k}; W_k+1=W_k{ t_k/J_k }

5). Присвоить k+1 и перейти к шагу 2.

Пример 10. Пусть требуется найти общий унификатор для множества

W={P(a, x, f(g(y)))), P(z, f(z), f(u))}.

Шаг 1. В соответствии с вышеизложенным будем иметь s₀=e, W₀=W. Так как W₀ не является единичным дизъюнктом, то s₀ не является наиболее общим унификатором для W.

Шаг 2. Множество рассогласований D₀={a, z}. В D₀ существует переменная v₀=z, которая не встречается в t₀=a.

Шаг 3. Пусть s₁=s₀{t₀/v₀}=e{a/z}={a/z}, W₁=W₀{t₀/v₀}={P(a, x, f(g(y))), P(z, f(z), f(u)))} {a/z}={P(a, x, f(g(y))), P(a, f(a), f(u))}.

Шаг 4. W₁ не является единичным дизъюнктом, так как имеется множество рассогласований D₁ для W₁: D₁={x, f(a)}.

Шаг 5. Из D₁ следует v₁=x, t₁=f(a).

Шаг 6. Пусть s₂=s₁{t₁/v₁}={a/z}{f(a)/x}={a/z, f(a)/x}, W₂=W₁{t₁/v₁}={P(a, x, f(g(y))), P(a, f(a), f(u))} {f(a)/x}={P(a, f(a), f(g(y))), P(a, f(a), f(u))}.

Шаг 7. W₂ не является единичным дизъюнктом, т.к. имеется множество рассогласований D₂ для W₂: D₂={g(y), u}. Из D₂  можно определить, что v₂=u, t₂=g(u).

Шаг 8. Пусть s₃=s₂{t₂/v₂}={a/z, f(a)/x}{g(y)/u}={a/z, f(a)/x, g(y)/u}, W₃=W₂{t₂/v₂}={P(a, f(a), f(g(y))), P(a, f(a), f(u))} {g(y)/u}={P(a, f(a), f(g(y))), P(a, f(a), f(g(y)))}={P(a, f(a), f(g(y)))}.

Шаг 9. Так как W₃ является единичным дизъюнктом, то s₃={a/z, f(a)/x, g(y)/u} есть наиболее общий унификатор для W.

Метод резолюции³³ для предикатов логики первого порядка определяется нижеследующими положениями.

Если две или более литер дизъюнкта С имеют наиболее общий унификатор s, то запись Сs называется склейкой С. Пусть С₁ и С₂ два дизъюнкта, называющихся дизъюнктами посылками, не имеют ни каких общих переменных. Пусть L₁ и L₂ две литеры С₁ и С₂ соответственно. Если L₁ и L₂  имеют наиболее общий унификатор s,то дизъюнкты вида (С₁s-L₁s)È(С₂s-L₂s) называются бинарной резольвентой С₁ и С₂. При этом С₁ и С₂  называются отрезаемыми литерами.

Пример 11. Пусть С₁=Р(х) È Q(x) С₂=ù Р(a) È R(x). Вследствие того, что в Х входят С₁ и С₂  , то заменим переменную С₁ и С_2, т.к. С₂= ù Р(a) È R(x) Û  ù Р(a) È R(y). Тогда L₁=P(x), L₂=ù P(a). Так как ù L₂= P(a) Þ L₁ и ù L₂  имеют общий унификатор s ={a/x} то можно записать резольвенту:

({P(a),j(a)} - {P(a)}) È ({ù Р(a),R(y)} - {ù Р(a)})={Q(a)} È {R(y)} =

= {Q(a)} È {R(y)} = {Q(a)},{R(y)} = Q(a)} È {R(y)

Рассмотрим возможные варианты формирования резольвенты:

Резольвентой посылок С₁ и С₂ является одна из следующих резольвент:

1). Бинарная резольвента С₁ и С₂.

2). Бинарная резольвента С₁ и склейки С₂.

3). Бинарная резольвента С₂ и склейки С₁.

4). Бинарная резольвента склейки С₁ и склейки С₂.