Способы доказательства и вывода в логике

Традиционной логикой называют формальную систему, пред­ложенную Аристотелем более 2500 лет назад. Аристотель стре­мился установить и формально записать способы, с помощью ко­торых можно было бы установить правильность рассуждений в разумной полемике. Множества правил, определяющих, какие умозаключения могут быть получены из множества суждений, он назвал силлогизмом. В данном случае под суждением понимается законченная мысль, которую можно выразить на естественном языке в одной из следующих четырех форм:

• все X являются Р — ;

• никакой Х не является ;

• некоторые из X являются Р — ;

• некоторые из Х неявляются

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

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

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

1. Modus Ponendo Ponens: «Если истинна импликация А—>В и А
истинно, то В истинно».

2. Modus Tollendo Tollens: «Если истинна импликация А—>В и В
ложно, то А ложно».

3. Modus Ponendo Tollens: «Если А истинно и конъюнкция АлВ
имеет результатом ложь, то В ложно».

4. Modus Tollendo Ponens: «Если А ложно и дизъюнкция AvB
истинна, то В является истиной».

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

5. Цепное заключение: «Если истинна импликация А—>В и
истинна импликация В—>С, то импликация А—>С является ис­
тинной».

Рассмотрим пример вывода с применением этих правил. Пусть заданы следующие посылки:

1. Р—>Q I* Если растут мировые цены на топливно-энергети­
ческие ресурсы, то увеличиваются поступления в бюджет */.

2. (RvQ)—>(RvS) /* Если наблюдается рост производства или
увеличиваются поступления в бюджет, то следует увеличение
производства или укрепление рубля */.

3. (.Р—>0—>((PvQ)—>(RvQ)) I* Если растут мировые цены на
топливно-энергетические ресурсы, то увеличиваются поступле­
ния в бюджет, из чего следует, что при росте цен на сырье или при
увеличении поступлений в бюджет происходит рост производст­
ва или увеличение бюджета */.

Используя Modus Ponendo Ponens, из посылок 1 и 3 можно вы­вести следующее заключение.

4. (PvQ)—>(RvQ) /* Если растут мировые цены на топливно-
энергетические ресурсы или увеличиваются поступления в бюд­
жет, то происходит рост производства или увеличение бюджета */.

Из посылок 4 и 2 с помощью цепного заключения можно по­лучить посылку 5.

5. (PvQ)—>(RvS) I* Если растут мировые цены на топливно-энергетические ресурсы или увеличиваются поступления в бюд­жет, то происходит рост производства или укрепление рубля */.

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

Проблема доказательства в логике состоит в нахождении ис­тинностного значения заключения В, если предполагается ис­тинность исходных посылок А1, А2, ...,Ап, что записывается в ви­де: А1, А2,..., . Знак в доказательствах и выводах следу­ет читать «верно, что» или «можно вывести».

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

Семантический метод состоит в следующем. Можно перечис­лить все атомы, входящие в формулы А1, А2,..., An, В, и составить таблицу истинности для всевозможных комбинаций значений этих атомов. Затем следует осуществить просмотр полученной таблицы, чтобы проверить, во всех ли ее строках, где формулы А1, А2, ..., An имеют значения «истина», формула В также имеет значение «истина». Этот метод применим всегда, но может ока­заться слишком трудоемким.

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

Иногда значение конкретной логической формулы не зави­сит от значений входящих в них атомов. Правильно построенные логические формулы, значением которых будет «истина» при лю­бых значениях входящих в них атомов, называются тавтология­ми. Тавтологии, или теоремы логики, обладают следующим свойством: если вместо всех вхождений некоторого атома в тавтоло­гию подставить произвольную логическую формулу, то снова бу­дет получена истинная формула. Эта новая формула называется частным случаем исходной формулы, или результатом подста­новки.

Правило подстановки. Если С(А) — тавтология и вместо всех вхождений формулы А в С подставить формулу В, то С(В) — тав­тология. Для обозначения тавтологий используется символ , ко­торый читается «общезначимо» или «всегда истинно».

Докажем то, что первая приведенная тавтология (Modus Ponendo Ponens) всегда будет иметь значение «истина», для чего построим сокращенную таблицу истинности (табл. 2).

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

Эквивалентность можно заменить двусторонней им­пликацией , так как эти выражения имеют одну и ту же таблицу истинности. Отсюда можно сделать вывод, что ло­гическая эквивалентность — это импликация в обоих направле­ниях. Эквивалентность можно привести в конъюнктивную нор­мальную форму, которая имеет вид: . Если в этом выражении раскрыть скобки, получим дизъюнктивную нормаль­ную форму: . Другими словами, если Аи В экви­валентны, то они либо оба истинны, либо оба ложны.

Примеры тавтологий с эквивалентностями:

Таблица 2.

Таблица истинности для доказательства тавталогии

В приведенной таблице Т — истина, F — ложь. Значение им­пликации совпадает со значением второго аргумента в том слу­чае, если первый аргумент имеет значение Т, поэтому в первых двух строках второго столбца присутствует второй аргумент — В, значение которого может быть произвольным. Конъюнкция Ал(А—>В) при истинном А также будет иметь результат, совпада­ющий со значением В. Последний столбец таблицы комментари­ев не требует, так как приведенные в нем результаты очевидны.

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

В процедурах логического вывода эквивалентности можно использовать двумя способами:

1)расписывать в виде двух отдельных импликаций;

