Основные определения логики предикатов первого порядка

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

Предикат¾это логическая функция одной или нескольких переменных P(x1,x2,… xn), определенная на множестве D и принимающая одно из двух значений, «истина» и «ложь», в зависимости от значений предметных переменных. Буква P ¾ предикатный символ. Предикат, зависящий от n переменных, называется n¾местным (или n¾арным) предикатом.

Для описания некоторой предметной области на языке исчисления предикатов (ИП) определяются множества исходных элементов, правила построения формул, система аксиом и множество правил вывода, каждое из которых описывает способ построения новых формул из исходных элементов и уже построенных формул.

 Исходными элементами ИП являются следующие множества:

1) Конечное множество предметных переменных {x₁,x₂,…x_k};

2) Конечное множество предметных констант {a₁,a₂,…a_n};

3) Конечное множество функциональных символов {f₁,f₂,…f_m};

4) Конечное, непустое множество предикатных констант {p₁,p₂,…p_r};

5) Логические связки: Ø (отрицание), & (конъюнкция), Ú (дизъюнкция), Þ (импликация).

6) Кванторы: " (квантор всеобщности) и $ (квантор существования).

7) Специальные символы: ( ) + - */ < > . , [ ] : ;

8) Знак пустого дизъюнкта ð, который является тождественно ложной формулой.

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

  Определение терма ¾ рекурсивно:

1) Терм ¾ это предметная переменная или предметная константа.

2) Если f ¾ функциональный символ, и t₁,t₂,…t_n ¾ термы, то f(t₁,t₂,…t_n) ¾ терм.

Предикат вида p(t₁,t₂,…t_n), где p ¾ предикатная константа, а t₁,t₂,…t_n ¾ термы, является элементарной формулой.

Правила построения ППФ (Правильно Построенных Формул) в логике предикатов 1-го порядка следующие:

1) Всякая элементарная формула есть ППФ.

2) Если A и B¾ ППФ, а x ¾ предметная переменная, то каждое из выражений ØA, A&B, AÚB, AÞB, ("x)A, ($x)A есть ППФ.

3) Других правил построения ППФ нет.

Для формул с кванторами справедливо следующее утверждение: формула Q(x₁,x₂,…,x_n) получена из формулы P(x₁,x₂,…x_n) посредством присоединения квантора, если 

Q(x₁,x₂,…,x_n) = ("x_i) P(x₁,x₂,…x_n) или

Q(x₁,x₂,…,x_n) = ($x_i) P(x₁,x₂,…x_n).

Пусть D={a₁ , a₂, …, a_n} есть множество предметных констант, и P(x) ¾ предикат, определенный на множестве D, тогда справедливы утверждения:

("x) P(x) = P(a₁) &P(a₂) &…&P(a_n) и

($x) P(x) = P(a₁) Ú P(a₂) Ú …ÚP(a_n).

Система аксиом исчисления предикатов включает в себя аксиомы исчисления высказываний А1¾А11 и две аксиомы с кванторами А12 и А13.

A1) A Þ(BÞC)

A2) (AÞ(BÞC)) Þ((AÞB) Þ(AÞC))

A3) A&B ÞA

A4) A&B ÞB

A5) (AÞB) Þ((AÞC) Þ(AÞB&C))

A6) AÞAÚB

A7) BÞAÚB

A8) (AÞC) Þ((BÞC) Þ(AÚBÞC))

A9) (AÞB) Þ(ØBÞØA)

A10) A ÞØØA

A11) ØØAÞ A

A12) ("x) A(x) ÞA(t)

A13) A(t) Þ($x) A(x), A(x) ¾ППФ, t ¾терм, не содержащий x. Все аксиомы тождественно истинны.

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

В исчислении предикатов определены следующие правила вывода:

1) Все аксиомы выводимы.

2) Правило подстановки.

Подстановка (t_i вместо x_i) есть множество q = {x₁=t₁,x₂=t₂,… x_k=t_k }, где x₁,x₂,…,x_k ¾ попарно различные предметные переменные, x_i¹x_j при i¹j , t₁,t₂,…,t_k  ¾ термы, если x_i= t_i, то t_i отличается от x_i.Правило подстановки означает, что если P(x₁,x₂,…x_k)¾ выводим, то и формула P(t₁,t₂,…t_k) =q (P(x₁,x₂,…x_k)) ¾ выводима.

3) Правило Modus Ponens (MP).

Если А ¾ выводимая ППФ, и A ÞB¾ выводима, то B ¾ также будет выводима.

4) Правило обобщения.

Если B ÞA(x)¾ выводимая ППФ, и B не содержит вхождений x, то формула B Þ("x)A(x) ¾ также будет выводима.

5) Правило конкретизации.

Если выводима формула A(x)ÞB, и B не содержит вхождений x, то формула ($x)A(x) ÞB ¾ также будет выводима.

6) Правило переименования переменных.

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

7) Других правил вывода нет.

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

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

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

ØA₁ÚØA₂Ú…ÚØA_kÚB₁ÚB₂Ú …Ú B_n ,  где элементарные формулы (предикаты) ØA_i и B_j называются литерами, причем B_j ¾ положительная литера, а ØA_i ¾ отрицательная литера.

Если k³1 и n=1, то такая клауза имеет вид ØA₁ÚØA₂Ú…ÚØA_kÚB и называется клаузой Хорна или хорновским дизъюнктом. Хорновский дизъюнкт содержит не более одной положительной литеры.

Дизъюнкт Хорна можно преобразовать с помощью правила де Моргана:

Ø(A₁&A₂&…&A_k)ÚB, а эта формула равносильна формуле A₁&A₂&…&A_k®B, что соответствует правилам “Если …,то”.

На языке Пролог дизъюнкт Хорна записывается в другом виде B:¾ A₁,A₂,…,A_k. При такой записи «,» соответствует знаку конъюнкции &, а знак “:¾” соответствует знаку импликации .

В языке Пролог используются только хорновские дизъюнкты, называемые правилами. При этом B называется заголовком правила, а конъюнкция A₁,A₂,…,A_k называется  телом правила. Знак “:¾” читается как “Если”. Таким образом, правило является условным предложением языка Пролог.

В клаузе Хорна атомарные формулы A₁,A₂,…,A_k могут отсутствовать, т.е. k=0, n=1. В этом случае правило имеет пустое тело:

B:¾ .

Это означает, что предикат B истинен всегда, такая конструкция в языке Пролог называется фактом.

Если в хорновском предложении отсутствует заголовок правила, т.е. k³1, n=0, то правило принимает вид:

? :¾ A₁,A₂,…,A_k.

Такое выражение называется вопросом или запросом, а предикаты A₁,A₂,…,A_k называются целями, или целевыми утверждениями.

Если в хорновской клаузе k= n=0 , клауза называется пустым дизъюнктом, имеет обозначение ð и интерпретируется как тождественно ложная формула.

Предложения языка Пролог являются либо правилами, либо фактами, либо запросами. Логическая программа на Прологе ¾ это конечная последовательность фактов и правил.

Синтаксис языка программирования Пролог.