Формальная система (теория) S определяется как четверка

Правило вывода - отношение вида r_i(f₁, f₂, ... f_n , g) на множестве F. При этом формула g называется непосредственно выводимой из множества формул f₁, f₂, ..., f_n по правилу r_i; формулы f₁, f₂, ..., f_n называются посылками, а g - следствием или заключением.
Для записи правил вывода часто используют представленную ниже нотацию:

• правила , применяемые к формулам, рассматриваемым как единое целое - правила продукций, продукции, продукционные правила;
• правила, которые могут применяться к любой отдельной части формулы (если эта часть сама является формулой) - правила переписывания.

Выводом формулы f_m в теории S из множества формул {f₁, f₂, ..., f_n} называется последовательность формул f_n+1, f_n+2, ..., f_m такая, что для любого i = n+1...m формула f_i либо аксиома, либо непосредственно выводима из множества {f₁, f₂, ..., f_i-1} (или его подмножества) по одному из правил множества R.

Примечание. Напоминаем, что запись вида {...} используется для перечисления элементов некоторого множества.

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

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

Пример. Простая формальная система:
Алфавит T = {a, b, #};
Формулы F = {символ или любая последовательность символов алфавита T};
Аксиомы А = {a#a} (одна единственная аксиома);
Правила вывода R = {C1#C₂ |- bC₁#C₂b} (одно единственное правило вывода), C₁ и C₂ обозначают любые последовательности символов a и b. Представленное правило вывода является правилом продукции.
Некоторые формулы теории (ппф): ###, aaa, bababbb, b#a#ab, a.
Формулы, не являющиеся ппф: abby, bob, baobab.
В данной теории формула babba#ab непосредственно выводима из формулы abba#a по единственному имеющемуся правилу вывода (но не является теоремой).
Теоремами здесь будут только следующие формулы:

Пример. Еще одна формальная система:
Алфавит T = {m, i, u};
Формулы F = {символ или любая последовательность символов алфавита T};
Аксиомы А = {mi} (одна единственная аксиома);
Правила вывода R = {

r₁: Ci |- Ciu (продукция),
r₂: mC |- mCC (продукция),
r₃: iii |- u (правило переписывания),
r₄: uu |- (пусто) (правило переписывания)
},

Задание. Для приведенной выше формальной системы доказать теорему mu.
 

Алфавит ИППП состоит из:

• предметных переменных z, y, x, ... (для их обозначения используются строчные буквы из конца латинского алфавита);
• предметных констант a, b, c, ... (для их обозначения используются строчные буквы из начала латинского алфавита);
• n-местных предикатных букв P_iⁿ, n>0, i=1,2,... (для их обозначения используются прописные буквы из середины латинского алфавита);
• m-местных функциональных букв f_i^m, m>0, i=1,2,... (для их обозначения используются строчные буквы из середины латинского алфавита);
• знаков связок: & (коньюнкция), | (дизъюнкция), ~ (отрицание), -> (импликация);
• кванторов общности A^-1 и существования E^-1;
• круглых скобок.

1. Терм:
• всякая предметная переменная и константа является термом;
• если f_i^m - функциональная буква и t₁, t₂, ..., t_m - термы, то f_i^m(t₁, t₂, ..., t_m) - также терм.
2. Формула:
• если P_iⁿ - предикатная буква и t₁, t₂, ..., t_n - термы, то P_iⁿ(t₁, t₂, ..., t_n) - элементарная формула (атом), являющаяся частным случаем правильно построенной формулы (ппф);
• если F и G - ппф, а x - предметная переменная, то ~F, (F&G), (F|G), (F->G), A^-1x(F) и E^-1x(F) - также ппф.

В формулах A^-1x(F) и E^-1x(F) принято F называть областью действия квантора, при этом переменная x в области действия квантора характеризуется как связанная, вне области действия она свободна.
Формула называется замкнутой, если она не содержит свободных переменных.

Рассматриваемое исчисление предикатов является исчислением первого порядка, поскольку в нем допустимы кванторы лишь по переменным (в исчислении второго порядка - дополнительно по предикатным и функциональным буквам).

Пример. Несколько правильно построенных формул ИППП:

• P(x) ,
• P(x)&~Q(a,y) ,
• A^-1x(E^-1y(Q(x,y))) ,
• E^-1x(P(x)|Q(x,b))->A^-1y(Q(y,b)&R(y,f(x,b),a)) .

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

A^-1xE^-1yQ(x,y) .

A1: F->(G->F)
A2: (F->G)->((F->(G->H))->(F->H))
A3: (F&G)->F
A4: (F&G)->G
A5: F->(G->(F&G))
A6: F->(F|G)
A7: G->(F|G)
A8: ~~F->F
A9: (F->G)->((F->~G)->~F)
A10: (F->H)->((G->H)->((F|G)->H))
A11: A^-1x(F(x))->F(y)
A12: F(y)->E^-1x(F(x))

Примечание. Фомулы F->G и ~F|G, а также F&G и ~(F->~G) эквивалентны, т.е. являются синонимами (подробнее об эквивалентности см. ниже).
Примечание. Для ИППП возможны и другие системы аксиом, например, существует система трех схем аксиом, содержащих только знаки отрицания и импликации.
Примечание. Аксиомы ИППП A1 ... A10 совпадают с аксиомами исчисления высказываний.

В ИППП используются следующие правила вывода.

1. Правило заключения (modus ponens)

R1: F, F->G |- G
(если F и F->G являются выводимыми формулами, то G - выводимая формула).
2. Правило обобщения (правило A^-1-введения)

R2: F->G(x) |- F->A^-1x(G(x))
, где G(x) содержит свободное вхождение переменной x, а F их не содержит.
3. Правило E^-1-введения

R3: G(x)->F |- E^-1x(G(x))->F
при тех же требованиях к G(x) и F, что и в предыдущем правиле.

R0: U(A) |- U(G)

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

Двумя полезными правилами-"метатеоремами" являются представленные ниже.

1. Правило переименования свободных переменных

R4: F(x) |- F(y)
, где F(x) содержит свободные вхождения x, ни одно из которых не находится в области действия квантора по y.
Доказательство:
а) |- F(x) (по условию)
б) F(x)->(G->F(x)) (аксиома A1, где в качестве G выбирается любая доказуемая формула, не содержащая свободных вхождений x)
в) G->F(x) (результат применения правила заключения R1 к формулам а и б)
г) G->A^-1xF(x) (правило обобщения R2 к формуле в)
д) A^-1xF(x) (правило заключения к формуле г при учете доказуемости G)
е) F(y) (правило заключения к д и аксиоме A11)
 
