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

Глава 4. Логический вывод и анализ модифицируемых рассуждений в АК

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

А.П. Чехов, "Огни"

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

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

.1. Интерпретация логического вывода

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

Теорема 4.1. Если для логических формул A и B имеется интерпретация в виде множеств SA и SB, то общезначимость импликации A B равносильна выполнению отношения SA SB.

Доказательство. За основу возьмем таблицу истинности импликации (табл. 1.4. в подразделе 1.2). Пусть задана система из двух множеств SA и SB, а также некоторый элемент t, относительно которого можно сказать, что он принадлежит какому-то множеству, либо его дополнению. Предположим, что высказываниям "A истинно" (A = 1) или "B истинно" (B = 1) соответствуют

130

утверждения t SA и t SB. Тогда выражениям A = 0 и B = 0 можно сопоставить

утверждения t SA и t SB . Согласно табл. 1.4 импликация A B истинна для

пар утверждений: (t SA и t SB ); (t SA и t SB); (t SA и t SB) и ложна

для пары (t SA и t SB ) – последнее означает ситуацию, когда не соблюдается соотношение SA SB. Во всех остальных истинных случаях утверждения о принадлежности элемента t не противоречат соотношению SA SB. Отсюда следует справедливость теоремы. Конец доказательства.

Рассмотрим интерпретацию одного из основных правил логического вывода – modus ponens. Формулируется оно следующим образом: если истинно A и истинно A B, то B тоже истинно. Когда интерпретацией A и B являются множества SA и SB, то истинность импликации означает, что SA SB. Следовательно, если некоторое множество SA соответствует истинному утверждению, то по правилу modus ponens любое множество SB, для которого справедливо SA SB, также будет истинным утверждением.

Этот вывод кажется парадоксальным с учетом того, что в современной логике принято считать, что дедукция, в отличие от индукции, есть переход от общего к частному. Однако справедливость данного соотношения подтверждается не только интерпретацией правила modus ponens, но и другими обоснованиями, о которых будет рассказано ниже.

Для более сложных случаев в АК предусматривается возможность использования обобщенных операций и отношений, о которых шла речь в подразделе 2.2. Суть этих операций и отношений, обозначаемых как G , G , \G , G , G и т.д., заключается в следующем. Операции и отношения алгебры кортежей и алгоритмы их выполнения определены только для однотипных АК-объектов. Если у них разные схемы отношения, то перед выполнением операций и проверок АК-объекты предварительно приводят к одинаковым схемам отношений с помощью добавления фиктивных атрибутов. Установлено, что добавление фиктивных атрибутов есть семантически равносильное преобразование. Поэтому, когда речь идет о логических формулах (например, A и B) с разным составом свободных переменных, и этим формулам соответствуют АК-объекты TA и TB, то формулам A B и A B в АК сопоставляются выражения TA G TB и TA G TB.

131

Аналогично, если АК-объекты (например, P и Q) имеют разные схемы отношения, то проверка отношения P G Q означает следующую последовательность операций: сначала они приводятся к одинаковым схемам отношения за счет добавления в них недостающих фиктивных атрибутов, после чего проверяется включение с использованием стандартных алгоритмов АК, сформулированных в главе 2.

С учетом сказанного рассмотрим интерпретацию известных теорем, позволяющих свести задачи логического вывода к решению задач выполнимости. Эти теоремы сформулированы и доказаны в [Чень, 1983], а в данной книге идут под номерами 1.6 и 1.7 в подразделе 1.3. Их интерпретацию

