дб. Четвертое издание джозеф Джарратано Университет Хьюстон клиэрЛэйк Гари Райли People5oft, Издательский дом "Вильямс" Москва СанктПетербург Киев 2007 ббк 32. 973. 26 018 75 Д
 Скачать 3.73 Mb.
|
действительным, то А называется теоремой данной формальной логической системы, что обозначается 3.9. Логические системы символом 1-. А) А) Ау, А Например, ГА означает, что А — теорема, которая следует из множества правильно построенных формул Г. Более явно определенная схема доказательства того, что А — теорема, является таковой А,А2, Ад I- А Символ 1, который показывает, что следующая правильно построенная формула представляет собой теорему, не является символом самой системы. Вместо этого символ 0 рассматривается как метасимвол, поскольку он используется для описания самой системы. В качестве аналогии можно рассмотреть такой язык программирования, как Java. Хотя программы на этом языке можно определять с применением синтаксических конструкций, в языке Java отсутствуют синтаксические конструкции, применимые для указания на то, что некоторая программа является действительной. Любое правило вывода формальной системы точно указывает, как могут быть получены новые утверждения (теоремы) из аксиом и ранее выведенных теорем. Примером теоремы может служить уже рассматривавшийся силлогизм о Сократе, записанный в форме логики предикатов: (Чх) (Н(х) — + М(х)), Н(з) — М(в) Например, если Ар ртов следующем выражении утверждается, что p V о — теорема, а сама эта теорема представляет собой тавтологию Qp/r p В этом выражении Н — предикативная функция, которая определяет понятие человека, а М — предикативная функция, определяющая понятие смертного. Поскольку выражение М(8) можно доказать на основании аксиом, приведенных слева от этого выражения, оно представляет собой теорему, основанную на этих аксиомах. Но следует отметить, что выражение не может быть теоремой, поскольку Зевс (греческий бог) — не человек и не предусмотрен альтернативный способ показать истинность выражения M(Zeus). Если теорема представляет собой тавтологию, из этого следует, что Г — множество меры нуль, поскольку правильно построенная формула всегда истинна и не зависит от любых других аксиом или теорем. Теорема, которая является тавтологией, обозначается символом С, как в следующем примере Глава 3. Методы логического вывода Обратите внимание на то, что, вне зависимости от значений, присваиваемых переменной р, будь то Т или I", теорема р V р всегда является истинной. Интерпретацией правильно построенной формулы называется определенный вариант присваивания истинностных значений переменным формулы, а моделью называется интерпретация, в которой правильно построенная формула является истинной. Например, моделью правильно построенной формулы p V q может служить р = Т и q = Т. Правильно построенная формула называется совместимой, или выполнимой, если существует интерпретация, в которой эта формула принимает истинное значение. А правильно построенная формула, ложная во всех интерпретациях, называется несовместимой, или невыполнимой. В качестве примера несовместимой правильно построенной формулы можно указать р Л р. Правильно построенная формула является действительной, если она истинна во всех интерпретациях, а в противном случае она рассматривается как недействительная. Например, правильно построенная формула р V р является действительной, ар может служить примером недействительной правильно построенной формулы, поскольку не имеет истинного значения при р = Т и q = I". Правильно построенная формула считается доказанной, если можно показать, что она действительна. Все пропозициональные правильно построенные формулы могут быть доказаны с помощью метода, основанного на использовании истинностной таблицы, поскольку в пропозициональном исчислении каждая правильно построенная формула имеет лишь конечное количество интерпретаций. Это означает, что пропозициональное исчисление является разрешимым. С другой стороны, исчисление предикатов не является разрешимым, поскольку для него не существует общего метода доказательства для всех правильно построенных формул исчисления предикатов, подобного методу пропозиционального исчисления, основанному на истинностных таблицах. В качестве одного из примеров действительной правильно построенной формулы исчисления предикатов можно указать следующую формулу, истинную для любого предиката В (зх)в(х) - [(чх) Эта формула показывает, как можно заменить квантор существования квантором всеобщности. Поэтому данная правильно построенная формула исчисления предикатов представляет собой теорему. Между такими выражениями, как Аи В, имеется значительное различие. Первое выражение означает, что А — теорема и поэтому может быть доказана на основании аксиом с помощью правил вывода. А во втором выражение утверждается, что В — правильно построенная формула, но может быть неизвестным доказательство, с помощью которого мог бы быть продемонстрирован вывод этой формулы. Пропозициональная логика является разрешимой, а логика предикатов не является таковой. Это означает, что не существует механической. Логические системы 239 процедуры, или алгоритма поиска доказательства теоремы логики предикатов за конечное число шагов. И действительно, теоретически доказано, что разрешимой процедуры для логики предикатов не существует. Тем не менее существуют разрешимые процедуры для таких подмножеств логики предикатов, как силлогизмы и пропозициональная логика. В связи с этим логику предикатов иногда называют полуразрешимой. Следует отметить, что язык основан на логике предикатов. Появление этого языка в х годах сразу же вызвало такой всплеск энтузиазма, что японские компании объявили о своих планах создания на базе данного языка ультрасовременных компьютерных систем 5-ro поколения. Эти системы должны были обеспечивать возможность задавать входные и выходные данные с помощью естественного языка, а также действительно понимать все, что им сказано. Но к тому времени еще не был накоплен достаточный объем компьютеризированных знаний, основанных на здравом смысле, а микропроцессоры, выпускавшиеся в 1980- х годах, небыли достаточно мощными, чтобы обеспечивать распознавание речи с высокой степенью точности. В настоящее время благодаря достижениям в области разработки онтологий, основанных на здравом смысле, подобных создаваемым в проекте Open. Сус, и качественных средств распознавания речи без обучения вероятность успешного создания таких систем стала намного выше (хотя и нес использованием языка. Ниже приведен очень простой пример определения полной формальной системы. ° Алфавит. Единственный символ "1". ° Аксиома. Строка "Г' (которая по стечению обстоятельств совпадает с символом "Г. ° Правило вывода. Если какая-либо из строк $ является теоремой, то таковой является и строка Это правило может быть записано как продукционное правило Поста следующим образом $ -+ $11. Если $ = 1, то приыенение этого правила приводит к получению $11 = 111. Если $ = 111, то применение этого правила приводит к получению $11 = 11111, и, вообще говоря, 1, 111, 11111, 1111111, Показанные в этом примере строки представляют собой теоремы рассматриваемой формальной системы. Безусловно, строки, подобные 11111, непохожи на теоремы такого вида, с которыми мы привыкли сталкиваться, но они представляют собой в полном смысле слова действительные логические теоремы. Данные конкретные теоремы имеют Глава 3. Методы логического вывода также семантический смысл, поскольку представляют собой нечетные числа, выраженные в единичной системе счисления, в которой применяется единственный символ — 1. В двоичной системе счисления имеются только символы алфавита О и 1, а в единичной системе счисления — лишь единственный символ 1. В табл. 3.13 приведен небольшой ряд чисел, представленных в единичной и десятичной системах счисления. Таблица Примеры чисел в единичной и десятичной системах счисления Единичная Десятичная 11111 Следует отметить, что в рассматриваемой формальной системе невозможно представить такие строки, как 11, 1111 и т.д., поскольку этого не допускают правила вывода и аксиома данной системы. Это означает, что 11 и 1111, которые, безусловно, представляют собой строки, полученные с помощью алфавита формальной системы, не являются в этой системе теоремами или правильно построенными формулами, поскольку их невозможно доказать с использованием только имеющихся правила вывода и аксиомы. Данная формальная система допускает вывод только нечетных чисел, а нечетных чисел. Для того чтобы иметь возможность выводить четные числа, требуется дополнительно ввести аксиому "11". Не менее важным свойством формальной системы является полнота. Множество аксиом является полным, если сего помощью можно доказать или опровергнуть любую правильно построенную формулу. Термин опровергнуть означает доказать, что некоторое утверждение является ложным. В полной системе каждая логически действительная правильно построенная формула является теоремой. Но, поскольку логика предикатов неразрешима, возможность получения доказательства зависит от удачи и находчивости того, кто стремится найти такое доказательство. Безусловно, еще одна возможность состоит в том, чтобы написать компьютерную программу, которая будет предпринимать попытки вывести доказательства, и загрузить ее работой. Еще одним желательным свойством логической системы является ее непротиворечивость. Непротиворечивой называется система, в которой каждая теорема является логически действительной правильно построенной формулой. Иными словами, непротиворечивая система не позволяет вывести заключение, не являющееся логическим следствием из его посылок. Такая система не позволяет прий- 241 3.10. Резолюция тик выводу, что какое-либо недействительное доказательство является действительным. Формальные системы образуют иерархию, определяемую тем, логика какого порядка в них используется. Язык первого порядка определен таким образом, что в нем действие кванторов распространяется на объекты, представляющие собой переменные, как в примере Чх. А в языке второго порядка предусмотрены дополнительные средства, в частности, две разновидности переменных и кванторов. Кроме переменных и кванторов, значение которых зависит оттого, какое место они занимают в правильно построенной формуле, в логике второго порядка могут применяться кванторы, переменные которых пробегают по множествам функций и предикативных символов. Примером выражения логики второго порядка может служить аксиома равенства, в которой утверждается, что два объекта равны, если они имеют одинаковую структуру и все применяемые в них предикаты равны. Если P — любой предикат с одним параметром, то следующее выражение представляет собой формулировку аксиомы равенства, в которой используется квантор второго порядка, VP, с областью определения в множестве всех предикатов х = у — = (>P) K'(х) Р(у)] 3.10 Резолюция Обычно в программах искусственного интеллекта, предназначенных для доказательства теорем, кроме всего прочего, применяется очень мощное правило вывода, называемое резолюцией, которое было предложено Робинсоном (Robinson) в 1965 году. Фактически резолюция является основным правилом вывода, используемым в языке. Благодаря этому в языке PROLOG вместо различных многочисленных правил логического вывода, имеющих ограниченную область применения, таких как модус поненс, модус толленс, правило слияния (merging rule), цепное правило и т.д., используется единственное правило логического вывода общего назначения — резолюция. В результате такого использования резолюции программы автоматического доказательства теорем, такие как PROLOG, становятся практически применимыми инструментами решения задач. Таким образом, не приходится предпринимать попытки использования различных правил вывода в надежде на то, что одно из них позволит добиться успеха, поскольку достаточно воспользоваться единственным правилом резолюции. Этот подход позволяет существенно уменьшить область поиска. Для того чтобы можно было проще ознакомиться с вводным описанием резолюции, вначале рассмотрим силлогизм о Сократе, представленный на языке PROLOG, как показано ниже; в этом фрагменте кода комментарии обозначены Глава 3. Методы логического вывода знаком процента ):-тап(Х). man(socrates). : — mortal(socrates). 'io Все люди смертны 'Ъ Сократ — человек 'Ы Запрос — смертен ли Сократ? ',4 Система PROLOG отвечает "да" yes В языке используется бескванторная система обозначений. Обратите внимание на то, что в утверждении о том, что все люди смертны, подразумевается применение квантора всеобщности, V. Язык PROLOG основан на логике предикатов первого порядка. Нов этом языке предусмотрен также целый ряд расширений, позволяющих упростить программирование приложений. Эти специальные программные средства нарушают чистую логику предикатов, поэтому называются экстралогическими средствами. К ним относятся операторы ввода и вывода, оператор отсечения (который изменяет область поиска, а также операторы добавления и удаления предикатов в базе знаний (при использовании которых происходит изменение истинностных значений без каких-либо логических обоснований. Прежде чем появится возможность применить резолюцию, правильно построенную формулу необходимо преобразовать в нормальную, или стандартную форму. Нормальные формы подразделяются натри основных типа: конъюнктивная нормальная форма, форма с логическими выражениями и подмножество последней формы с хорновскими выражениями. Основное назначение любой нормальной формы состоит в том, чтобы дать возможность представлять правильно построенные формулы в стандартной форме, в которой используются только знаки операции Ли, возможно, . После этого появляется возможность применять к правильно построенным формулам в нормальной форме, в которых удалены все прочие связки и кванторы, метод резолюции. Такое преобразование в нормальную форму является необходимым, поскольку резолюция — это операция, выполняемая над парами дизьюнктов, в результате которой создаются новые дизъюнкты, а правильно построенная формула упрощается. Ниже показана правильно построенная формула в конъюнктивной нормальной форме, определенная как конъюнкция дизъюнкций, в состав которых входят литералы. (Р V P2 V ...) Л (Qy V Qg V... ) Л Л (Zy V Zg V... ) Такие термы, как Р, обязательно должны быть литералами, а это означает, что в них не должны содержаться какие-либо логические связки наподобие знаков операции импликации и двусторонней импликации или кванторов. Литералэто атомарная формула или отрицаемая атомарная формула. Например, следующая 3.10. Резолюция правильно построенная формула находится в конъюнктивной нормальной форме (А V В) Л ( В С) Термы в круглых скобках представляют собой выражения А1/ В и ВЧС Как будет показано ниже, любая правильно построенная формула логики предикатов (включающей пропозициональную логику в качестве частного случая) может быть записана с применением выражений. Полная форма с логическими выражениями позволяет представить любую формулу логики предикатов, но может оказаться, что в таком виде формула выглядит неестественно или становится неудобной для чтения человеком. В основе синтаксиса языка лежит подмножество хорновских выражений, которое позволяет значительно упростить и повысить эффективность механического доказательства теорем с помощью языка по сравнению с такими системами, в которых используется стандартная система обозначений логики предикатов или полная форма с логическими выражениями. Как было указано в главе 1, в языке PROLOG допускается использование в голове оператора только одного выражения. А утверждения в полной форме с логическими выражениями, как правило, записываются в специальной форме, называемой формой Ковальского с логическими выражениями А, А, А- В, ВАЛА Эту правильно построенную формулу можно представить в дизъюнктивной форме как дизъюнкцию литералов с использованием следующей эквивалентности uC=— -ËV× Это приводит к получению такой формулы А Л А. Ау — В 1/ ВАЛА. Ау) V (В V В. Вм) А А. Ау VВ2...ВМ Это утверждение интерпретируется как высказывание, согласно которому, если все подцели А, А, Ау являются истинными, то одно или несколько выражений из числа В, В, Вм также являются истинными. Следует отметить, что иногда в этой системе обозначений правая и левая части меняются местами и направление стрелки изменяется на противоположное. Приведенное выше выражение, записанное в стандартной системе обозначений логики предикатов, принимает такой вид Глава 3. Методы логического вывода в которой для упрощения последнего выражения применяется закон де Моргана: -(рло) = — -рч-д Как было описано в главе 1, в языке используется форма с логическими выражениями сокращенного типа, те. форма с хорновскими выражениями, в которой разрешена только одна голова А1,А2,... Ау — В Приведенное выше выражение может быть записано в синтаксисе языка PROLOG следующим образом В- А,А2,...Ау АVВ А1/В Один из способов убедиться в том, что из этих посылок действительно следует указанное заключение, может предусматривать запись этих посылок в такой форме (А В) ЛАВ) При осуществлении попытки непосредственно доказать теорему возникает проблема, связанная стем, что при осуществления дедуктивного вывода с использованием только правил вывода и аксиом системы обнаруживаются сложности Это означает, что для вывода теоремы может потребоваться очень много времени, или даже у того, кто пытается ее доказать, может вообще не хватить временных или пространственных ресурсов, чтобы выполнить эту задачу. Для доказательства истинности теоремы применяется классический метод приведения к абсурду, или доказательства от противного. При использовании этого метода предпринимается попытка доказать, что теоремой является отрицаемая правильно построенная формула. А если в результате обнаруживается противоречие, это означает, что первоначальная неотрицаемая правильно построенная формула является теоремой. По существу, целью операции резолюции является вывод нового выражения, резольвенты, из двух других выражений, называемых родительскими выражениями. Резольвента должна иметь меньше термов, чем родительские выражения. Продолжая процесс резолюции, можно в конечном итоге достичь противоречия еще один вариант может состоять в том, что процесс будет окончен из-за того, что не обнаруживается какого- либо прогресса. Простой пример применения резолюции показан в следующем доказательстве. Системы резолюции и дедукция 245 Для дальнейшего упрощения этой формулы может использоваться один из вариантов распределительного закона, который имеет следующий вид рV(qЛт) р) Л(pvт) Применяя его к посылкам, |