2. Правило переименования связанных переменных

R5': A^-1xF(x) |- A^-1yF(y)
R5": E^-1xF(x) |- E^-1yF(y)
, где F(x) содержит свободные вхождения x, ни одно из которых не находится в области действия квантора по y, и не содержит свободных вхождений y.
Доказательство для правила-"метатеоремы" R5':
а) |- A^-1xF(x) (по условию)
б) A^-1x(F(x))->F(y) (аксиома A11)
в) A^-1x(F(x))->A^-1y(F(y)) (правило обобщения к б)
г) A^-1yF(y) (правило заключения к а и в)

Интерпретация ИППП

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

1. каждой предикатной букве P_iⁿ ставит в соответствие n-местное отношение на M,
2. каждой функциональной букве f_j^m - m-местную операцию на M,
3. каждой предметной константе - элемент M.

Всякая замкнутая (т.е. не содержащая свободных переменных) ппф представляет собой высказывание об элементах, отношениях и операциях на M, которое может быть истинным или ложным. При этом атомарной формуле P_iⁿ(t₁, t₂, ..., t_n) приписывается значение истины, если термы t₁, t₂, ..., t_n соответствуют элементам из M, удовлетворяющим отношению, определяемому данной интерпретацией. Значение истинности составных формул вычисляется в соответствие с входящими в них знаками связок, интепретируемых как логические операции (& - И, | - ИЛИ, ~ - НЕ, -> - импликация).

Примечание. Логическая операция "импликация" имеет следующую таблицу истинности:
 

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

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

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

Формула называется общезначимой, если она выполняется (т.е. превращается в истинное высказывание) при любой подстановке констант, и противоречивой, если она невыполнима при любой подстановке констант.

Интерпретация ставит вопрос об адекватности

1. содержательно построенной теории предметной области, рассматриваемой как множество объектов и отношений и операций на нем, с одной стороны,
и
2. множества высказываний об этой теории, построенного как формальная система, с другой.

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

 

	теорема	нетеорема
истина	?	?
ложь	?	?

