Материал: Алгебра_кортежей

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

правильные цепочки символов (формулы, предложения); аксиомы – выбранная совокупность правильных предложений;

правила (логического) вывода, позволяющие выводить из аксиом теоремы и следствия.

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

Другими словами, если заданы некоторый алфавит, множество формул (синтаксических правил их составления), множества аксиом и правил вывода, то тем самым задана некоторая формальная система F [Поспелов, 1989]:

Здесь T – конечное множество символов, базовых элементов, кирпичиков, не расчленяемых на более простые. Примерами таких элементов служат буквы (графемы) или детали в детском конструкторе. Единственное требование к элементам множества T состоит в том, что для любого элемента за конечное число шагов можно узнать, принадлежит он T или нет, а также отличить одни элементы от других, отождествляя одинаковые элементы.

L – множество правил грамматики (синтаксические правила), применение которых к символам из T позволяет конструировать правильно построенные формулы. Так, из графем возникают линейно упорядоченные сочетания, называемые словами, предложениями, текстами; из деталей детского конструктора возникают более сложные образования, в которых отдельные элементы набора скреплены.

Множество Q включает выделенные синтаксически правильные формулы, принимаемые без доказательств, к которым предъявляются специфические требования – полнота, непротиворечивость, независимость и т.д. Они называются аксиомами.

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

35

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

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

В этом случае говорят, что B выводима из A1, A2, ..., An (или является следствием A1, A2, ..., An). Элементы последовательности A1, A2, ..., An

называются посылками вывода.

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

доказуемой формулой или теоремой.

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

непосредственно выводима из формул A1, A2,..., An, с помощью какого-то одного правила вывода.

Второй вариант записи A1, A2, ... , An ├ Bиспользуется, как правило, в более общем случае. Символом "├" (иногда вместо него пишут символ " ") обычно обозначается отношение выводимости. Если знак "├" находится перед формулой (например, ├ B), значит, B – выведенная теорема. Для большей точности этот знак сопровождается нижним индексом, который указывает на имя теории, в которой осуществляется вывод, например, ├L обозначает отношение выводимости в теории L.

В качестве примера формальной системы можно привести силлогистику

36

Аристотеля, подробно рассмотренную ниже. Ее элементы T – это, например, имена терминов, а также символы A, E, O, I. Синтаксические правила образуют из элементов нормальные формы представления высказываний Asp, Esp и т.п. Исходные аксиомы – законы силлогистики: закон тождества (├ Аss), закон противоречия (├ (Asр Esр)), закон исключенного третьего (├ (Isр Оsр)). Наконец, к правилам вывода относится таблица получения заключений в правильных модусах при наличии посылок для этих заключений.

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

1.Счетное множество букв: z, y, x, …; которое будем называть множество символов для обозначения переменных языка.

2.Счетное множество букв: a, b, c, …; которое будем называть множество символов для обозначения констант языка.

3.Счетное множество прописных букв P, Q, …; для обозначения предикатных символов языка.

4.Счетное множество строчных букв f, g, …; для обозначения функциональных символов.

5.Символы для обозначения логических связок ( , , , ).

6.Символы для обозначения кванторов ( , ).

7.(, ) – скобки.

Предикатные буквы P, Q, … и функциональные символы f, g, … могут быть n-местными. Грамматика языка исчисления предикатов первого порядка приведена, например, в [Колмогоров, 1982; Мендельсон, 1984; Новиков, 1973].

Пусть дана формальная система F с языком исчисления предикатов первого порядка и алгебраическая система B = <A, F, P>. Зададим отображение I, которое всякому константному символу из алфавита T системы F ставит в соответствие некоторый элемент a A из алгебраической системы B, всякому n-местному предикатному символу – n-местное отношение из P, всякому n- местному функциональному символу – n-местную операцию из F. Тогда I

называется интерпретирующим отображением, а алгебраическая система B

37

– моделью или интерпретацией формальной системы F. Аналогично может быть введено понятие интерпретации для любой формальной системы.

Формальные системы часто ассоциируются с дедуктивными системами или исчислениями [Маслов, 1986]. При этом неявно предполагается, что алгебраический подход не предназначен или, в лучшем случае, плохо приспособлен для моделирования логического вывода. Современная математическая логика построена по строгим канонам чистого исчисления и, хотя найдены соответствия между многими разделами логики и алгебраическими системами, однако сам по себе алгебраический подход в настоящее время в теоретических исследованиях по классической логике применяется крайне редко. Он используется, в основном, в прикладных исследованиях, но отнюдь не в исследованиях, которые, по мнению многих специалистов, причисляются к исследованиям фундаментальным. Такая установка, хотя и следует из тенденции развития современной логики, но, по мнению авторов, не является безусловной истиной.

При организации процедур вывода в программных системах на основе формального подхода, помимо перечисленных во Введении, возникают следующие проблемы [Поспелов, 1989]:

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

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

впамяти системы.

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

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

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

Как показано в последующих главах, при более углубленном исследовании

38

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

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

1.3.2. Силлогистика Аристотеля и алгебра множеств

До начала XIX столетия основным инструментом логического анализа была созданная еще Аристотелем силлогистика [Аристотель, 1978]. Объектом исследования силлогистики является категорический силлогизм, в котором содержится три суждения, из них два суждения являются посылками, а третье

– заключением. Каждое суждение силлогизма должно быть одним из четырех предусмотренных Аристотелем типов. К ним относятся:

A (общеутвердительное): Все S есть P;

E (общеотрицательное): Все S не есть P;

I (частноутвердительное): Некоторые S есть P;

O (частноотрицательное): Некоторые S не есть P.

Других типов суждений в категорическом силлогизме не предусмотрено. В каждом суждении утверждается определенное соотношение между субъектом (S) и предикатом (P). Деление на субъекты и предикаты в суждениях относительно – в суждениях в качестве субъектов могут использоваться термины, которые в других суждениях играют роль предикатов, и наоборот.

Если рассматривать термины S и P как множества, то каждый тип суждений можно представить как соотношения между множествами

[Колмогоров, 1982]:

A: S P или S \ P ;

39