|
дб. Четвертое издание джозеф Джарратано Университет Хьюстон клиэрЛэйк Гари Райли People5oft, Издательский дом "Вильямс" Москва СанктПетербург Киев 2007 ббк 32. 973. 26 018 75 Д
Согласно методу опровержения, первоначальное заключение это теорема, поскольку отрицание этого заключения ведет к противоречию ° 13. Резолюция и логика предикатов первого порядка Определим такие предикаты В таком случае посылки и отрицаемое заключение можно записать, как показано ниже, где к заключению была применена операция отрицания в целях подготовки его к применению в методе резолюции.
Преобразование в форму с логическими выражениями Девять описанных ниже шагов представляют собой алгоритм преобразования правильно построенных формул логики предикатов первого порядка в форму с логическими выражениями. Эта процедура иллюстрируется на примере приведенной выше правильно построенной формулы (1). Устранить знаки условной операции, -, с помощью следующей эквивалентности pq— : -pVq (3x) [Р(х) Л (V>)(F(>) V Н(х, уз) Р(х) = х — программист Г(х) = х — нарушение в работе S(x) х — успех Н(х, ух ненавидит у (Зх) [Р(х) Л (Чу)(Г(у) — Н(х,
у))] (Чх) [Р(х) — (Чу) (Я(у) - Н(х, у (М(
(у) -
(уИ В результате
выполнения этого этапа правильно построенная формула (принимает такой вид 2. По возможности устранить знаки операции отрицания или свести область определения операции отрицания до одного атома, используя при этом такие эквивалентности, показанные в приложении А, как -(рЛо) =-рЧ-д
(3x) P(x) = (Vx) Р(х) (b'х)Р(х) = (3x) Р(х) 3. Стандартизировать переменные, применяемые в правильно построенных формулах, таким образом, чтобы связанные или фиктивные переменные
Глава 3. Методы логического вывода 256 каждого квантора имели уникальные имена. Обратите внимание на то, что имена переменных в кванторах являются фиктивными. Это означает,
что имеет место формула (Ух)Р(х) = — (Чу)Р(у) = (Ч)РЯ
поэтому стандартизированная форма выражения (Зт) - Р(х) /
(Ух)Р(х) принимает следующий вид (3x) Р(х) V (Чу)Р(у) (3x) Эта правильно построенная формула может быть заменена следующей Л(а) В данном выражении а — константа, такая как 1, в результате применения которой выражение принимает истинное значение. Такая константа а называется сколемовской константой и представляет собой частный случай сколемовской функции. В том случаев котором перед квантором существования находится квантор всеобщности,
например, как в следующем выражении, где предикат L(x, принимает истинное значение, если целое число х меньше целого числах, р) Эта правильно построенная формула означает, что для каждого целого числах можно найти целое число у, которое больше по сравнению с х. Обратите внимание на то, что в этой формуле не указано, как вычислить у,
если дано значение х. Предположим, что существует функция, которая вырабатывает число у, большее чем х. Поэтому приведенная выше правильно построенная формула становится сколемизированной таким образом (Vx)L(x, f (x)) 4. Устранить кванторы существования, 3, с использованием сколемовских функций, названных в честь норвежского логика Торалфа
Сколема (Thoralf Skolem). Рассмотрим следующую правильно построенную формулу, в которой выражение L(x) определено как предикат, принимающий истинное значение, если x ( О. Резолюция и логика предикатов первого порядка 257 Сколемовская функция от переменной квантора существования, заданной в области определения квантора всеобщности, представляет собой функцию от всех переменных кванторов, находящихся в левой части выражения. Например, следующая формула (Эи) (Vv) (Vw) (Эх) (Чу) (3z) Р(и, v, ю, х, у, z) сколемизируется, как показано ниже, где а — та же константа, а вторая сколемовская функция, д, должна отличаться от первой функции, f. (Чи)(Vm)(Чу)P(a, v, и, f(v, и, y, g(v, ю, y)) Таким образом, правильно построенная формула, применяемая в качестве примера, принимает следующий вид Р(а) Л (Чу)( Е(у) На) (Vy) [Р(а) Л F(y) V На, у 6. Преобразовать матрицу в конъюнктивную нормальную форму, представляющую собой конъюнкцию из выражений, в которой каждое выражение является дизъюнкцией. Рассматриваемый пример уже находится в коньюнктивной нормальной форме, в которой одним выражением служит Р(а), а другим — ( Г(у) V На, у. В случае необходимости можно использовать следующее распределительное правило для преобразования матрицы в конъюнктивную нормальную форму p V (q Л r) = (p V q) Л (p V r) 5. Преобразовать правильно построенную формулу в предваренную форму, представляющую собой последовательность кванторов Q, за которой следует матрица М. Вообще говоря, в качестве кванторов могут применяться либо Ч, либо 3. Нов данном случае на этапе 4 уже должны были быть устранены все кванторы существования, поэтому в последовательности Q могут присутствовать только кванторы К Кроме того, в каждом кванторе Ч имеется его собственная фиктивная переменная. Таким образом, все кванторы Ч могут быть передвинуты в левую часть правильно построенной формулы, и поэтому областью определения каждого квантора Ч может стать вся правильно построенная формула. Рассматриваемый пример принимает следующий вид, где в качестве матрицы используется терм в круглых скобках Глава 3. Методы логического вывода 7. Удалить как ненужные кванторы всеобщности, поскольку все переменные в правильно построенной формуле на этом этапе уже должны быть связанными. Теперь правильно построенная формула имеет вид матрицы. В данном примере правильно построенная формула становится таковой Р(а) Л ( F(y) \/ Нар. Удалить знаки операции Л, записав правильно построенную формулу как множество выражений. В данном примере формула имеет видР(а), Р(р) V Нар) и должна быть записана без фигурных скобок как следующий ряд выражений Р(а) -F(y) V Нар. В случае необходимости переименовать переменные в выражениях для того, чтобы одно и тоже имя переменной использовалось только водном выражении. Например, если в нашем распоряжении имеются такие выражения то их можно было бы переименовать следующим образом После проведения этой процедуры для преобразования в форму с логическими выражениями второй посылки и отрицаемого заключения, рассматриваемых в данном примере, в конечном итоге будут получены выражения, номера которых соответствуют номерам исходных посылок и отрицаемого заключения (la) (16) (а) (За) (3b) Р(х) Л Q(x) V L(x, y) -P(x) V Q(y) -Q(z) V L(z, р) Р(хl) Л Q(xl) V L(xl, р) Р(х2) V Q(y2) -Q(z) V L(z,y3) Р(а) -F(y) V Нар Н(х, р) F(b) S(b) 259 3.13. Резолюция и логика предикатов первого порядка Таким образом, посылка (1) и заключение (3) преобразуются соответственно в два выражения с суффиксами, (аи (За, а посылка (2) — водно выражение, (а. Унификация и правила После преобразования правильно построенных формул в форму с логическими выражениями обычно возникает необходимость найти подходящие подстановочные экземпляры для переменных. Дело в том, что, например, следующие два выражения нельзя привести по методу резолюции к предикату до тех пор, пока параметры F в обоих выражениях не будут совпадать -F(y) v Нар) к(ь) IF датчик 1 показывает наличие дыма THEN включить пожарную сирену 1 IF датчик 2 показывает наличие дыма THEN включить пожарную сирену 2 ° ° ° IF датчик показывает наличие дыма THEN включить пожарную сирену Но благодаря унификации появляется возможность использовать в качестве идентификатора датчика единственную переменную?Ю, что позволяет записать одно правило, следующим образом IF датчик ?N показывает наличие дыма включить пожарную сирену ?N После унификации двух взаимно дополнительных литералов их можно удалить с помощью резолюции. Например, если рассматриваются два приведенных Процесс поиска переменных, которые могут быть подставлены для того, чтобы параметры стали совпадающими, называется унификацией. Унификация — это одна из особенностей, которая отличает экспертные системы от систем с простыми деревьями решений. Без унификации можно было бы согласовывать в условных элементах правил только константы. Это означает, что приходилось бы записывать конкретное правило для каждого возможного факта. Например, предположим, что разработчики системы противопожарной защиты решили предусмотреть включение звукового сигнала пожарной тревоги при обнаружении дыма одним из датчиков. Причем, если бы количество датчиков было равно N, то потребовалось бы отдельное правило для каждого датчика, как в следующем примере: Глава 3. Методы логического вывода 260 выше выражения, то подстановка b вместо у позволяет получить следующее F(b) На, о) F(b) Теперь предикат F унифицирован и может быть удален с помощью резолюции, что приводит к преобразованию этих двух выражений водно На, о) Вообще говоря подстановка определяется как одновременная замена переменных термами, которые рассматриваются как отличные от переменных. В качестве термов могут использоваться константы, переменные и функции. Конкретный вариант подстановки термов вместо переменных представляется в виде множества, примерно так (1/<1 2/2 ° ° > ХИ) Если 0 такое множество, а А — доказательство, то АО определяется как подстановочный экземпляр А. Например, если заданы следующие подстановка и доказательство 0 = (а/х,/(у)/р,х/з) А = Р(х) v Q(y) v В) то подстановочный экземпляр принимает такой вид АО = Р(а) v Q(f (y)) v В(х) Обратите внимание на то, что подстановка выполняется одновременно во всех выражениях, поэтому был получен терм В(х), а не В(а). Предположим, что имеются два выражения, Си С, определенные следующим образом С = Р(х) С = РЦ()) Одной из возможных унификаций предиката Р является следующая С — — Cg(f (х) = P(f (С' — — С1(/(а)/ } = Р(/(а)) С = С = РУ()) Еще одна возможная унификация для предиката Р может предусматривать две подстановки с использованием константы а 261 3.13. Резолюция и логика предикатов первого порядка В этом выражении 0P — это составная подстановка, созданная путем применения вначале подстановки 0, а затем подстановки Р. Алгоритмом унификации называется метод поиска наиболее общего унификатора для конечного унифицируемого множества доказательств. Для рассматриваемого примера, состоящего из выражений (а) — (ЗЬ), результаты подстановки и унификации показаны в дереве опровержения резолюции (рис. 3.20). Корнем этого дерева является выражение nil, а это означает, что отрицаемое заключение является ложным, поэтому заключение, что "ни одно нарушение в работе не является успехом", является действительным. Рис. 3.20. Дерево опровержения резолюции, применяемое для доказательства того, что ни одно нарушение в работе не является успехом Рассматриваемые до сих пор примеры были простыми, а выполняемые в них операции резолюции — несложными, хотя и утомительными для человека. Ново многих других ситуациях процесс резолюции может зайти в тупик, что приводит к возникновению необходимости выполнить возврат, чтобы попытаться найти Следует отметить, что подстановочный экземпляр Р(/(х)) является более общим, чем Р(/(а)), поскольку подстановка некоторой константы вместо х позволит в дальнейшем получить бесконечное количество экземпляров Р(/(х)). Поэтому выражение, подобное С, называется наиболее общим выражением. Вообще говоря, подстановка О называется унификатором для множества выражений (А1,А,...,A„j тогда и только тогда, когда А = АО = АО. Множество выражений, для которого может быть предусмотрен некоторый унификатор, называется унифицируемым. А наиболее общим унификатором (most general unifier — mgu) называется такой унификатор, по отношению к которому все прочие унификаторы являются экземплярами. Это определение можно выразить более формально, указав, что О представляет собой наиболее общий унификатор тогда и только тогда, когда для каждого унификатора о множества выражений имеется подстановка,д, такая, что Глава 3. Методы логического вывода альтернативные варианты выбора выражений для резолюции. Безусловно, метод резолюции является очень мощными служит основой языка, но при решении некоторых задач он может оказаться неэффективным. Одним из недостатков метода резолюции является то, что в нем не предусмотрена действенная встроенная стратегия поиска, поэтому программист вынужден предусматривать применение эвристических средств, таких как операторы отсечения языка РВ.OLOG, для обеспечения эффективного поиска. Был исследован целый ряд модифицированных версий резолюции, таких как повышение приоритета единичных выражений, резолюция по входным данным, линейная резолюция и применение множества поддержки. Основным преимуществом резолюции является то, что она представляет собой единственный мощный метод, подходящий для многих случаев. Благодаря использованию резолюции становится проще создавать универсальные системы логического вывода, такие как PROLOG, чем системы, в которых предпринимается попытка реализовать много разных правил логического вывода. Еще одно преимущество резолюции состоит в том, что в случае успешного завершения процесса резолюции автоматически формируется доказательство, в котором демонстрируется последовательность этапов, приведших к получению выражения nil. 3.14 Прямой и обратный логический вывод Р +Ч Группа из нескольких этапов логического вывода, соединяющих задачу с ее решением, называется цепью (логического вывода. Цепь, поиск которой или переход по которой осуществляется от задачи к ее решению, называется прямой цепью. Для описания процесса построения прямой цепи (называемого также формированием прямого логического вывода) применяется еще одно определение проведение рассуждений от фактов к заключениям, которые следуют из этих фактов. А цепь, переход по которой происходит от гипотезы обратно к фактам, поддерживающим эту гипотезу, называется обратной цепью. Еще одним способом описания процесса построения обратной цепи (называемого также формированием обратного логического вывода) является определение, в котором речь идет о цели, достигаемой путем выполнения подцелей. Как показывают эти определения, выбор терминологии, используемой для описания прямого и обратного логического вывода, зависит от рассматриваемой задачи. Процессы построения прямой или обратной цепи можно легко описать в терминах логического вывода. Например, предположим, что в нашем распоряжении имеются следующие правила типа модус поненс: 3.14. Прямой и обратный логический вывод 263 Ас помощью этих правил формируется примерно такая цепь логического вывода elephant(x) — + mammal(x) mammal(x) — + ашта1(х) Эти правила могут использоваться в причинной цепи прямого логического вывода, позволяющей прийти к дедуктивному заключению, согласно которому, если дано, что Клайд — слон, из этого следует, что Клайд — животное. Такая цепь логического вывода показана на рис. 3.21. Обратите внимание на то, что та же диаграмма может также служить иллюстрацией процесса обратного логического вывода. Рис. 3.21. Причинная прямая цепь На рис. 3.21 причинная цепь представлена в виде последовательности вертикальных черт (), соединяющих консеквент одного правила с антецедентом другого. Вертикальная черта обозначает также унификацию переменных с фактами. Например, прежде чем появится возможность применить правило для слонов (elephant), необходимо вначале унифицировать переменную х в предикате elephant(x) с учетом факта elephant(Clyde). Данная причинная цепь фактически представляет собой последовательность операций импликации и унификации, как показано на рис. 3.22. Обратный логический вывод представляет собой противоположный процесс. Предположим, что требуется доказать гипотезу Центральная задача обратного логического вывода состоит в поиске цепи, связывающей свидетельство с гипотезой. В проблематике обратного логического вывода факт elephant(Clyde) называется свидетельством для указания на то, что этот факт используется для обоснования гипотезы, по такому же принципу, как свидетельство в суде применяется для доказательства виновности или невиновности ответчика 264 Глава 3. Методы логического вывода Рис. 3.22. Явная причинная цепь В качестве простого примера прямого и обратного логического вывода предположим, что вы управляете автомобилем и внезапно обнаруживаете полицейский автомобиль с мерцающими проблесковыми маячками и включенной сиреной. Применяя прямой логический вывод, вы можете прийти к заключению, что полицейские требуют, чтобы остановились вы или кто-либо другой. Это означает, что в данном случае исходные факты служат обоснованием для двух возможных заключений. Если же полицейский автомобиль пристроится прямо за вашим автомобилем или вам сделает знак жезлом полицейский, то дополнительные этапы логического вывода позволят прийти к заключению, что требование остановиться относится к вам, а не к кому-либо другому. Приняв это за рабочую гипотезу, вы можете применить обратный логический вывод для рассуждений о том, чем вызвано это требование. В качестве некоторых возможных промежуточных гипотез можно принять предположение, что вы оставили мусор, превысили скорость, используете неисправное оборудование или ведете краденый автомобиль. Теперь вы можете приступить к изучению свидетельств, позволяющих обосновать такие промежуточные гипотезы. Была ли причиной преследования вашего автомобиля та бутылка из-под пива, которую вы выбросили из окна, проезд на скорости 100 миль в час по участку дороги с ограничением скорости в 30 миль в час, разбитые задние сигнальные огни или номерные знаки автомобиля, которые указывает на то, что выведете краденый автомобиль Предположим, что в данном случае каждый фрагмент свидетельства поддерживает промежуточную гипотезу, поэтому все эти фрагменты являются истинными. Это означает, что любая из промежуточных гипотез или все гипотезы являются возможными основаниями, позволяющими доказать рабочую гипотезу, что требование остановиться относится именно к вам. Часто бывает полезно визуально представить ход прямого и обратного логического вывода в терминах пути через пространство задач, в котором промежуточные состояния соответствуют промежуточным гипотезам при обратном логическом выводе или промежуточным заключениям при прямом логическом выводе. В табл. 3.15 приведены некоторые общие сведения о характерных особенностях
3.14. Прямой и обратный логический вывод 265 Таблица Некоторые характерные особенности прямого и обратного логического вывода Обратный логический вывод Прямой логический вывод Планирование, текущий контроль, управление
Диагностика От настоящего к будущему От антецедента к консеквенту От настоящего к прошлому От консеквента к антецеденту Управляемые данными, восходящие рассуждения
Управляемые целями, нисходящие рассуждения Поиск в обратном направлении для определения фактов,
|
|
|
Скачать 3.73 Mb.