Некоторая ппф F логически следует из множества Ф ппф, если каждая подстановка констант, удовлетворяющая Ф, также удовлетворяет и F.

Пример. Формула A^-1x Q(x) логически следует из множества {A^-1x(~P(x)|Q(x)), A^-1xP(x)}.

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

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

Пример. Доказано, что правило заключения (modus ponens) ИППП является логичным правилом вывода.

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

 

	теорема	нетеорема
истина	+	-
ложь	-	+


 

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

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

A11': A^-1x(F(x)) -> F(t)
A12': F(t) -> E^-1x(F(x))

Еще одним полезным правилом-"метатеоремой" является правило специализации
R6: A^-1x(F(x)) |- F(a)
, где a - любая предметная константа.
Доказательство для правила R6:
а) |- A^-1xF(x) (по условию)
б) A^-1xF(x) -> F(t) (аксиома A11')
в) F(t) или F(a) (правило заключения к а и б, где в качестве терма t принимается предметная константа a)

Пример. Пусть необходимо построить теорию первого порядка на базе ИППП для следующей чрезвычайно упрощенной предметной области "проектирование башен".
Башня представляет собой сооружение из крыши и поддерживающего ее ствола. Крыша может быть призматической высотой 4 м или плоской высотой 1 м. Ствол башни может состоять из 1, 2 или 3 блоков одинаковой формы. Цилиндрические блоки имеют высоту 5 и 3 м, а блоки в виде параллелепипеда - 4 и 2 м.
Основной задачей, рещаемой в этой предметной области, является создание проекта башни заданной высоты.

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

1. КРЫША(призма,4)
2. КРЫША(плоск,1)
3. БЛОК(цилиндр,5)
4. БЛОК(цилиндр,3)
5. БЛОК(параллелепипед,4)
6. БЛОК(параллелепипед,2)
7. A^-1x A^-1h БЛОК(x,h) -> СТВОЛ(x,h)
8. A^-1x A^-1h₁ A^-1y A^-1h₂ БЛОК(x,h₁) & БЛОК(y,h₂) & РАВНО(x,y) & НА(y,x) -> СТВОЛ(x,f²_sum(h₁,h₂))
9. A^-1x A^-1h₁ A^-1h₂ A^-1h₃ БЛОК(x,h₁) & БЛОК(x,h₂) & БЛОК(x,h₃) -> СТВОЛ(x,f³_sum(h₁,h₂,h₃))
10. A^-1x A^-1h_стA^-1y  A^-1h_кр СТВОЛ(x,h_ст) & КРЫША(y,h_кр) & НА(y,x) -> БАШНЯ(x,y,f²_sum(h_ст,h_кр))

Полезные теоремы

R7: |- F->F
Доказательство:
а) (F->(F->F))->((F->((F->F)->F))->(F->F)) (аксиома A2, в которой вместо G подставлена (F->F), а вместо H - F);
б) F->(F->F) (аксиома A1 с подстановкой F вместо G);
в) (F->((F->F)->F))->(F->F) (правило заключения к а и б);
г) F->((F->F)->F) (аксиома A1 с подстановкой (F->F) вместо G);
д) F->F (правило заключения к в и г).

R8: F&G |- F,G
Доказательство: применение (дважды) правила заключения к аксиомам A3 и A4.

R9: F,G |- F&G
Доказательство: двукратное применение правила заключения к аксиоме A5.

R10: (F->G)&(G->H) |- F->H (свойство "транзитивности" импликации)
Доказательство:
а) F->G (по правилу R8, примененному к исходной формуле (F->G)&(G->H))
б) G->H (по правилу R8, примененному к исходной формуле (F->G)&(G->H))
в) (F->G)->((F->(G->H))->(F->H)) (аксиома A2)
г) (F->(G->H))->(F->H) (правило заключения к а и в)
д) (G->H)->(F->(G->H)) (аксиома A1 с заменой F на (G->H) и G на F)
е) F->(G->H) (правило заключения к б и д)
ж) F->H (правило заключения к е и г)

R11: если Ф,F|-G, то Ф|-F->G (теорема дедукции),
где Ф - множество формул, а F и G - формулы.
Доказательство приведено в [1, стр. 223].