2)использовать при заменах.

При этом важно понимать отличие замены от подстановки, которое состоит в следующем: если , то А можно заменить на В в любом вхождении в формулу С, не меняя ее значения, причем замену не обязательно осуществлять во всех вхождениях.

В противовес тавтологиям в логике существуют противоречия - формулы, значением которых всегда будет «ложь» независимо от значений входящих в них атомов. Примером является выраже­ние при любом значении В.

Множество ППФ для некоторой предметной области называ­ется теорией заданной области знаний, а каждая отдельная ППФ именуется аксиомой. Цель построения теории заключается в описании нужных знаний наиболее экономичным способом. Ес­ли удается построить теорию, которая адекватно описывает заданную область знаний, то все истинные факты из области ин­терпретации будут следствиями аксиом этой теории, другими словами, их можно будет вывести из множества ППФ. Соответст­венно ложные факты не будут следствиями теории, следователь­но, их нельзя будет получить путем логического вывода на осно­вании аксиом данной теории. Теорию называют полной, если все истинные факты являются следствиями этой теории. Это означа­ет, что каждая истинная для данной теории ППФ может быть до­казана на основании ее аксиом.

Про теорию говорят, что она является синтаксически последо­вательной (непротиворечивой), если из аксиом теории невозмож­но вывести противоречие. Теория, в которой можно доказать и Р, и Р, непоследовательна.

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

«Если у Вас нету дома,

Пожары ему не страшны,

И жена не уйдет к другому,

Если у Вас нет жены».

Постараемся обойтись средствами логики высказываний и начнем с формирования области интерпретации. Для этого вве­дем обозначения:

А — «У Вас есть дом»

В — «Дом может сгореть»

С — «У Вас есть жена»

D — «Жена может уйти к другому»

На базе этих четырех высказываний построим логические формулы:

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

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

Кратко рассмотрим три основные стратегии доказательства:

• доказательство с введением допущения;

• доказательство методом «от противного» (приведение к про­
тиворечию);

• доказательство методом резолюции.

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

Теорема 1. тогда и только тогда, когда

Эта теорема утверждает, что доказуемость заключения В при допущении истинности А эквивалентна доказуемости имплика­ции без дополнительных допущений. Справедливость дан­ной теоремы следует из приведенной ранее таблицы истинности {см. табл. 3).

Теорема 2. тогда и только тогда, когда

Эта теорема выводится из предыдущей и того факта, что по­сылки А\, А2, ..., An истинны только тогда, когда истинна их конъюнкция.

Пример: требуется доказать . В соответст-

вии стеоремой 2 получим . Применив эквива-

лентность вида , имеем

в силу теоремы 2 .

Приведение к противоречию. Этот метод доказательства, пред­ложенный К. Робинсоном в 1960-х гг., вывел исследования в об­ласти искусственного интеллекта на новый уровень. Метод обус­ловил появление обратных выводов и эффективных способов вы­явления противоречий. Суть его состоит в следующем. Напри­мер, требуется доказать . Вместо этого можно попытаться доказать , используя эквивалентность. Такое доказательство можно провести двояко, а именно: или допустить А и доказать затем В (это будет прямой вывод), или сделать допущение о том, что В— ложно, после чего сделать попытку опровергнуть по­сылку Л (обратный вывод).

Таблица 3.

Доказательства правила резолюции

Приведение к противоречию — ком­бинация прямого и обратного вывода, т.е. для доказательства А—>В можно одновременно допустить А и —,В (посылка истинна, а заключение — ложно):

В процессе доказательства можно двигаться по пути, который начинается от А или от -i.fi. Если В выводимо из А, то, допустив истинность А, мы доказали бы В. Поэтому, сделав допущение —iB, получим противоречие. Если вывод приведет к успеху (т.е. проти­воречие не будет получено), это будет свидетельствовать о несов­местимости либо противоречивости исходных посылок. Мы так­же не получим противоречия, если доказываемое предложение А—>В является ложным.

Доказательство методом резолюции. Этот метод считается бо­лее трудным для понимания, однако имеет важное преимущест­во перед другими: он легко формализуем. В основе метода лежит тавтология, получившая название «правило резолюции»:

Теоремы 1 и 2 позволяют записать это правило в следующем виде:

что дает основания утверждать: из посылокмож-

но вывести

Докажем эту тавтологию с помощью тождеств булевой ал­гебры:

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

Легко убедиться, что все значения в столбце R будут истинны­ми и при значении A=F.

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

2. Операция отрицания продвигается внутрь формул с помо­
щью законов де Моргана:

3. Логические формулы приводятся к дизъюнктивной форме:

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

Предположим, нужно доказать, что если истинны соотноше­ния _ , то можно вывести формулу RvS. Для этого нужно выполнить следующие шаги.

1. Приведение посылок к дизъюнктивной форме:

2. Построение отрицания выводимого заключения

Полученная конъюнкция справедлива, когда одновременно истинны.

3. Применение правила резолюции:

Итак, предположив ложность выводимого заключения, полу­чаем противоречие, следовательно, выводимое заключение явля­ется истинным, т.е. RvS выводимо из исходных посылок.

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

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

Алгоритм унификации предикатных логических формул включает следующие шаги.

1. Исключение операций эквивалентности.

2. Исключение операций импликации.

3. Внесение операций отрицания внутрь формул.

4. Исключение кванторов существования.

Это может произойти на шаге 3 вследствие применения законов де Моргана, а именно: в результате отрицания 3 меняется на V, но при этом может произойти и обратная замена. Тогда для исключения 3 поступают следующим образом: все вхождения некоторой переменной, связанной квантором существования, например (ЗА), заменяются в формуле на новую константу, например а. Эта константа представляет собой некоторое (неизвестное) значение переменной X, для которого утверждение, записанное данной формулой, истинно. При этом важно то, что на все места, где присутствует А", будет подставлено одно и то же значение а, пусть оно и является неизвестным в данный момент. Такие константы называются сколемовскими, а операция — сколемизацией (по имени известного математика Сколема).

5. Кванторы общности выносятся на первые места в формулах. Это также не всегда является простой операцией, иногда при
этом приходится делать переименование переменных.

6. Раскрытие конъюнкций, попавших внутрь дизъюнкций.

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

Если задано несколько аксиом (теория Th) и предстоит сделать заключение о том, выводима ли некоторая формула Р из аксиом теории Th, строится отрицание Р и добавляется к Th, при этом получают но­вую теорию Тh1. После приведения и аксиом теории к систе­ме дизъюнктов можно построить конъюнкцию и аксиом тео­рии Th. При этом существует возможность выводить из исходных дизъюнктов дизъюнкты-следствия. Если Р выводимо из аксиом теории Th, то в процессе вывода можно получить некоторый дизъюнкт Q, состоящий из одной литеры, и противоположный ему дизъюнкт . Это противоречие свидетельствует о том, что Р выводимо из аксиом Th. Вообще говоря, существует множество стратегий доказательства, нами рассмотрена лишь одна из воз­можных - нисходящая.

Пример: представим средствами логики предикатов следую­щий текст:

«Если студент умеет хорошо программировать, то он может стать специалистом в области прикладной информатики».

«Если студент хорошо сдал экзамен по информационным си­стемам, значит, он умеет хорошо профаммировать».

Представим этот текст средствами логики предикатов перво­го порядка. Введем обозначения: X — переменная для обозначе­ния студента; хорошо — константа, соответствующая уровню квалификации; Р{Х) — предикат, выражающий возможность субъекта X стать специалистом по прикладной информатике; Q(X, хорошо) — предикат, обозначающий умение субъекта А" про­фаммировать с оценкой хорошо; R(X, хорошо) — предикат, задаю­щий связь студента А с экзаменационной оценкой по информа­ционным системам.

Теперь построим множество ППФ:

Дополним полученную теорию конкретным фактом R(ива-нов, хорошо).

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

Доказательство

1. Выполним преобразование исходных формул теории в це­
лях приведения к дизъюнктивной форме:

2. Добавим к имеющимся аксиомам отрицание выводимого
заключения

3. Построим конъюнкцию дизъюнктов

Результат применения правила резолюции называют резольвен­той. В данном случае резольвентой является

4. Построим конъюнкцию дизъюнктов с использованием ре­
зольвенты, полученной на шаге 3:

5. Запишем конъюнкцию полученной резольвенты с послед­
ним дизъюнктом теории:

Следовательно, факт Р{иванов) выводим из аксиом данной теории.

Для определения порядка применения аксиом в процессе вы­вода существуют следующие эвристические правила:

1. На первом шаге вывода используется отрицание выводимо­
го заключения.

2. В каждом последующем шаге вывода участвует резольвен­
та, полученная на предыдущем шаге.