Владеет (ласточка, гнездо)

где является (_,_); имеет (_,_); владеет (_ _) - атомарные предикаты; «,» и «» - логические связки.

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

является (Х, птица) имеет (Х, крылья), владеет (Х, гнездо)

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

Однако предикат, который содержит переменные; например,

имеет (Х, крылья)

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

Однако иногда можно определить значения предиката не делая подстановок используя кванторы общности (") и существования ($), которые обозначают «для всех» и «существует по крайней мере одно».

Тогда приведенная выше логическая формула будет записана в виде:

("X) [являться (Х, птица) имеет (Х, крылья), владеет (Х, гнездо)]

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

Кванторы " и $ могут использоваться и для любого числа переменных. Рассмотрим их различное использование на примере двухместного предиката

любит (Х, У),

который описывает отношение «Х любит Y»:

("X) ("Y) любит (Х, Y) - все люди любят всех людей;

($Х) ("Y) любит (Х, Y) - существует человек, который любит всех;

("Х) ($Y) любит (Х, Y) - для каждого человека существует тот, который его любит;

($Х) ($Y) любит (Х, Y) - существует человек, который кого-нибудь любит.

Определение правильно построенной формулы

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

Если говорить применительно к естественному языку, то ППФ описывает обычное предложение общего вида.

Термом является либо константа, либо переменная, либо кортеж из n термов, перед которым стоит функтор.

Предикат - это кортеж из n термов, перед которым стоит предикатный символ.

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

1. Если F и G - логические формулы, то (F); F,G; FÚG; ù F; F®G; F«G - также являются логическими формулами.

2. Если F(X) - логическая формула, то оба выражения ("Х) F(X), ($X) F(X) является логическими формулами.

3. Все результаты, получаемые повторением конечного числа n1 - n6, являются логическими формулами.

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

Воспользовавшись этими определениями, можно, например, предложение «все люди смертны» записать в виде:

("X) [человек (Х) смертен]

Логический вывод

Логический вывод - это процесс получения из множества правильно построенных формул (S) некоторой ППФ (s) путем применения одного или нескольких правил вывода.

Правило резолюции для простых предложений

Наиболее простой метод логического вывода использует только одно правило вывода, называемое резолюцией, которое применяют к логическим формулам вида:

факт: А

отрицание: ù (А₁, ... , А_n)

импликация: А В₁, ... , В_m,

где А_i (i = 1, n) и B_j (j = 1, m) - произвольные предикаты.

Рассмотрим наиболее простую из форм резолюции для случая всего лишь двух S = { S₁ , S₂ } ППФ вида:

S1 (отрицание): ù А

S₂(импликация): А В ,

в которых предикат А из S₁ совпадает с предикатом А левой части S_2.

В результате одного шага вывода из S₁ и S₂ будет получена новая ППФ вида:

S: ù B

На этом шаге вывода ППФ S₁и S₂называются родительскими предложениями, а S - резольвентой, которая получается в результате применения резолюции к S₁ и S₂.

Резолюция в этом простейшем случае соответствует правилу вывода modus tollens, которое записывается в виде:

(*)

ù A AB

Ugrave; B

и соответствует следующему умозаключению:

допуская, что: НЕ А и А ЕСЛИ В,

Выводим: НЕ В

В еще более простом случае, когда S₁ - отрицание, а S₂ - факт, т.е.:

S1: ù А

S2: А

применение правила резолюции даст резольвенту - пустое отрицание

S: 

и означает противоречие. Данный шаг вывода может быть записан в виде:

(**)

ù A, A

и резолюцией является рассуждения типа

Допуская, что: НЕ А и А

Выводим противоречие.