R12: если Ф,F|-G и Ф,F|-~G, то Ф|-~F (правило введения отрицания)
Доказательство:
а) Ф|-F->G (теорема дедукции R11 к первой части условия);
б) Ф|-F->~G (теорема дедукции R11 ко второй части условия);
в) Ф|-(F->~G)->~F (правило заключения к а и аксиоме A11);
г) Ф|-~F (правило заключения к б и в).
Примечание. Правило R11 лежит в основе метода доказательства от противного: предполагается, что F выводима, далее показывается одновременная выводимость G и ~G, что свидетельствует о реальной выводимости ~F.

R13: F&G|-~(F->~G)
Доказательство (от противного):
а)F->~G (предположение о выводимости);
б)F (правило R8 к посылке);
в)G (правило R8 к посылке);
г)G->(F->G) (аксиома A1);
д)F->G (правило заключения к в и г);
е)(F->~G)->~F (правило заключения к д и аксиоме A9);
ж)~F (правило заключения к а и е);
з)~(F->~G) (правило R12 к б и ж с учетом предположения а).

R14: |-F->~~F
Доказательство:
а)(F&~F)->F (аксиома A3);
б)(F&~F)->~F (аксиома A4);
в)~(F&~F) (правило R12 к а и б);
г)~~(F->~(~F)) (правило R13 к в);
д)~~(F->~~F)->(F->~~F) (аксиома A8 с заменой F на F->~~F);
е)F->~~F (правило заключения к г и д).

Задание. Самостоятельно доказать следующие теоремы:
R15: ~(F->~G)|-F&G
R16: F->G|-~F|G
R17: ~F|G|-F->G
 

Эквивалентность E1: F=~~F
Доказательство:
а) ~~F->F (аксиома A8);
б) F->~~F (правило-"метатеорема" R14);
в) (~~F->F)&(F->~~F) (правило R9 к а и б).

Ниже без доказательства приведены некоторые важные эквивалентности:
E2: F->G = ~F|G
E3: ~(F->~G) = F&G
E4: ~(F&G) = ~F|~G
E5: ~(F|G) = ~F&~G
E6: A^-1F(x) = ~E^-1x~F(x)
E7: F|(G&H) = (F|G)&(F|H)

Примечание. Эквивалентности E4 и E5 называются законами де Моргана.

Очень важным для проведения доказательств является следующее правило-"метатеорема":
если |-A=B, то |-F(A)=F(B),
где F(A) - формула, в которой выделены все вхождения формулы A, а F(B) - формула, полученная из F(A) заменой всех вхождений A на формулу B.
 

Правило резолюции:
R18: (P|R)&(~P|Q)&F |- (R|Q)&F ,
где P, R, Q и F обозначают произвольные ппф.
Доказательство:
а) (P|~(~R))&(~P|Q), F (по правилу R8 и в силу эквивалентности формул F и ~~F),
б) ((~R)->P)&(P->Q), F (в силу эквивалентности F->G и ~F|G),
в) ((~R->Q), F (правило R10 к б),
г) (~(~R)|Q), F (в силу эквивалентности F->G и ~F|G),
д) (R|Q)&F (по правилу R9 и в силу эквивалентности формул F и ~~F).

Примечание. Формула-следствие правила резолюции называется резольвентой.

Использование правила резолюции ставит две проблемы:

1. приведение формулы-посылки к специальному виду "коньюнкция дизъюкций";
2. приведение положительной и отрицательной формул в дизъюнктах к абсолютно единому виду.

1. Исключение символов импликации, для чего используется ~F|G вместо F->G.
2. Ограничение области действия отрицания только атомарными ппф. Здесь используются законы (эквивалентности E4 и E5) де Моргана:
~(F&G) = ~F|~G
~(F|G) = ~F&~G
3. Разделение переменных. Переименование переменных с той целью, чтобы каждый квантор имел свою переменную.
4. Исключение кванторов существования введением т.н. сколемовских функций и констант. Например, A^-1x(E^-1y P(x,y)) заменяется на A^-1xP(x,f(x)), где f(x) - сколемовская функция.

Если исключаемый квантор существования не входит в область действия ни одного из кванторов общности, то применяется сколемовская функция без аргументов, т.е. константа. Так, E^-1x P(x) преобразуется в P(a), где a - сколемовская константа.
Важно, чтобы сколемовские функции и константы были уникальны.
5. Вынесение кванторов в начало формулы, она получает префиксную форму.
6. Исключение кванторов общности из формулы (считается "по умолчанию", что все переменные формулы находятся в области действия кванторов общности).
7. Приведение ппф в коньюнктивную нормальную форму с использованием эквивалентности E7 вида F|(G&H) = (F|G)&(F|H).
8. Исключение символов коньюнкции по правилу R8, в результате чего образуется множество предложений (дизъюнктов).

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