Таким образом, в АК выводимость основана не на правилах вывода, а на проверке включения АК-объектов или проверке пустоты при пересечении определенных отношений. По сравнению с теоремами 1.6 и 1.7, в теоремах 4.2 и 4.3 добавлено условие ((F1 G ... G Fn) , которое исключает ситуацию, когда "из лжи можно вывести все, что угодно" (в терминах алгебры множеств: "пустое множество включено в любое множество"). Почему-то в исчислениях гильбертовского типа считается допустимой ситуация, когда конъюнкция посылок – тождественно ложная формула, а вывод правильный (по крайней мере, в специальной литературе этот вопрос даже не обсуждается), хотя с точки зрения естественного логического вывода она явно абсурдна.

132

4.2.Формулировки задач и алгоритмы логического вывода

4.2.1.Типы задач логического вывода

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

1)на основе правил вывода исчисления предикатов;

2)натуральный вывод [Гладкий, 2001] – система вывода с расширенным по сравнению с предыдущим набором правил;

3)вывод на основе принципа резолюции [Чень, 1983];

4)на основе специфических правил вывода, предусмотренных в конкретной системе знаний [Russel, 2003; Рассел, 2006], [Вагин, 2004]; эти правила позволяют формировать новые отношения с помощью соединения или композиции исходных отношений, в силу чего их можно назвать

семантическими правилами.

Валгебре кортежей предлагается новая система логического вывода, использующая обобщенные операции и соотношения. Предположим, что задана система аксиом A1, …, An, которые отображены в виде АК-объектов. Тогда возможно решение следующих двух типов задач.

1) Задача проверки правильности следствия. Если задано предполагаемое следствие B, то доказательство производится проверкой правильности обобщенного включения

(A1 G … G An) G B. (4.1)

2) Задача вывода произвольных следствий. Для решения этой задачи сначала вычисляется АК-объект A = A1 G … G An, после чего выбираются такие Bj, для которых соблюдается A G Bj. При этом можно не только использовать известные правила вывода. Ниже приводятся алгоритмы, позволяющие при известном A вычислить варианты Bj с учетом заданных ограничений.

Разумеется, логический анализ включает в себя не только эти задачи, но и такие, как проверка корректности гипотез, вывод абдуктивных заключений и т.д. Последние выходят за рамки логического вывода и, как правило, не рассматриваются в теоретических работах по математической логике. Решение таких задач средствами АК будет рассмотрено в подразделе 4.3.

133

4.2.2. Алгоритмы решения задачи проверки правильности следствия

Соотношение (4.1) – по сути, другая формулировка одного из соотношений теоремы 4.2. Кроме того, для его подтверждения авторами была произведена проверка всех известных в классической логике правил логического вывода. Оказалось, что (4.1) выполняется для всех правил. Исключение – формулировка правила обобщения, приводимая в некоторых монографиях по математической логике. Например, в [Мендельсон, 1984] это правило формулируется так:

"Правило обобщения (или связывания квантором всеобщности): из A

следует x1A".

Элементарная поверка показывает, что в случае, когда x1 содержится как свободная переменная в формуле A, соотношение (4.1) выполняется лишь в исключительных случаях. При внимательном прочтении текста в [Мендельсон, 1984] можно лишь предположить, что формулировка правила подразумевает случай, когда в A переменная x1 не свободна. На это указывает, в частности, приведенная на той же странице аксиома

(4): x1A(x1) A(x1).

Если допустить, что в правиле обобщения x1 есть свободная переменная в A, то правило обобщения окажется утверждением, обратным аксиоме (4), что является логической ошибкой. Однако явного указания на это обстоятельство применительно к правилу обобщения в тексте нет.

На сомнительность правила обобщения в такой формулировке обратили внимание некоторые логики. В частности, в системе натурального вывода оно применяется лишь для случая, когда в формуле A отсутствует переменная x1. Такое же требование предъявляется к операции добавления фиктивных атрибутов в АК – добавление допустимо лишь в случае их отсутствия в схеме отношения соответствующего АК-объекта.

При решении задачи проверки правильности следствия можно использовать алгоритмы выполнения операций АК и проверки правильности отношения включения [Кулик, 2008 b], подробно изложенные в главе 2, а для задач большой размерности применять методы уменьшения трудоемкости, рассмотренные в главе 3. Методы решения этой задачи рассмотрим на

134