Традиционной логикой называют формальную систему, предложенную Аристотелем более 2500 лет назад. Аристотель стремился установить и формально записать способы, с помощью которых можно было бы установить правильность рассуждений в разумной полемике.
Множества правил, определяющих, какие умозаключения могут быть получены из множества суждений, он назвал силлогизмом. В данном случае под суждением понимается законченная мысль, которую можно выразить на естественном языке в одной из следующих четырех форм:
• все X являются Р —
• никакой Х не является
• некоторые из X являются Р —
• некоторые из Х не являются
Каждое правило силлогизма определяет переход от предпосылок к заключению, являющемуся интуитивно очевидным. Силлогизм изначально предназначен для управления разумной дискуссией на естественном языке. Как формальная теория, он чрезмерно сложен и неполон. Силлогизм можно назвать логикой классов, которая не содержит понятия дополнения класса. Например, определив класс А (допустим, субъекты, являющиеся водителями автомобилей), мы не можем построить его дополнение (т.е. установить всех лиц, которые не являются водителями).
Будучи тесно связанным с естественным языком, силлогизм иногда приводит к абсурдным результатам, в частности, не допуская логическую эквивалентность двух способов выражения одной и той же мысли. Силлогизм неполон в том смысле, что он не позволяет осуществлять логические выводы, в которых затрагиваются вопросы существования элемента некоторого класса.
Последователи Аристотеля, основываясь на силлогизме, сформулировали принципы дедуктивного вывода для высказываний, которые находятся на более высоком уровне абстракции по сравнению с суждениями.
На основе этих правил сформулировано правило «цепного заключения», весьма удобное для вывода в системе исчисления высказываний.
5. Цепное заключение: «Если истинна импликация А—>В и истинна импликация В—>С, то импликация А—>С является истинной».
Рассмотрим пример вывода с применением этих правил. Пусть заданы следующие посылки:
Используя 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) всегда будет иметь значение «истина», для чего построим сокращенную таблицу истинности.
Помимо использования тавтологий и подстановок полезным средством для вывода является эквивалентность. Необходимо уметь правильно осуществлять замену взаимно эквивалентных формул. Например, можно подставить QvP вместо PvQ, так как
Эквивалентность
Примеры тавтологий с эквивалентностями:
В приведенной таблице Т — истина, F — ложь. Значение импликации совпадает со значением второго аргумента в том случае, если первый аргумент имеет значение Т, поэтому в первых двух строках второго столбца присутствует второй аргумент — В, значение которого может быть произвольным. Конъюнкция Ал(А—>В) при истинном А также будет иметь результат, совпадающий со значением В. Последний столбец таблицы комментариев не требует, так как приведенные в нем результаты очевидны.
Попробуем установить тавтологичность этой же формулы синтаксическим методом. Для этого раскроем все скобки по распределительному закону и убедимся, что результат упрощается до формул с очевидными значениями истинности:
В процедурах логического вывода эквивалентности можно использовать двумя способами:
При этом важно понимать отличие замены от подстановки, которое состоит в следующем: если
В противовес тавтологиям в логике существуют противоречия — формулы, значением которых всегда будет «ложь» независимо от значений входящих в них атомов. Примером является выражение
Множество ППФ для некоторой предметной области называется теорией заданной области знаний, а каждая отдельная ППФ именуется аксиомой. Цель построения теории заключается в описании нужных знаний наиболее экономичным способом. Если удается построить теорию, которая адекватно описывает заданную область знаний, то все истинные факты из области интерпретации будут следствиями аксиом этой теории, другими словами, их можно будет вывести из множества ППФ. Соответственно ложные факты не будут следствиями теории, следовательно, их нельзя будет получить путем логического вывода на основании аксиом данной теории. Теорию называют полной, если все истинные факты являются следствиями этой теории. Это означает, что каждая истинная для данной теории ППФ может быть доказана на основании ее аксиом.
Про теорию говорят, что она является синтаксически последовательной (непротиворечивой), если из аксиом теории невозможно вывести противоречие. Теория, в которой можно доказать и Р, и
В качестве примера рассмотрим построение теории и ее проверку на полноту и непротиворечивость для следующего фрагмента знаний:
«Если у Вас нету дома,
Пожары ему не страшны,
И жена не уйдет к другому,
Если у Вас нет жены».
Постараемся обойтись средствами логики высказываний и начнем с формирования области интерпретации. Для этого введем обозначения:
А — «У Вас есть дом»
В — «Дом может сгореть»
С — «У Вас есть жена»
D — «Жена может уйти к другому»
На базе этих четырех высказываний построим логические формулы:
Кроме логических формул, выражающих связь фактов, любая теория содержит истинные факты, на основе которых становится возможным конкретная интерпретация ППФ. Допустим, что в нашей теории такими фактами являются
Полученная теория является полной и последовательной, поскольку каждый факт этой теории выводится из остальных аксиом, при этом не возникнет противоречия. Доказать это несложно как семантическим, так и синтаксическим способом, однако для более сложных областей знаний необходимо использовать определенные стратегии доказательства, позволяющие преодолеть хаотичность процессов логического вывода.
Кратко рассмотрим три основные стратегии доказательства:
Доказательство с введением допущения. Для доказательства импликации вида
Теорема 1.
Эта теорема утверждает, что доказуемость заключения В при допущении истинности А эквивалентна доказуемости импликации
Теорема 2.
Эта теорема выводится из предыдущей и того факта, что посылки А\, А2, …, An истинны только тогда, когда истинна их конъюнкция.
Пример: требуется доказать
Приведение к противоречию. Этот метод доказательства, предложенный К. Робинсоном в 1960-х гг., вывел исследования в области искусственного интеллекта на новый уровень. Метод обусловил появление обратных выводов и эффективных способов выявления противоречий. Суть его состоит в следующем. Например, требуется доказать
В процессе доказательства можно двигаться по пути, который начинается от А или от -i.fi. Если В выводимо из А, то, допустив истинность А, мы доказали бы В. Поэтому, сделав допущение —iB, получим противоречие. Если вывод приведет к успеху (т.е. противоречие не будет получено), это будет свидетельствовать о несовместимости либо противоречивости исходных посылок. Мы также не получим противоречия, если доказываемое предложение А—>В является ложным.
Доказательство методом резолюции. Этот метод считается более трудным для понимания, однако имеет важное преимущество перед другими: он легко формализуем. В основе метода лежит тавтология,
Теоремы 1 и 2 позволяют записать это правило в следующем виде:
что дает основания утверждать: из посылок можно вывести
Докажем эту тавтологию с помощью тождеств булевой алгебры:
Для наглядности построим сокращенную таблицу истинности, из которой можно убедиться в справедливости правила резолюции, результат которого обозначен в таблице через R.
Легко убедиться, что все значения в столбце R будут истинными и при значении A=F.
В процессе логического вывода с применением правила резолюции выполняются следующие шаги.
Операция отрицания продвигается внутрь формул с помощью законов де Моргана:
Правило резолюции содержит в левой части конъюнкцию дизъюнктов, поэтому приведение посылок, используемых для доказательства, к виду, представляющему собой конъюнкции дизъюнктов, является необходимым этапом практически любого алгоритма, реализующего логический вывод на базе метода резолюции. Метод резолюции легко программируется, это одно из важнейших его достоинств.
Предположим, нужно доказать, что если истинны соотношения
1. Приведение посылок к дизъюнктивной форме:
2. Построение отрицания выводимого заключения
3. Применение правила резолюции:
Итак, предположив ложность выводимого заключения, получаем противоречие, следовательно, выводимое заключение является истинным, т.е. RvS выводимо из исходных посылок.
Именно правило резолюции послужило базой для создания языка логического профаммирования PROLOG. По сугй дела, интерпретатор языка PROLOG самостоятельно реализует вывод, подобный вышеописанному, формируя ответ на вопрос пользователя, обращенный к базе знаний.
В логике предикатов для применения правила резолюции предстоит осуществить более сложную унификацию логических формул в целях их приведения к системе дизъюнктов. Это связано с наличием дополнительных элементов синтаксиса, в основном кванторов, переменных, предикатов и функций.
Алгоритм унификации предикатных логических формул включает следующие шаги.
После выполнения всех шагов описанного алгоритма унификации можно применять правило резолюции. Обычно при этом осуществляется отрицание выводимого заключения, и алгоритм вывода можно кратко описать следующим образом: Если задано несколько аксиом (теория Th) и предстоит сделать заключение о том, выводима ли некоторая формула Р из аксиом теории Th, строится отрицание Р и добавляется к Th, при этом получают новую теорию Тh1. После приведения
Пример: представим средствами логики предикатов следующий текст:
«Если студент умеет хорошо программировать, то он может стать специалистом в области прикладной информатики».
«Если студент хорошо сдал экзамен по информационным системам, значит, он умеет хорошо профаммировать».
Представим этот текст средствами логики предикатов первого порядка. Введем обозначения: X — переменная для обозначения студента; хорошо — константа, соответствующая уровню квалификации; Р{Х) — предикат, выражающий возможность субъекта X стать специалистом по прикладной информатике; Q(X, хорошо) — предикат, обозначающий умение субъекта А» профаммировать с оценкой хорошо; R(X, хорошо) — предикат, задающий связь студента А с экзаменационной оценкой по информационным системам.
Теперь построим множество ППФ:
Дополним полученную теорию конкретным фактом R(ива-нов, хорошо).
Выполним логический вывод с применением правила резолюции, чтобы установить, является ли формула Р(иванов) следствием вышеприведенной теории. Другими словами, можно ли вывести из этой теории факт, что студент Иванов станет специалистом в прикладной информатике, если он хорошо сдал экзамен по информационным системам.
Доказательство
1. Выполним преобразование исходных формул теории в це лях приведения к дизъюнктивной форме:
2. Добавим к имеющимся аксиомам отрицание выводимого заключения
3. Построим конъюнкцию дизъюнктов
Результат применения правила резолюции называют резольвентой. В данном случае резольвентой является
4. Построим конъюнкцию дизъюнктов с использованием ре зольвенты, полученной на шаге 3:
5. Запишем конъюнкцию полученной резольвенты с послед ним дизъюнктом теории:
Следовательно, факт Р{иванов) выводим из аксиом данной теории.
Для определения порядка применения аксиом в процессе вывода существуют следующие эвристические правила:
Если основа оригинала (карты пли плана) прозрачна, то копию можно снять при помощи стола со…
Определение координат точки. Пусть точка А (рис. 32) находится в квадрате, абсциссы и ординаты вершин…
Рельефом местности называется совокупность неровностей физической поверхности земли. В зависимости от характера рельефа местность делят…
Для обозначения на планах и картах различных предметов местности, применяются специально разработанные условные знаки. Для обличения…
В инженерной геодезии чаще всего пользуются топографическими картами. Их составляют в масштабах 1:10000, 1:25000, 1:50000…