Пример. Пусть необходимо из утверждений "все люди смертны" и "Сократ - человек" доказать формальным путем (используя ИППП) теорему "Сократ - смертен". Тогда предметные аксиомы будут иметь следующий вид:

AA1: A^-1x(Ч(x)->C(x))
AA2: Ч(Сократ)

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

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

1. P(z,f(v),b)
2. P(g(z),f(a),b)
3. P(c,f(a),b)

Подстановки принято представлять в виде множества пар "терм/переменная":

s1={z/x, v/y};
s2={g(z)/x, a/y};
s3={c/x, a/y}.

Некоторые свойства подстановок:

(Fs1)s2 = F(s1s2)
(s1s2)s3 = s1(s2s3)
s1s2 не равно s2s1 в общем случае

Наиболее общий унификатор (ноу) g обладает тем свойством, что, если s - любой унификатор для {F_i}, то существует некоторая подстановка s' такая, что

Существует много (не рассматриваемых здесь) алгоритмов, которые можно использовать для унификации конечного множества ппф [2].

Примечание. Унификация является более общим механизмом по сравнению с механизмом сопоставления с образцом (используемым в СУБД).

Напомним, что (согласно правилу R12) ппф (множество ппф) является противоречивой, если для нее существует ппф G такая, что G и ~G одновременно выводимы из этой ппф. Резолюция для двух ппф G и ~G дает пустую резольвенту nil, что и служит признаком противоречивости исходной ппф (множества ппф).

Пример. Даны следующие утверждения.
1. Каждый, кто умеет читать, - грамотный.
2. Все дельфины неграмотны.
3. Некоторые дельфины обладают интеллектом.
Необходимо доказать следующее утверждение (теорему):
4. Некоторые из тех, кто обладает интеллектом, не умеют читать.
Представим исходные утверждения и теорему в виде формул ИППП:
A1. A^-1xЧ(x)->Г(x)
A2. A^-1xД(x)->~Гx
A3. E^-1xД(x)&И(x)
T4. E^-1xИ(x)&~Ч(x)

Найдем отрицание теоремы:
Т4₁. ~(E^-1xИ(x)&~Ч(x))
Т4₂. A^-1x~(E^-1xИ(x)&~Ч(x)) (эквивалентность E6)
Т4₃. A^-1x(~И(x)|Ч(x)) (эквивалентности E4 и E1)

Преобразуем исходные ппф во множество предложений, используя описанный ранее алгоритм.
C1. ~Ч(x)|Г(x)
C2. ~Д(y)|~Г(y)
C3'. Д(a)
C3". И(a)
C4. ~И(z)|Ч(z)

Докажем требуемую теорему методом резолюции.
а) ~И(x)|Г(x) (резолюция к C4 и C1 с подстановкой x/z в C4)
б) ~И(x)|~Д(x) (резолюция к а и C2 с подстановкой x/y в C2)
в) ~И(a) (резолюция к б и C3' с подстановкой a/x в б)
г) nil (резолюция в и C3")

Итак, при опровержении на основе резолюции отрицание целевой ппп ~W добавляется к множеству исходных ппф (аксиом) Ф={F_i}. Это расширенное множество ппф преобразуется во множество предложений. Далее систематически используется правило резолюции с целью вывода пустого предложения nil.
Существует много различных стратегий подбора пары родительских предложений для получения резольвенты (в ширину, опорного множества, предпочтения одночленам и т.п.). В рассмотренном выше примере нами была использована простейшая линейная по входу стратегия - опровержение начинается с резолюции отрицания целевой ппф и первой встретившейся подходящей ппф из множества Ф. Далее в резолюции участвуют самая последняя резольвента и первая встретившаяся подходящая ппф из множества Ф.
Примечание. Линейная по входу стратегия подбора ппф-кандидатов на резолюцию реализована в системе программирования ПРОЛОГ.
 

1. Кузнецов О.П., Адельсон-Вельский Г.М. Дискретная математика для инженера. - М: Энергоатомиздат, 1988. - 480с.
2. Нильсон Н. Принципы искусственного интеллекта.
3. Лорьер Ж-Л. Системы искусственного интеллекта. - М.: Мир, 1991. - 568с.