APPROCHE LOGIQUE DE L'INTELLIGENCE ARTIFICIELLE 1 DE LA LOGIQUE CLASSIQUE A LA PROGRAMMATION LOGIQUE par Andre Thayse, Pascal Gribomont, Georges Louis, Dominique Snyers. Pierre Wodon Philips Research Laboratory, Bruxelles Paul Gochet Universite de Liege Eric Gregoire Universite de Louvain, Louvain-la-Neuve Eduardo Sanchez Ecole Polytechnique Federale de Lausanne avec la collaboration de Philippe Delsarte Philips Research Laboratory, Bruxelles Dunod informatique v ЛОГИЧЕСКИЙ ПОДХОД К ИСКУССТВЕННОМУ ИНТЕЛЛЕКТУ От классической логики к логическому программированию Перевод с французского П. П. Пермякова под редакцией Г. П. Гаврилова Москва «Мир» ]990 ББК 32.973 Л 69 УДК 681.3 Авторы: А. Тей , П. Грибомон, Ж. Луи, Д. Сний- ерс, П. Водон, П. Гоше, Э. Грегуар, Э. Санч.ес, Ф. Дельсарт Л69 Логический подход к искусственному интел- лекту: от классической логики к логическому программированию: Пер. с франц./Тейз А., Гри- бомон П., Луи Ж. и др. — М.: Мир, 1990. — 432 с., ил. ISBN 5-03-001636-8 (русск.) Монография специалистов из Бельгии и Швейцарии, излагающая проблемы и методы искусственного интеллекта с точки зрения математической логики. Она состоит из шести глав: логика, аксиоматические системы, представле- ние знаний и рассуждении, логика и модифицируемые рас- суждения, формальные грамматики и логической програм- мирование, Пролог и логическое программирование. Книга построена так, что для понимания материала от читателя требуется только знание основ информатики. Для всех изучающих и использующих методы искусст- венного интеллекта и логического программиоования. 1602110000—423 041(01)—90 22—90 ББК 32.973 Редакция литературы по математическим наукам ISBN 5-03-001636-8 (русск.) ISBN 2-04-018658-1 (франц.) Bordas, Paris, 1988 перевод на русский язык, П. П. Пермяков, 1990 Предисловие редактора перевода Многообразие научных и технических исследований, называемое искусственным интеллектом, уже давно использует различные логические средства — язык, понятия и приемы логических исчислений. В искус- ственном интеллекте есть целая область, существенно опирающаяся на логические представления и кон- струкции, основная ее задача состоит в разработке способов доказательства теорем. Вполне естественным поэтому представляется стремление авторов данной книги рассказать и пока- зать, где и как работает логика в искусственном ин- теллекте; причем они попытались сделать это так, чтобы изложение было доступно даже читателю, не имеющему специальной подготовки ни по искусст- венному интеллекту, ни по логике. Отметим, однако, что решить эту сложную задачу в полной мере авторам, как нам кажется, пока не удалось. Но все же «развеять немного туманную за- весу» над довольно обширной «логической панора- мой» искусственного интеллекта они смогли. Читателю, не являющемуся специалистом по ло- гике, книга, бесспорно, сослужит добрую службу, хотя и потребует от него систематического ее прочтения и привлечения хорошего руководства по математиче- ской логике. Для читателя, имеющего традиционную логическую подготовку, т.,е. изучавшего теорию вы- сказываний (логику и исчисление) и теорию преди- катов первого порядка (логику и исчисление), инте- рес могут представить гл. 3 и 4, материал которых на русском языке в достаточно последовательном и полном виде пока еще не появлялся. Та часть книги, в которой описывается ряд аспектов логического про- граммирования, просто представляет читателю неко- торые взаимосвязи, существующие между логически- ми исчислениями и языками логического программи- рования. Она, естественно, не может служить руко- водством по Прологу. Предисловие редактора перевода В предисловии авторы говорят о своем намерении осветить в последующих томах и другие важные приложения логики в искусственном интеллекте. Как стало известно, в настоящее время появился второй том, имеющий подзаголовок «От модальной логики к логике баз данных». В заключение отметим, что, по нашему мнению, книга будет полезна научным и инженерно-техниче- ским работникам, а также студентам старших кур- сов вузов и всем читателям, интересующимся при- ложениями математической логики. Г. П. Гаврилов Предисловие Цель этой книги — представить понятия и методы ис- кусственного интеллекта (ИИ), используя в каче- стве определяющего логический подход. Мы стре- мились добиться достаточно автономного и дидакти- чески выдержанного изложения. Оно ориентировано на читателей (студентов или исследователей), имею- щих хорошую культуру в области математики и ин- форматики. Однако особых знаний ни в логике, ни в ИИ не предполагается. Мы пока что запланировали выпустить два тома. Содержание данного тома, пер- вого из них, можно описать следующим образом. В первой главе собраны математические и логи- ческие сведения, которые будут использоваться в дальнейшем. Излагаются основные понятия класси- ческой логики. Сперва рассмотрено исчисление вы- сказываний, а затем — исчисление предикатов. Осо- бое внимание уделено методу резолюций и связан- ным с ним понятиям, что обусловлено их ролью в приложениях. Вторая глава представляет аксиоматический под- ход к логике и служит введением в теории первого порядка. В ней показано, как исчисление предикатов превращается в основу теории для изучения специ- фических математических структур. В этом контексте изложены некоторые фундаментальные вопросы ло- гики, естественным образом продолжающиеся в тео- ретическую информатику. В частности, это касается алгоритмических языков Тьюринга и Гёделя, тезиса Чёрча, класса вычислимых функций и понятия раз- решимости. В третьей главе показано, как классическая логи- ка (особенно логика предикатов) может использо- ваться для представления знаний и автоматических рассуждении, относящихся к ним. Изложены ме- тоды, позволяющие преобразовать логическое представление в сетевое и объектное. Затем обсуж- Предисловие даются сравнительные достоинства этих различных представлений. Классическая логика связана с фор- мализацией корректных рассуждении. Однако, как это бывает в ИИ, моделирование рассуждении не ограничивается областью абсолютно корректных рас- суждений. Основанные на неполной, неточной или изменчивой информации, наши рассуждения часто гипотетичны, лишь в той или иной степени правдопо- добны и предполагают осуществление систематиче- ских пересмотров (модификаций). Четвертая глава служит введением в логики, ко- торые предназначены для формализации модифици- руемых рассуждении: логики умолчаний, модальные логики знания и веры, немонотонные логики, авто- эпистемические логики. Пятая глава — вспомогательная. В ней показы- вается, как логическая интерпретация формальных грамматик и их правил вывода приводит к языкам логического программирования, наиболее известным из которых является Пролог. Грамматики классифи- цированы по иерархии Хомского. Каждая из грамма- тик этой иерархии описывается соответствующей ма- шиной или автоматом. Автомат является основной моделью в теории грамматик и языков. Эта модель послужила источником сетевого формализма. Пока- зана связь между такими сетями и языками функцио- нального программирования, среди которых особенно типичен Лисп. В шестой главе представлен язык программирова- ния Пролог. Его создание навеяно формальной логи- кой и формальными грамматиками. В Прологе неко- торые логические формулы (хорновские дизъюнкты) становятся инструкциями, допускающими исполнение на ЭВМ. Пролог можно считать языком ИИ, который хорошо приспособлен для автоматизации некоторой формы логических рассуждении. В этом смысле он представляет собой итог изучения понятий и методов ИИ, основанных на логике. Итак, главная цель авторов — изложить согласо- ванно и стройно набор дисциплин, включающий: классические логики, представление знаний и кор- ректные рассуждения, неклассические логики, моди- Предисловие фицируемые рассуждения, формальные грамматики, теорию автоматов, логическое программирование (особенно язык Пролог). Это интеграция различных дисциплин такого типа для решения сложных про- блем, составляющих предмет того, что обычно при- нято называть ИИ. Среди проблем, особенно часто исследуемых свойственными ИИ методами, назовем распознавание и понимание речи и изображений, со- здание экспертных систем, имитацию рассуждении (например, в функционировании сознания или меди- цинских дисциплинах), робототехнику. Зависимость между главами первого тома этой книги можно схематически изобразить так. Планируется выпуск второго тома, который будет посвящен четырем следующим темам: • временная логика и ее приложения в ИИ и информатике, • углубленное изучение представления знаний л рассуждении, • логические грамматики и их применение к мо- делированию естественного языка и пониманию речи, • логика баз данных и баз знаний. Авторы хотели представить в этих двух томах основы ИИ, руководствуясь логикой. Важные аспек- ты ИИ были либо сильно сокращены (как, например, логическое программирование), либо полностью обойдены молчанием. В частности, последнее отно- сится к: • функциональному программированию и объ- ектно-ориентированному программированию, 10 Предисловие • доказательству теорем и верификации про- грамм, • эвристикам поиска и стратегиям, • видению, пониманию речи, обучению, • построению экспертных систем. Эти темы могли бы быть изложены в последую- щих томах. Мы благодарны всем, кто помог нам в работе: Даниэль Брике, Мари-Франс Деклерфей, Даниэль Дзиржовски, Пьер-Ив Шоббен и Мишель Зинцофф согласились прочесть и прокомментировать части этой книги. Анна-Мари Де Сеете и Эдит Моэ участвовали в редактировании текста. Один из авторов (Эрик Грегуар) благодарит Бельгийский институт научных исследований в про- мышленности и сельском хозяйстве за оказанную под- держку (Конвенция 4856: Общее направление иссле- дований в ИИ). 1. Логика 1.1. Исчисление высказываний 1.1.1. Введение Исчисление высказываний — одна из самых простых теорий, однако оно основательно используется в весь- ма различных областях. Логикам, информатикам и математикам необходима полная ясность. Исчисление высказываний изучает предложения, которые могут быть либо истинными, либо ложными. Рассмотрим три следующих истинных предложения (утверждения) : • За четверть часа до своей смерти он был еще жив. • Если верно, что когда идет дождь, то дорога мокрая, то справедливо также и следующее утверждение: если дорога сухая, то дождя нет, • Земля вертится. Чтобы убедиться в правильности первого предло- жения, достаточно понимать смысл слов: это предло- жение является истиной языка. Чтобы принять вто- рое утверждение, достаточно понимать смысл некото- рых слов (если ... то, нет), а также знать, что куски фразы «идет дождь» и «дорога мокрая» являются высказываниями, т. е. предложениями, которые могут быть истинными или ложными. Второе предложение останется истинным, если заменить эти два высказы- вания другими. Такие истины языка называются ло- гическими истинами. Напротив, третье предложение не является истиной языка, так как оно выражает не- который факт (в данном случае — из физики и астро- номии). Таким образом, это предложение—фактиче- ская истина. 1.1.2. Словарь Пропозициональный логический словарь традиционно составляется из бесконечного счетного множества 208 3. Представление знаний и рассуждении 3.3.13. Заключение Логика предикатов применима для представления зна- ний, используемых некоторыми системами ИИ. Одна- ко существуют специфические виды знаний, с трудом представимые языком логики предикатов. Поэтому мы ввели неклассические (модальную и .временную) логики и альтернативные (сетевое и объектное) пред- ставления. С другой стороны, мы указали различные методы рассуждении, связанных с логическим, сетевым и объектным представлениями. Кроме того, определи- ли рассуждения с умолчаниями в рамках объектного представления. Это подвело нас к введению других видов рассуж- дении (таких как рассуждения здравого смысла, не- строгие рассуждения по поводу предположений и мо- дифицируемые рассуждения), формализация которых дается в гл. 4. 4. Логика и модифицируемые рассуждения 4.1. Многочисленные роли логики 4.1.1. Введение В гл. 3 введены различные элементарные формы пред- ставления знаний: логическая, сетевая и объектная. Две последние часто являются альтернативой первой. Было показано, что их можно переписать и переинтер- претировать с помощью логического формализма. Таким образом, мы подошли к вопросу о реальной роли логики в методах представления знаний и рас- суждений. В действительности форма вклада, который мате- матическая логика должна вносить в развитие мето- дов представления знаний и рассуждении, остается предметом нескончаемых дебатов. В этой связи воз- можны различные, не исключающие друг друга, точ- ки зрения: • Логика может рассматриваться как средство, хорошо подходящее для представления знаний и рассуждении. • Логика может рассматриваться как формализм для ссылок. • Логика может рассматриваться как метод под- тверждения рассуждении и семантического ана- лиза представленных знаний. В параграфах этого раздела будут развиты эти различные точки зрения на роль логики. 4.1.2. Логика как средство для представления знаний и рассуждении Предмет формальной логики — корректные формы рассуждении. Она предоставляет различные средства формализации и анализа правильности дедуктивных 210 4. Логика и модифицируемые рассуждения рассуждении. Эти средства рассмотрены в гл. 1: системы семантической оценки и системы вывода формул. Методы формализации и обоснования рассуждении были привиты на различные языки, позволяющие представлять знания. Важнейшее свойство этих язы- ков состоит в том, что они предоставляют пользова- телю строгий синтаксис. Второе свойство заключено в существовании средств связи с семантикой. Это по- зволяет установить однозначное соответствие между миром и его представлением в языке. Более того, они обеспечивают обоснование выводов, которые можно сделать из представленных знаний. Таким образом, логическая система будет со- стоять из языка, формальной семантики и системы вывода 1). Эти логические средства, можно применять довольно непосредственно. Логические языки служат опорой для выражения знаний, которые также пред- ставлены декларативно в виде логических выражений. Рассуждение определяется как операция доказатель- ства общезначимости или выполнимости логического утверждения. Напомним, что логическая формула общезначима, если все ее интерпретации являются мо- делями, и выполнима, если допускает хотя бы одну модель (§§ 1.1.6, 1.2.5). Рассуждения осуществляются окольным путем, посредством манипулирования дедук- тивными компонентами рассматриваемой логической системы. Например, такими компонентами являются классические аксиоматические системы (§§ 2.1.3, 2.1.8), системы натурального вывода (§§ 2.1.7, 2.1.9) или се- мантика рассматриваемой логической системы. Так как процесс доказательства должен быть автоматизи- рован, то это очень часто реализуется методами пои- ска, причем производится систематическая манипуля- ция с дедуктивной компонентой. Этот способ действий ведет к методу логического программирования [58], [63], который можно прямо использовать для представления знаний и рассужде- ]) Это верно для большинства обычных логических систем, но некоторые из названных средств могут отсутствовать у отдель- ных систем. Например, интенсиональные логики Монтегю [76] лишены системы вывода. 4.1. Многочисленные роли логики 211 ний. Наиболее распространенной системой такого сор- та является язык Пролог [19], [18]—соединение ме- тода резолюций (§§ 1.1.12, 1.2.14), языка хорновских дизъюнктов (§ 1.1.6), метода поиска вглубь типа об- ратного вывода (§ 3.1.23) и использование отрицания для получения противоречия [17]. Подобные системы будут описаны в гл. 5 и 6. Здесь мы ограничимся анализом их пригодности для пред- ставления знаний и рассуждении. Он имеет три ас- пекта: эпистемический, дедуктивный и связанный с алгоритмической эффективностью. • Эпистемический аспект Поскольку конечная цель — представление зна- ний, основным критерием адекватности используемого логического языка является его выразительность. Си- стемы ИИ чаще всего ограничиваются применением логических языков порядков 0 и 1: логики высказы- ваний и логики предикатов. Логика предикатов слу- жит эталоном выразительности для альтернативных систем [44]. Кстати, она достаточно выразительна для решения многих проблем представления знаний в ИИ, но не универсальна. Некоторые знания формализуе- мы лишь в логических языках высших порядков. На- пример, квантификация формул не представима в ло- гике порядка 1. Была отмечена трудность формализации некоторых знаний в обычных логических языках. Типичные при- меры — пространственно-временные отношения, для которых лучше приспособлены специфические логики, в частности модальные (§ 3.1.11). С другой стороны, основные логические системы не оснащены средствами структурирования и агреги- рования знаний. Применение систем классификации и типизации объектов через механизм ассоциированного доступа прямо не предусмотрено. Иногда ищется ком- промисс через соединение чисто логических методов с объектным и сетевым представлениями (разд. 3.2, 3.3). Системы классификации и механизмы доступа объектного формализма используются для иерархиче- ского таксономического1) представления термов, на 11 Или, иначе, классификационного. — Прим. перев, 212 4. Логика и модифицируемые рассуждения которые ссылаются логические утверждения (§§ 3.2.19, 3.3.11). Логический язык дополняющим образом ис- пользуется для представления позитивных знаний об этих термах. Реализованный в системе KRYPTON [9] союз между логической и сетевой системами опи- рается не только на эпистемический аспект, но и на аспект эффективности. Чтобы оттенить сказанное, за- метим, что недавние применения систем логического программирования (вроде распространенной системы Пролога LOGIN [2]) направлены на внесение в ло- гику систем классификации с наследованием свойств (§3.2.13). • Дедуктивный аспект Формальная логика связана с формализацией и обоснованием корректных рассуждении. Последние также называются общезначимыми: их правильность несомненна при всех интерпретациях. Дедуктивные системы логики специально приспособлены для фор- мализации этого класса рассуждении. А распростра- няется ли их полезность на другие классы? Рассуждения, которые желательно моделировать в приложениях ИИ, не все общезначимы. Часто они приблизительны и неопределенны по сути или от не- полноты, или неопределенности предпосылок. Выве- денные из неопределенных рассуждении заключения должны допускать возможность отказа от них, если предпосылки, приведшие к принятию предположения о возможности этих заключений, больше не подтверж- даются или если новая информация блокировала эту дедукцию. Дедуктивные системы логики не позволяют прямо формализовать модифицируемые рассуждения. Симптом этой ограниченности — свойство монотон- ности всех обычных логических систем: множество теорем такой системы лишь растет с увеличением мно- жества основных аксиом. Различные логические си- стемы, формализующие модифицируемые рассужде- ния, будут введены и подробно описаны в последую- щих разделах этой главы. 4.1. Многочисленные роли логики 213 • Аспект эффективности Эффективность важна во всех практических при- менениях дедуктивных принципов логики. , Особое внимание следует обратить на стратегию проведения преобразований в дедуктивной системе. Ей грозит комбинаторный взрыв пространства поиска, могущего подчас стать бесконечным. Существенное неудоб- ство — неразрешимость логических систем, наблюдае- мая с тех пор, как она поразила логику предикатов (§2.2.11). 4.1.3. Логика как формализм ссылок Если можно считать логику средством представления знаний и рассуждении (возможно, в сочетании с бо- лее адекватными альтернативными системами), то можно признать за ней и другие роли. Можно интер- претировать логику как формализм ссылок, полезный на разных уровнях в определении других эффектив- ных методов представления. Прежде всего, она может служить их строгому определению. Переписыванием языков и законов в логический формализм можно уточнить семантику этих методов. Логика предика- тов широко используется для этого [44], но не всегда дает достаточно выразительную систему. Например, системы множественного наследования с исключения- ми (§ 3.3.12) позволяют выразить немонотонные фор- мы рассуждении. Их нельзя прямо переписать в ло- гику предикатов, но можно строго определить в более развитых логических языках [НО]. Так как многочисленные формализмы можно пе- реписать на логический язык, то последний — эталон выразительности. Альтернативный формализм можно строго определить путем переписывания его языка и законов в рамках логики. Сам он, вроде бы, и не ну- жен. Однако объективно уступающие логике предика- тов методы представления бывают привлекательны приростом некой эффективной выразительности. С Паскаля можно все перевести на язык ассемблера. Тем не менее Паскаль обладает в некоторых отноше- ниях превосходящей эффективной выразительностью. Так же как и некий формализм, сводимый к логике предикатов. 214 4. Логика и. модифицируемые рассуждения Особенно это относится к сетевым (разд. 3.2) и объектным (разд. 3.3) представлениям. Ранее мы продемонстрировали перевод /п-арных предикатов в бинарные и их интерпретации в сетевом и объект- ном представлениях. Таким образом, эти представле- ния «эквивалентны» логическому в смысле возмож- ности взаимного преобразования. Между тем было показано, что сетевое и объектное представления дают «структурный» образ мира, чего логическое представление само не делает. Логика может также выполнять роль блюстителя логических принципов и правил во всех системах, кроме явно оговоренных исключений. Соблюдение этих принципов в данном формализме можно прове- рить переписыванием их в логический или простым сравнением с ним. 4.1.4. Неизбежность логики Иногда утверждают, что некоторые проблемы пред- ставления знаний и рассуждении решаемы лишь с по- мощью логических языков и ассоциированных дедук- тивных систем (как бы то ни было с ролью логики как системы ссылок или средства точного определе- ния других формализмов). В частности, благодаря точному определению принципов применения опера- торов и связок (вроде конъюнкции, дизъюнкции, от- рицания, равенства, кванторов существования и об- щности) логика позволяет задать некоторые часто полезные парадигмы рассуждении [77]. Например, логика предикатов с равенством (§ 2.1.10) дает возможность: в выразить, что нечто обладает определенным свойством, не указывая, что именно (роль Э- квантификации), • выразить, что каждый элемент некоего класса обладает определенным свойством, без указа- ния, что представляет из себя каждый- такой элемент (роль V-квантификации), в выразить, что хотя бы одно из двух утвержде- ний истинно, не говоря, какое именно (роль дизъюнкции), 4.1. Многочисленные роли логики 215 в явно сказать, что нечто ложно (роль отри- цания), ® утверждать или оставлять неустановленным тот факт, что два различных выражения озна- чают один и тот же объект (роль равенства). Даже если бы дело дошло до задумывания нело- гического формализма, опирающегося на эти функ- циональные средства выразимости и дедуктивности, то естественно возник бы вопрос о возможности об- ретения вновь некой разновидности логики. Эти парадигмы полезны и подчас необходимы при решении многих проблем (в частности, требующих рассуждении в ,условиях неполной информации). Вот пример [77]. Три блока Л, В и С расположены в линию (рис. 4.1). Известно, что Л зеленый и С си- ний. Цвет В неизвестен. Находится ли зеленый блок рядом с незеленым? Ответ «да»: если В зеленый, то он рядом с незеленым С. Если В незеленый, то он рядом с зеленым А. Согласно Муру, три трудно познаваемых в нело- гическом формализме логических фактора вплетены в рассуждения для обретения возможности: • увидеть истинность Э-квантифицированного вы- сказывания, не зная, какой объект делает его истинным, • распознать подтверждаемость некоего высказы- вания, либо его отрицания, ® рассматривать ряд случаев по отдельности. 4.1.5. Анализ знаний и рассуждении Иные авторы приписывают логике в основном функ- ции семантического анализа знаний и обоснования выводов [43], [82]. Представить знания — это значит выразить в не- котором формализме имеющийся у нас образ мира. А В Рис. 4.1. Пример. 216 4. Логика и модифицируемые рассуждения Соответствие между миром и его представлением устанавливается семантическим анализом. Такой анализ имеет целью определить объекты представле- ния и уточнить образ мира, определяемый представ- лением. Следовательно, оно должно позволить осу- ществлять анализ истинности высказываний о мире. Иначе говоря, для плодотворности представления нужно, чтобы оно могло быть предметом анализа, использующего информацию из этого представления для выявления того, что свойственно миру, а что нет. С этой точки зрения обоснованный вывод или дедук- ция «подтверждаются» видением мира, который опре- делен семантическим анализом представления. Сказать, что Р. Рейган все еще жив и является президентом США, — это значит вообразить мир, где истинно, что Р. Рейган жив, но и равным образом ложно, что он мертв и что другой человек является президентом США, если известно, что у власти мо- жет находиться лишь один президент. Семантический анализ представленного в некото- ром формализме знания должен позволять опреде- лить, что в этом воображаемом мире влечет истину, а что — ложь. Даже если анализ облечен другими аспектами, подобная операция относится по опре- делению к компетенции логики и делает особенно полезным обращение к теории моделей [43], [77], [82]: «...нелогический анализ знаний—такая же чушь, как программирование без программистов...» [82, с. 17]. Итак, логику можно считать преимущественно средством анализа знаний и рассуждении. В свою очередь это вызывает другие рассмотрения. 4.1.6. Заключение Роль логики в проблематике представления знаний и рассуждении многообразна. • Логику можно прямо использовать для пред- ставления знаний и рассуждении. • Она может пригодиться для ссылок и как эта- лон выразительности, модель компетенции, га- рант элементарных логических принципов. Мо- 4.2. Логика и модифицируемые рассуждения 217 жет помочь в точном определении альтернатив- ных методов. • Она определяет принципы и законы, незамени- мые при решении многих проблем. • Она позволяет анализировать смысл некоего представления знаний и обоснованность вы- водов. • В этом отношении она является преимущест- венно средством анализа знаний и рассужде- нии как таковых. 4.2. Логика и модифицируемые рассуждения 4.2.1. Формализация модифицируемых рассуждении Классическая логика формализует строго корректные рассуждения. Моделирование встречающихся в ИИ рассуждении не должно ограничиваться формализа- цией непогрешимого интеллекта. Наш интеллект ча- сто способен вырабатывать разумные рассуждения в условиях неопределенности. Имея дело с неполной, неточной или изменчивой информацией, наши рас- суждения часто предположительны, всего лишь прав- доподобны и должны подвергаться пересмотру. Рас- смотрим пример. «Зная, что большинство птиц может летать и что Тити — птица, я заключаю, что Тити может летать». Этот вывод кажется приемлемым. Между тем он не является абсолютно корректным и общезначимым, ибо не учитывает возможных исклю- чений. Следовательно, он неточен и подлежит пере- смотру. Если уточнено, что Тити—страус, то утверж- дение «Тити может летать» отвергается. Априори ясно, что логическая система для форма- лизации модифицируемых рассуждении должна быть немонотонной. Численность теорем, которые можно получить, может уменьшаться при росте числа основ- ных аксиом или предпосылок. 4.2.2. Классическая логика и общезначимые рассуждения Дедуктивные системы классической .логики ограничи- ваются формализацией общезначимых рассуждении 218 4. Логика и модифицируемые рассуждения (разд. 2.1). Следовательно, как таковые они не под- ходят для формализации нестрогих и модифицируе- мых рассуждении. Фундаментальные свойства фор- мальных систем дедукции ясно свидетельствуют об этой ограниченности. Формальная система дедукции классической ло- гики состоит из множества схем аксиом и правил вы- вода (разд. 2.1). Она позволяет делать заключения из предпосылок. Таким образом, между формулами определено отношение выводимости I—, которое [35]: • рефлексивно: {р^, ...,/?„, q} \- q, • монотонно: если {/?i, . .., рп} \- q, то {pi, ..., рп, г}(-<7, • транзитивно: если [pi, ..., рп} h- r и {pi, ..., рп, г)1--<7, то {PI, ••-, Рп}\- q. Здесь /?i, ..., рп, q, г — формулы рассматриваемого логического языка. Эти фундаментальные свойства формализуют требования к общезначимым рассуж- дениям: • Вывод заключения, идентичного одной из по- сылок, есть общезначимая операция. • Полученный результат не опровергается даль- нейшими. • Промежуточные результаты можно использо- вать для установления общезначимости за- ключения. Формальные системы дедукции классической ло- гики предстают как алгебраические системы перепи- сывания с учетом этих требований. Свойство моно- тонности препятствует прямой формализации моди- фицируемых рассуждении. Следовательно, с чисто синтаксической точки зрения построение немонотон- ной системы вывода делает необходимым ослабление свойств дедуктивных систем классической логики. Классическое определение отношения семантического следования непригодно для формализации модифи- цируемых рассуждении. 4.2. Логика и модифицируемые рассуждения 219 Семантическая характеризация логической систе- мы состоит в приписывании семантических значений выражениям языка посредством интерпретации.. Если последняя истинна, то она есть модель (§ 1.2.5). Эта характеризация осуществляется посредством припи- сывания семантических значений основным выраже- ниям языка и определения правил семантической оценки 1) более сложных выражений. Например, та- ков композиционный принцип, который был описан в §§ 1.1.4, 3.1.10. Отношение семантического следования |== (§ 1.1.6) между множеством посылок Л и заключе- нием р классически определяется так: А\= р, если любая модель для А является моделью для р. В этом определении слово «любая» влечет, что из Л можно вывести лишь «точные» («общезначи- мые») следствия. Модифицируемое рассуждение не является в клас- сическом смысле общезначимым. Вывести р из мно- жества посылок Л и отказаться от р, как только ин- формация q будет добавлена к Л, означает, что до- пустимо вывести р, в то время как существует модель для Л U [q} (которая тем более является моделью для Л), не подтверждающая р. Для построения немонотонной логики нужно оп- ределить отношение вывода, позволяющее получать заключения, которые подтверждаются не во всех мо- делях для посылок. Неадекватность систем дедукции классической ло- гики для формализации модифицируемых рассужде- нии объясняется также тем, что их правила вывода являются лишь позволяющими [74]. Они всегда имеют вид: «<7 — теорема, если pi, pi, ..., рп — тео- ремы». Это позволяет лишь получать новые теоремы, но не отказываться от ранее полученных теорем. Мо- делирующая модифицируемые рассуждения система должна была бы содержать также ограничивающие правила вида: «q—теорема, если р\, рг, ..., рп—не теоремы». 1) Или, иначе, означивания. —\JJpuM. перед. 220 4. Логика и модифицируемые рассуждения 4.2.3. Характеристики немонотонных логик Немонотонные логики должны иметь системы вывода для моделирования модифицируемых (следовательно, необщезначимых в классическом с-мысле) рассужде- нии. Формализующая эти рассуждения система вы- вода должна давать «правдоподобные» формулы. С семантической точки зрения это* сводится к выводу выполнимых вместе с посылками формул (в смысле их подтверждения хотя бы в одной модели). В этом предположении моделируют разумного субъекта, за- ключения которого выполнимы вместе с множеством исходных сведений. Например, заключение «Тити ле- тает» не является общезначимым следствием из мно- жества двух посылок: «Большинство птиц летает» и «Тити — птица». Оно просто выполнимо с этим мно- жеством. Следовательно, заключение принадлежит к возможно выполнимому на основе двух своих посы- лок образу мира. С другой стороны, кажется разумным потребо- вать, чтобы невыполнимые в совокупности заключе- ния не выводились бы все вместе. Даже от способ- ного лишь на правдоподобные заключения субъекта можно потребовать согласованности утверждений. Недопустимо ему утверждать одновременно «Тити летает» и «Тити не летает». Требование выполнимости связано с модифицируе- мостью. При поступлении новой информации предпо- ложения могут стать невыполнимыми с новым мно- жеством посылок и будут отвергнуты. Узнав, что Тити — страус, и зная, что страусы не летают, мы отвергнем утверждение: «Тити летает». Немонотонная логика даст возможность выводить формулы, выполнимые как сами по себе, так и с дан- ным множеством посылок. В этом контексте нужно выяснить ряд логических вопросов. • Каков статут для формул, которые могут быть' выведены? Они больше не тавтологии и не общезначимы (в классическом смысле) по отношению к своим по- сылкам, но лишь выполнимы с ними (§§ 1.1.6, 1.2.5). 4.2. Логика и модифицируемые рассуждения 221 в Какова структура множеств выведенных фор- мул? В классической дедуктивной системе растущее множество образуют все заключения, выводимые из множества посылок. Множество посылок можно уве- личить лишь вместе с увеличением множества за- ключений. Немонотонная система" не обязана обла- дать этим свойством. Из нее можно получить, ис- пользуя правила вывода, различные несовместные множества формул. Отдельно взятое множество заклю- чений существенно зависит от порядка применения правил вывода. Если выведена всего лишь правдопо- добная формула, то следует запретить дальнейшее выведение других правдоподобных (но невыполни- мых вместе с первой) формул. Например, если выве- дено «Тити летает», то нельзя выводить «Тити не ле- тает». И наоборот. Таким образом, в зависимости от порядка применения правил вывода можно получить два разных множества формул. • Как избежать наличия нескольких несовмести- мых множеств возможных заключений? Можно ослабить монотонность (§ 4.2.2) до огра- ниченной монотонности [35]: если {pi, .. ., рп} |~ г и{/?1, .. ., pa} 1~ q, то {/?i,. .. •••, Рп, г} |~ q , (где |~ есть символ отношения выводимости в рассма- триваемой системе). Заметим, что ограниченная монотонность не поз- воляет моделировать взаимно несовместимые альтер- нативы рассуждении. • Как охарактеризовать множества возможных заключений? Когда формулы сначала выводят, а потом отвер- гают, утрачивается простая итеративная структура классических аксиоматических систем (§ 2.1.2), поз- воляющая строить и перечислять множества возмож- ных заключений. 222 4. Логика и модифицируемые рассуждения Охарактеризуем множества выводимых формул с .ц помощью «неподвижных точек» соответствующих опе- раций. Неподвижная точка представляет собой устой- чивое множество предположений, из которого нельзя вывести никакую новую выполнимую формулу. Этот метод непосредственно применяется в немонотонные логиках Мак-Дермотта (разд. 4.5). В логиках умол- чаний Рейтера (разд. 4.3) он предстает в виде рас- ширений с умолчаниями, а в автоэпистемических ло- гиках Столнекёра и Мура (разд. 4.6) — в виде устойчивых расширений, полных и легальных мно- жеств заключений идеально разумного субъекта, вы- веденных из множества посылок. • Что станет с понятиями теоремы, общезначи- мого вывода и доказательства? Мнения расходятся. В классической логике тео- рема — это тавтология и результат общезначимых выводов. В теории формальных языков теорема пони- мается шире, как утверждение, выводимое с по- мощью системы подстановок термов (которая не обя- зательно дает общезначимые выводы). В немонотон- ной логике за «теоремы» можно принять формулы, присутствующие во всех выводимых устойчивых мно- жествах утверждений. Можно также поинтересовать- ся строением одного из этих множеств. Тогда будут представлять интерес и все утверждения, которые могут выражать картину мира, нарисованную неким субъектом с использованием исходных предположе- ний и с соблюдением свойства выполнимости. В по- следнем случае доказательство сводится к установле- нию существования для данной формулы устойчивого выполнимого множества предположений. Оно должно быть выводимым из рассматриваемых посылок и со- держать нашу формулу. Что будет с классическими метатеоремами? Без монотонности большинство метатеорем клас- сической логики станут необщезначимыми. Например, метатеорема дедукции (§ 2.1.4) неверна в немонотон- ных логиках Мак-Дермотта (разд. 4.5). 4.2. Логика и модифицируемые рассуждения 223 4.2.4. Зацикливание правил немонотонного вывода Если немонотонная система должна сама обеспечи- вать отказ от своих выводов, то ее правила вывода должны быть модифицируемыми. Их применение мо- жет динамически блокироваться. Для этого они осна- щаются условиями применения, проверка которых ди- намически изменяется вместе с множеством посылок. Эти правила будем называть правилами немонотонно- го вывода. Их условия (называемые предусловиями) позволяют проверять (до вывода) выполнимость не- коего утверждения вместе с уже выведенными утвер- ждениями в этой системе из существующего множе- ства посылок. Рассмотрим правило «если х птица, то х летает». Сделаем его правую часть выводимой, когда она всего лишь выполнима вместе с посылками и другими (уже выведенными) формулами. Для этого преобра- зуем наше правило в «если х птица и если выполним вывод, что х летает, то х летает». Условие выпол- нимости само может ставиться в форме невыводи- мости некоего утверждения: «Если выполним вывод, что х летает» можно заменить на «если нельзя выве- сти, что х не летает». Проверка такого рода предусловий может дина- мически изменяться вместе с множеством формул. уже выведенных системой, успешно сокращая мно- жество утверждений, выполнимых при данном со- стоянии системы. Как интерпретировать условия выполнимости и выводимости, используемые в этих предусловиях? В самом деле, интерпретация этих условий должна апеллировать к отношению выводимости, заданному системой, которая содержит эти правила с предусло- виями. Интерпретация понятия выводимости, входя- щего в предусловие «нельзя сделать вывод, что х не летает», должна учитывать то, что можно вывести с помощью оснащенных этим предусловием правил. Есть опасность зацикливания в определении и ин- терпретации отношения выводимости. Для проверки невыводимости некоего утверждения модифицируе- мые правила должны апеллировать к содержащей их 224 4. Логика и модифицируемые рассуждения системе вывода. Таким образом, для проверки пред- условия «нельзя сделать вывод, что х не летает» при- дется рассматривать все правила вывода системы, включая немонотонные. Следовательно, нельзя определить независимые отношения выводимости, чтобы задать проверку ус- ловий применения модифицируемых правил, с одной стороны, и охарактеризовать оснащенную правилами с предусловиями систему вывода, с другой стороны. Рассмотрим эту проблему ближе. Пусть р — вы- сказывание, 'А—множество высказываний, считаю- щихся посылками. Определим примитив UNLESS [97], [59] следующим образом: • UNLESS (p) истинно тогда и только тогда, когда р недоказуемо с использованием множе- ства посылок Л в логике высказываний. Этот примитив можно применять в определении правил немонотонного вывода перед разрешением получить новое утверждение, исходя из предполо- жения о невыводимости некоторых других утверж- дений. Для этого применим UNLESS к высказываниям данного языка как оператор истинности. Дедуктивная система логики высказываний, пополненная новыми правилами с этим оператором и примененная к мно- жеству посылок Л, немонотонна. Но она не обладает желаемыми свойствами. В частности, противореча уже изученному, она не запрещает вывести одновре- менно р и UN LESS (р), ибо UNLESS не зависит от нового отношения выводимости (как хотелось бы), но лишь от дедуктивной системы логики высказываний. Действительно, вообразим немонотонное правило UNLESS(q)\-^ p. Предполагая недоказуемость р из множества посылок Л в логике высказываний, выводим UN LESS (р), опи- раясь прямо на определение UNLESS. С другой сто- роны, если q недоказуемо из множества посылок Л в логике высказываний, то получаем UN LESS {q). Из последнего по правилу немонотонного вывода сле- дует р. 4.2. Логика и модифицируемые рассуждения 22S Итак, годная для проверки условия немонотонно- го правила система выводы должна содержать это правило. 4.2.5. Полирасширяемость немонотонной системы Проиллюстрируем проблему полирасширяемости не- монотонной системы. Для этого предположим, что UNLESS корректно определен и зависит не только от исчисления высказываний, но и от всех других правил и аксиом данной системы. Последние могут и сами использовать примитив UNLESS. Пусть Sp — пополненный оператором UNLESS язык исчисления высказываний. Л — множество {а, а Л UNLESS (b) => с, а Л UNLESS [с) => Ь}, где а, Ь и с—высказывания из Зр. Очевидно, либо b, либо с выводимы из Л, но не оба сразу. Действи- тельно, если Ь невыводимо в этой системе, то имеем UN.LESS(b}. Откуда можно вывести с. Но тогда нельзя вывести UNLESS (с). Совершенно симметрич- но, если невыводимо с, то выводимо Ь. Так можно получить различные несовместные множества заклю- чений из одного множества посылок. 4.2.6. Различные формы немонотонных рассуждении Природа модифицируемых рассуждении различна. Причины модификации знаний самые разные. Для выбора наиболее адекватных методов моделирования надо понимать явления и гипотезы, участвующие в рассуждениях. Выделим два класса модифицируемых рассуж- дении. • Рассуждения, модифицируемые из-за неопре- деленности и гипотетичности: Вообще объекты. типа Х имеют свойство Р. Если А — объект типа X, то я делаю вывод, что А (по-видимо- му) обладает 'свойством Р. Пример: «Если Тити— птица, то я вывожу, что (по-видимому) Тити летает». 8 А. Тейз и др. 226 4. Логика и модифицируемые рассуждения Знание, которое позволяет выводить подобные за- ключения, принадлежит к типу «большинство птиц летает» или «типичная птица летает». Это рассужде- ние неточно и дополнительная информация может привести к его модификации. • Рассуждения, модифицируемые по интроспек- тивной 1) природе: Исходя из состояния моих знаний, я могу сде- лать вывод, что...» Пример: «Мне ничего не известно о старшем брате, и отсюда я делаю вывод, что у меня нет старшего брата». Утверждение о том, что у меня нет старшего бра- та, сделано не потому, что «правдоподобно», что его у меяя нет. Механизм рассуждения иной. Он интро- спективен и основан на предположении о том, что все знания, имеющиеся по этому вопросу, таковы: «если бы у меня был старший брат, то я бы об этом знал». Можно потребовать от этих рассуждении, чтобы они осуществлялись «определенным образом», в пред- положении наличия и корректности всей соответст- вующей информации, полагая при этом, что все, что не дано, ложно. Иначе говоря, можно потребовать от рас- суждений «общезначимости» относительно этого со- стояния знаний [80]. Модифицируемый характер рас- суждений проистекает из зависимости от состояния знаний. Оно присуще рассуждающему субъекту и мо- жет изменяться. Попутно заметим, что многие модифицируемые от неопределенности рассуждения моделируемы интро- спективно. Но различие между двумя классами мо- дифицируемых логик важно для понимания областей применимости разных немонотонных логик. Послед- ние перечислены ниже и описаны далее в этой главе. • Логики умолчаний (разд. 4.3) —это логические системы, в которых немонотонность обусловле- на необщезначимостью правил вывода, прису- щих области применения. Правила выражают 1) За-висящей от текущего состояния знаний субъекта.—Прим. перев. 4.3. Логики умолчаний 227 знания типа «большинство птиц летает» в виде: «если вывод, что птица может летать, является выполнимым, то выводимо, что она летает». Та- ким образом, эти приемы вывода позволяют вы- разить правила с исключениями, не перечисляя исключений. • Немонотонные логики Мак-Дер мотта (разд. 4.5). Их назначение—предложить уни- версальную (независимую от области примене- ния) аксиоматическую систему оценки «выпол- нимых» множеств утверждений, выводимых из множества посылок. • Автоэпистемические логики (разд. 4.6) — это реконструкции немонотонных логик Мак-Дер- мотта. Они моделируют чисто интроспективные рассуждения. Идеально разумный субъект рас- суждает на основе своих предположений. Рас- суждения модифицируемы, ибо зависят от из- менчивого состояния знаний. • Методы, основанные на принципе замкнутого мира и принципе ограничения. Предполагается наличие в системе всей информации по данной проблеме. Соответствующие методы развива- ются и обосновываются теорией моделей (разд. 2.2). Они определяют (часто неявным образом) правила вывода истинных выраже- ний из посылок в некоторых моделях. Эти ме- тоды будут представлены во втором томе. 4.3. Логики умолчаний 4.3.1. Введение Логики умолчаний1) введены и развиты Рейтером {88] для формализации рассуждении, являющихся всего лишь выполнимыми. При неполной информации мы вынуждены получать всего лишь правдоподобные предположительные заключения. Иногда мы считаем абсолютно общими правила, которые правильны 1) Другое название—логики типичного.—Прим. перев. 8* 228 4. Логика и модифицируемые рассуждения в большинстве случаев, но допускают некие исклю- чения. Если Тити птица, то выводимо, что Тити летает. Не все птицы летают. Но можно без особого на то разрешения заключить «Тити летает», если это не за- прещено. Так как «Тити летает» выполнимо вместе с моими представлениями, то я заключаю «Тити ле- тает» (ибо это наиболее естественно). Это рассужде- ния с умолчаниями. Логики умолчаний позволяют формализовать та- кие рассуждения в виде правил вывода, называемых умолчаниями: о:Л1р v Интуитивный смысл таков. Если мы верим в та и если р выполнимо вместе со всем, во что мы верим, то можно верить и у. Итак, правило «птицы вообще летают» выразимо в виде: Птица (х} : М Летает (х) Летает (х) Интуитивно: если х птица и если выполнимо «л" ле- тает», то выводимо «х летает». Общее правило с ис- ключениями гласит, что типичные птицы летают. Это правило умолчания позволяет обрабатывать исключе- ния без их предварительной идентификации. Система логики умолчаний представляется тео- рией с умолчаниями (или подробнее: с правилами с умолчаниями}, состоящей из некоторого множества особо выделенных формул и правил вывода. В ней содержатся формулы логики предикатов, представ- ляющие основную информацию о системе, обрабаты- ваемую в соответствии с имеющимися аксиомами. Содержатся также правила умолчаний, отражающие различные утверждения, касающиеся исключений. Для такой системы существует несколько (нуль или больше) множеств выводимых предположений. Эти множества представляют различные картины мира, которые можно вообразить, исходя из теории с умолчаниями. 4.3. Логики умолчаний 229 4.3.2. Теории с умолчаниями Обозначим через 2 язык предикатов первого поряд- ка (разд. 2.2). Правило умолчания (сокращенно: умолчание} О) — это выражение вида а(х):^р,(х), .... Л^(х) у(х) где • a(x), pi(x), ..., рот(х) и у(х)— формулы язы- ка 2', свободные переменные у которых выбра- ны среди x==(JCi, .. . , Хп), • ос(х) называется требованием умолчания 3), pi (х) — обоснованием умолчания 3), t==l, ... ..., m. •y(x)— следствием умолчания 3), • М—некий символ метаязыка. Умолчание 3) называется замкнутым тогда и только тогда, когда а(х), pi(x), ..., рот(х) и у(х) не содер- жат свободных переменных. При этом можно исполь- зовать более простые обозначения: ос,, pi, ..., рот и у соответственно. Свободные переменные умолчания считаются V- квантифицированными. Область действия этих кван- торов простирается на все члены умолчания. Не- замкнутое умолчание называется открытым. Оно представляет общую схему вывода. Его конкретиза- цией является замкнутое умолчание, полученное за- меной всех свободных переменных открытого умолча- ния на константы языка 2 (с соблюдением неявного закона об области действия свободных переменных умолчания). Теория с умолчаниями А—это пара (D,F), где • D — множество умолчаний, • F—множество замкнутых формул из 2. Она называется замкнутой тогда и только тогда, когда все умолчания из D замкнуты. 4.3.3. Примеры применения умолчаний Для начала рассмотрим пример представления непол- ных знаний (этот пример заимствован из [88]). 230 4. Логика и модифицируемое рассуждения Пусть неполные знания представлены двумя умол- чаниями: • По-русски: "Человек обычно живет вместе со своей семьей'7 Логически: (Семья (х, у) Л (Живет (у) == г) : М Живет (х) = г)_________ Живет(х) ==z • По-русски: "Человек обычно живет в одном городе с нанимателем" Логически: Наниматель (х, г/)Л(Город (у)==г): М (Живет (х} == г)__________ Живет(х) == z Предположим, что супруг Мари живет в Брюсселе, а ее наниматель — в Париже. Два наших правила вы- вода дают два невыполнимых совместно заключения. Если сперва применить первое правило, то нужно вос- препятствовать всем выводам, приводящим к «Мари живет в Париже». «Мари живет в Брюсселе» и «Ма- ри живет в Париже» — два (невыполнимых совмест- но) расширения данной теории с вышеуказанными умолчаниями. Следующий пример [32] иллюстрирует возмож- ность использования умолчаний в иерархических структурах с исключениями. Утверждения: 1) моллюски являются раковинными, 2) головоногие — моллюсками, но не раковинными; 3) наутилусы — головоногими и раковинными представимы теорией А с двумя умолчаниями и трема формулами. „ _ Мо (х) : М (Ра (х} А -1 Го {х}} • Умолчание D[: ———-——„ ,.——————— Pa {x) По-русски: Если х — моллюск и выполнимо «х раковинный и не головоногий», то х раковинный. ,, п Го (х) : М (-} Ра (х) Л -1 На (х)) • Умолчание D^. —'———-^ р..——————— По-русски; Ееди х головоногий и вылол-нимэа «х не раковинный и не наутилус», •ЕЕ) х не раковинный. 4.3. Логики умолчаний. 231 • Формула Г; : Ул: (На (х) => Го (х)) По-русски: Наутилусы являются головоногими. •Формула Fz : VJC (fo (х) =э Мо (х)) По-русски: Головоногие являются моллюсками. • Формула Fs : Vn: (На (х) =з Ра (х)) По-русски: Наутилусы являются раковинными. Если х наутилус, то эти три формулы дают: «л: — го- ловоногий, моллюск и раковинный». Этот вывод опре- деляет единственное расширение данной теории объ- единением теории А и утверждения «х наутилус». Если х головоногий и не наутилус, то из формулы Рг следует: «х моллюск», а из правила Da следует: «х не раковинный». Этот вывод определяет единствен- ное расширение данной теории — объединение Л и утверждения «х головоногий и не наутилус». Формаль- ное определение расширения см. в § 4.3.4. 4.3.4. Расширения теорий с умолчаниями Теория с умолчаниями A=(D, F) подразумевает не- которое (нулевое или большее) число множеств пред- положений, которые выводимы с использованием мно- жества формул F, и удовлетворяет свойству выполни- мости. Эти множества предположений называются расширениями данной теории с умолчаниями. Расширения теории с умолчаниями явно определе- ны здесь лишь для замкнутых теорий. Открытую теорию можно преобразовать эффективным образом в замкнутую, заменяя каждое открытое умолчание мно- жеством всех его конкретизации, получаемых посред- ством применения открытых умолчаний к эрбрановой области (§ 1.2.9) данной теории. Используя это пре- образование, полученные для замкнутых теорий с умолчаниями результаты можно распространить на открытые теории (когда они конечны). Заметим, что теории, содержащие функциональные символы нену- левой арности, имеют бесконечную эрбранову об- ласть. Прежде чем приступать к формализации, охарак- теризуем интуитивно свойства, которыми должно 232 4. Логика и модифицируемые рассуждения обладать расширение замкнутой теории с умолчания- ми. Расширение—это надмножество основных сведе- ний системы, включающее все выводимое (по прави- лам классической логики и/или логики умолчаний). Пусть Х—подмножество из 3, Ths(X')— мно- жество замкнутых формул, общезначимо выводимых из Х по классическим правилам вывода из 3'. Thy {X) == [w \ w s 3, w замкнута и X 1— w}. Пусть A==(D, F}—теория с умолчаниями, S—под- множество в 3. Обозначим через Г(5) наименьшее подмножество в 3, удовлетворяющее следующим трем условиям: •F=r(S), • n^ns))-^), _ a'.MQi, ..., Мвгп г-> п/г.1 • если ——•• ——'—•— <= D, а (= Г (S) v • ' и -1р„ ..-, -Ifi^S, то у=Г(5). Множество формул Е s 3 является расширением, для А тогда и только тогда, когда Т{Е)==Е (т. е. Е—неподвижная точка оператора Г). Расширение Е можно охарактеризовать так. Строим последовательность формул Ei полагая Eo=F и ?,„==rA.(?,)u{Y ^^-.-^^Дили ae=?, и Пр„ .... П ^ ф Е} для t = О, 1, 2, ... . Множество Е есть расширение для А тогда и только тогда, когда 00 Е-[]Е,. i=.0 4.3.5. Примеры расширений теорий с умолчаниями Теория с умолчаниями иногда позволяет вывести не- сколько расширений из одного множества посылок. • Пример 1 [70]. л ^ ^ п ( :МА :МР : MQ\ Пусть A=(D, .F),rAeD=.j-=j-p-, —^> —i-sJ и F==0. 4.3. Логики умолчаний 233 Эта теория обладает расширением • E^Th^([-\P, -15}). • Пример 2. Пусть A==(D, F), где D - { 4^ I и /••=0. Эта теория не имеет расширений. в Пример 3 [70]. гг л /п ^ п (:МА :МВ\ Пусть A=(D, F), где D == •{ -=^-, -=^ ^ и /7==0. У этой теории два расширения: ?\ == Ths ({""l Л}) и E2==Ths-({~^B}). в Пример 4 [88]. • гг л /г> ^ г> ГЛ:Л^З^Р(л:) . Пусть Л = (D, F), где D = ^ ^JD^)—— : МЛ : Af П Л и F=. А 'ПЛ J " ---• Расширений два: ^1==:Г/^(ПЛ}) и ^=Г/г^({Л, ЭхР(х)}). Например, первым умолчанием из D можно формализовать «большинство профессоров уни- верситета имеет степень доктора»: Проф_унив (х) : М СЗу Конкр (у, доктор) А А Имеет {х, у)) __ Зг/ Конкр (г/, доктор) А Имеет (х, у) 4.3.6. Нормальные теории Как показывает пример 2 из § 4.3.5, некоторые теории с умолчаниями не обладают расширениями. Сущест- вование расширений гарантировано, если следствие и обоснование одного и того же умолчания совпадают [88]. Такие теории называются нормальными. Они 234 4. Логика и модифицируемые рассуждения состоят из нормальных умолчаний: а (х): МР (х) f»(x) Кроме интересного свойства допускать хотя бы одно расширение нормальная теория с умолчаниями обла- дает свойством полумонотонности: если увеличить множество умолчаний, то полученная теория допус- кает расширение, включающее какое-то расширение исходной теории [88]. Практически важное след- ствие этого свойства состоит в возможности построе- ния такой теории доказательств, в которой использо- ванные умолчания проявляются локальным образом. 4.3.7. Теория доказательств для нормальных теорий Можно ли построить теорию доказательств для логик умолчаний? В частности, для замкнутых нормальных теорий? Точнее, даны замкнутая нормальная теория А и замкнутая формула f из 2'. Существует ли метод проверки наличия для А расширения Е, содержаще- го /? Для получения ответа Рейтер [88] определил до- казательство в теории с умолчаниями следующим образом. Пусть Л = (D, F)—замкнутая нормальная теория и f—замкнутая формула из 3. Конечная по- следовательность Do, .. ., Dk конечных подмножеств из D есть доказательство для f в А тогда и только тогда, когда 1. F U {КС (Do).} Ь- f, 2. F U {КС (D;)} h- КТ (D.._i) для i == 1, 2, ..., k, 3. Dfe=0, 4. F U {КС (D,) | 0 < i < k} выполнимо, где KC(D;)— конъюнкция следствий и KT(D()— конъ- юнкция требований умолчаний из D,. Итак, доказательство есть последовательность под- множеств умолчаний. Его можно интерпретировать следующим образом. Первое подмножество {Dk) выбирается пустым. Последовательно строятся 4.3. Логики умолчаний 235 Dk-\, .. ., D], Do. Множество основных аксиом с до- бавленной к нему конъюнкцией следствий из всех умолчаний Do должно обеспечивать доказательство / классическим образом. Из построения подмножества D,_i вытекает, что множество F (с добавленной к не- му конъюнкцией следствий из D,) должно позволять доказывать классическим образом требования из D;_i и, следовательно, гарантировать применимость умолчаний из D,_i. Глобальная применимость всех умолчаний устанавливается проверкой выполнимости объединения F и конъюнкций следствий всех исполь- зованных умолчаний. Заметим, что в определении не говорится, как строить подмножества D„ и не приводится разрешаю- щей процедуры для используемого отношения дока- зательства (из классической теории предикатов пер- вого порядка). Более того, оно предполагает провер- ку выполнимости некой формулы из 3, тогда как множество замкнутых выполнимых формул из 3 не является рекурсивно перечислимым. Метод Рейтера [88] сочетается со свойством пол- ноты. Пусть f—замкнутая формула из 3. Нормаль- ная теория Л (замкнутая и выполнимая) обладает расширением Е (содержащим f) тогда и только тогда, когда f обладает доказательством в А. К сожалению, во всей общности проблема провер- ки существования расширения с данной замкнутой формулой не полуразрешима (§ 2.2.6). Это не столь неожиданно. Тем не менее в некоторых случаях она поддается практическому решению (особенно когда ограничиваются рамками высказываний). Можно определить особые теории с умолчания- ми, разрешимые с помощью метода полного доказа- тельства. Например, Бенар, Кинью и Кинтон [6] при- меняют метод насыщения, позволяющий реализовы- вать метод полного доказательства для разрешимых теорий, содержащих только так называемые «свобод- ные» умолчания: :MP(x}^R{x) 236 4. Логика и модифицируемые рассуждения 4.3.8. Полунормалькые теории Нормальные умолчания выглядят достаточно привле- кательными при представлении многих форм рассуж- дении. Свойства формальных систем, составляющих нормальные теории, особенно выигрышны в силу сле- дующих обстоятельств. Следствие и обоснование нормального умолчания совпадают. Следовательно, нормальные умолчания не- применимы, когда ложность их следствий доказана. Эти умолчания не могут вводить невыполнимости, опровергать обоснования из других ранее применен- ных нормальных умолчаний и своих собственных. Итак, нормальные теории полумонотонны, всегда об- ладают хотя бы одним расширением и представляют довольно простую теорию доказательств. Между тем в ходе применения нормальных умол- чаний могут возникать неприятные осложнения. В частности, взаимодействие различных нормальных правил может приводить к нежелательным заключе- ниям [89]. Поэтому иногда необходимо блокировать транзи- тивность между умолчаниями. Например, рассмотрим нормальную теорию A=(Z), F), где D содержит два нормальных умолчания: «обычно студент университета является взрослым», или в символьном виде: С (х}: MB (х) В(х) «обычно на работу берут взрослых», или в символь- ном виде: В (х): МП (х) П(х) и где F—множество из одного элемента {С (Эрик)}. Правила из D позволяют по умолчанию вывести, что студента университета взяли на работу. Это неже- лательный вывод. Осложнение предотвращается с по- мощью третьего нормального умолчания: «обычно студента не берут на работу». Таким образом, полу- чается нормальная теория &'=^(0\ F} где D'—мно- 4.3. Логики умолчаний 237 жество умолчаний: • ( С (х} : MB {х) В (x} : МП (х) \ В(х) ' П{х) С (х} : М -1 П (х) ) ~1 п (х) J • Для данного студента множество D' может дать два расширения теории А7 (соответствующих различной занятости студента): Thy ({С (Эрик). В (Эрик), ~[П(Эрик)}) и Thy ({С (Эрик), В (Эрик), П(Эрик)}). Тем не менее разумно потребовать блокирования транзитивности между двумя первыми правилами из D. Следовало бы также выделить априори расшире- ние, соответствующее ситуации, когда студента не при- нимают на работу. Это можно осуществить модифи- кацией второго правила: чтобы оно не могло быть применено в исключительном случае — «взрослый является студентом». Итак, для теории М' =(D", F), где D" есть • f С (x): MB (х) С (х) : М -1 П (х) \ В(х) ' ~ДП{х) В (х) : М {П (х) Л ~| С W) 1 П (х) ; • получаем желаемое расширение Т ha-({С (Эрик), В (Эрик), П П (Эрик)}). Третье умолчание D" полунормальное '[89], т. е. имеет вид а(х):М(р(х)Лу(х)) Р(х) Таким образом, полунормальное умолчание явно уп- равляется дополнительным условием в обосновании; Теория с полуормальными умолчаниями (полунор- мальная теория) не обязательно обладает расшире- нием. Она теряет некоторые достоинства нормальных теорий, в частности полумонотонность. 4.3.9. Наследственные системы с исключениями Системы сетевого и объектносо представлений часто позволяют выразить наследование свойств с исклю- 258 4. Логика и модифицируемые рассуждения чениями и встроить механизмы вывода, связанные с этими методами (§ 3.3.12). Поведение такой системы редко бывает корректным и полностью охарактеризо- ванным. Соответствующие методы довольно плохо освоены [НО], [29]. Если наследственные свойства между классами и подклассами можно относительно легко охарактери- зовать в классической логике (§ 3.3.11), то исследо- вание исключений требует ухищрений. Логика умол- чаний очерчивает естественные рамки для формали- зации систем представления знаний и рассуждении с исключениями. Между тем прямое обращение к теории с умолча- ниями (в частности, к нормальной) простым не яв- ляется. Наследственная система обеспечивает пере- дачу свойств по транзитивности (§ 3.2.19). Когда к системе добавляются исключения, транзитивность свойств должна допускать возможность блокирования. В литературе предложены различные формализмы систем представления с механизмами наследования свойств. • Можно использовать полунормальные умолча- ния [27], [29]. Исключения для наследования . свойств явно перечислены в умолчаниях. Эте- рингтон [29] определил подкласс полунормаль- ных умолчаний (связанных отношением зави- симости), для которых соответствующие полу- нормальные теории всегда обладают хотя бы одним расширением. Он предложил процеду- ру эффективного построения полунормальных теорий. • Можно использовать нормальные умолчания с неявным порядком, подчиненным иерархии мо- делируемой структуры [НО]. Можно не упо- минать явно исключения в умолчаниях. • Можно использовать таксономические теории с умолчаниями (не являющиеся ни нормальными, ни полунормальными). Они обладают един- ственными расширениями [33], [34]. 4 4. Модальные логики знания и веры 239 4.4. Модальные логики знания и веры 4.4.1. Введение Первейшей функцией модальной логики является фор- мализация модальностей «возможность» и «необхо" димость». Другое ее применение — моделирование и анализ парадигм «знание» и «вера». Для этого логи- ческие системы используют формальные языки с мо- дальными операторами «веры» и «знания». Системы сочетают различные схемы аксиом и правила вывода для формализации свойств этих операторов. Модаль- ные системы снабжены специфической семантикой. Различные модальные логики, которые мы рассмот- рим, являются расширениями логики первого поряд- ка. В частности, они заимствуют оттуда аксиомы, правила вывода и теоремы. .4.4.2. Некоторые элементарные модальные системы Ограничимся неквантифицированными частями мо- дальных языков с синтаксисом из § 3.1.14. Пусть 2— модальный язык высказываний, р и q — метаперемен- ные, представляющие формулы в языке 2. Модаль- ные операторы в 2 обозначим символами L и М (в модальной логике необходимости и возможности это D и О). Операторы общности L и существования М двойственны: L =s П М ~\. В логиках веры и знания оператор L принимает соответственно значения «предполагается» и «из- вестно». Значения оператора М — соответственно.. «противоположное не предполагается» и «противопо- ложное не известно». Нормальная модальная система — это четверка, состоящая из: • Множества всех теорем логики высказываний (разд. 1.1), область действия которых распрост- ранена на формулы модального языка выска- зываний 2'. • Схемы аксиомы дистрибутивности L{p =) q) =з (Lp =s Lq), 240 4. Логика и модифицируемые рассуждения обозначаемой буквой К. В соответствии с тол- кованием модальности «необходимость» схема К утверждает, что «если необходимо, что р вле- чет ц, то из необходимости р вытекает необхо- димость q». • Правила modus ponetis Р ?'=> Ч ч • Модального правила вывода необходимости р Lp («р необходимо истинно» при условии, что «р истинно»). Можно получить модальные системы и поизощ- реннее — обогащая нормальную модальную систему различными схемами аксиом, вроде нижеследующих: • Схема аксиомы знания Lp=>p. Ее обозначают буквой Т. По определению зна- ние — информация. Таким образом, схема Т ут- верждает: «то, что известно, — верно». Эту схему добавляют к нормальной модальной си- стеме, чтобы оператор L означал «известно». На- против, схемы Т не будет в системе аксиом, формализующих «предположение», ибо оно мо- жет быть ошибочным. Нормальная модальная система, пополненная схемой Т, перенимает имя от двух входящих в нее схем модальных аксиом: она обознчается че- рез КТ (иногда просто через ?7"). • Схема аксиомы, позитивной интроспекции: Lp => LLp. Она обозначается цифрой 4. Когда модальный оператор L означает «известно», то схема 4 утверждает: «если мне известно р, то я знаю, что известно р». Если же модальный оператор L означает «предполагается», то схема 4 гла- сит: «если я предполагаю, что р подтверж- 4.4. Модальные логики знания и веры 241 дается, то я предполагаю, что я предполагаю, что р подтверждается». Описанная схемой 4 возможность интроспек- ции нужна для формализации совершенного интроспективного интеллекта. Нормальная мо- дальная система, пополненная схемами аксиом Г и 4, обозначается К.Т 4 (или, в более класси- ческой манере, S4). • Схема аксиомы негативной интроспекции, Мр гз LMp. Она обозначается цифрой бив логиках знания и веры формализует совершенную негативную интроспекцию. Схема 5 эквивалентна такой: —! Lp :э L ~\ Lp. Когда оператор L означает «известно», то схема 5 утверждает: «если я не знаю, что р подтверждается, то я знаю, что я не знаю, что р подтверждается». Если же опе- ратор L означает «предполагается», то она гласит: «если я не предполагаю, что р под- тверждается, то я предполагаю, что я не пред- полагаю, что р подтверждается». Это свойство, конечно, чрезвычайно обремени- тельное. Оно выражает совершенное понима- ние пределов нашего знания или веры. Нор- мальная модальная система, пополненная схе- мами аксиом Г, 4 и 5, обозначается /СГ45 (или, в более классической манере, S5). Выбор модальной системы зависит от моделируе- мого понятия. Если хочется охарактеризовать знания разумного субъекта, обладающего совершенной спо- собностью к логической интроспекции относительно того, что «известно» и что «неизвестно», то следует выбрать модальную систему S5 (разд. 4.5). Если же- лательно моделировать предположения идеально разумного субъекта (некоторые предположения кото- рого могут оказаться ошибочными, но который обла- дает совершенной способностью к логической интро- спекции относительно того, что он предполагает и чего не предполагает), то лучше выбрать систему 242 4. Логика и модифицируемые рассуждения К45, называемую также слабой 85-системой (разд. 4.6). Каждая из этих различных модальных систем ин- дуцирует присущее ей синтаксическое отношение вы- водимости. Оно обозначается 1—s, где 5—имя рас- сматриваемой модальной системы. 4.4.3. Семантика возможных миров Модальность увеличивает выразительность классиче- ской логики и позволяет выявлять некоторые понятия с помощью специфических операторов. Семантический анализ модального выражения зависит от парамет- ров, неявно вносимых этими операторами. Например, выражения на языке временной логики используют модальные операторы с неявной переменной, отра- жающей временную эволюцию (§ 3.1.13). Формула йр эквивалентна формуле 1t:p(t). Семантический анализ этой формулы должен осуществляться с уче- том неявно подразумеваемого параметра t в модаль- ном операторе D. Для этого Крипке [60] ввел метод специфического семантического анализа: семантику возможных ми- ров. Модальная формула будет оцениваться в лоне некоего «универсума» различных «возможных миров» (§ 3.1.17). Точнее, анализ истинности некой модаль- ной формулы зависит от рассматриваемого возмож- ного мира. В примере с временной логикой различ- ные возможные миры представляют состояние мира в различных его конкретизациях. Некое «отношение доступности» свяжет эти возможные миры между со- бой и укажет последовательность различных момен- тов, в которые рассматривается мир. Опишем кратко эту семантику. Универсум W есть множество возможных миров, связанных отношением доступности R. Пусть а и b — два мира из универсума W, тогда факт доступности мира b после мира а обозначается aRb. Пара (W,R) называется структурой. Свойства отношения R инду- цируют различные схемы модальных аксиом, обще- значимых в рассматриваемой логике. Оценка У—это отображение из W X 3 в {И, Л}, которое для каж- 4.4. Модальные логики знания и веры 243 дого мира w из универсума W сопоставляет каждой пропозициональной константе из 3 определенное значение истинности. Тройка (W,R,7"} называется моделью. Для семантической оценки формул из 3 жела- тельно иметь в виду конкретный мир из универсума W вместе с рассматриваемой оценкой V. Рекурсивно определяют отношение семантического следования ^= между моделями и формулами языка. Запись (W, R, Т) \=y,f означает, что f истинно в мире w для модели (W, R, У). Основные правила следующие: •(r,^,r)h=„ и, •(W,R,r)\^--^ Л, • (W, R, r)KJ, если r(w, /)=И и /-пропо- зициональная константа из 3, • (W, R, r)\=^f^g, если (Г, R, Г)Ь=„/ только тогда, когда (W, R, Г)\=^,§, • (W, R, У) )==„,/,/, если для любого мира х уни- ; версума W при wRx имеем (W, R, У) |=;J. Смысл последнего правила: формула Lf подтверж- дается в мире w для некой модели (W, R, У), если формула / подтверждается во всех мирах универсума W, доступных из мира w. Оно учитывает желатель- ные значения модального оператора L. Действитель- но, в логике необходимого формула Lp представляет необходимость формулы р: «р необходимо в данном мире» интуитивно означает подтверждаемость р во всех мирах, доступных из данного. С другой стороны, в логике знания формула Lp означает «р известно» и, следовательно (интуитивно), что р подтверждается во всех возможных мирах, какие только можно во- образить на основе некоего множества знаний и предположений. Из двойственности M=s~\L~\ непосредственно вытекает правило • (W, R, Т) \=у, Mf,ecJiu существует мир х из уни- версума W, такой что wRx и (W, R, У)[=х1- Прежде чем заняться анализом истинности мо- дальной формулы в каждом из возможных миров, введем ряд понятий. 244 4. Логика ч модифицируемые рассуждения • Формула / из 3 общезначима в модели (W, R, У} тогда и только тогда, когда f подтверж- дается во всех мирах этой модели, т. е. если y(w,f) = И для всех миров w из W, или, в .символьной записи (W, R, T)\=f. • Формула / из 3 общезначима в структуре (W,R) тогда и только тогда, когда f общезна- чима в любой модели (W, R, У). Символьная запись выглядит так: (W, R} |= /. • Формула f из 3 общезначима тогда и только тогда, когда / общезначима в любой структуре (W,R). Символьная запись такова: [=f. Укажем на связь между семантическим отноше- нием |== и синтаксическим отношением г-. Сущест- вует соответствие между выбором схем основных аксиом данной формальной системы и свойствами отношения доступности между возможными мирами семантической характеристики этой системы. Можно показать, что конкретизации • схемы аксиомы дистрибутивности, т. е. схемы К, общезначимы, • схемы аксиомы знания (схемы Т) общезна- чимы в любой структуре с рефлексивным отно- шением доступности R, • схемы аксиомы позитивной интроспекции (схе- мы 4) общезначимы в любой структуре с тран- зитивным отношением доступности R, • схемы аксиомы негативной интроспекции (схе- мы 5) общезначимы в любой структуре с ев- клидовым 1) отношением доступности R. Из факта «f—формула Зч> доказуемо вытекают утверждения: • Y-к] тогда и только тогда, когда f общезначима в любой структуре, • I"" Krf тогда и только тогда, когда f общезна- чима в любой структуре с рефлексивным R, '> Отношение R называется евклидовым, если из aRb и aRc вы- текает ЬРс. 4.5. Немонотонные логики Мак-Дермотта 245 • \~KT4f тогда и только -тогда, когда / общезна- чима в любой структуре с рефлексивным и транзитивным R, • V^KTsf тогда и только тогда, когда f общезна- чима в. любой структуре с рефлексивным и ев- клидовым R. Структура возможных миров семантически харак- теризует различные модальные системы в зависи- мости от свойств отношения доступности. Например, если выбрать систему КТ45 (она же 55) для аксиоматизации свойств модального опера- тора L, то соответствующая семантическая характе- ризация будет состоять из множества возможных ми- роч, связанных между собой отношением доступности R, являющимся отношением эквивалентности. Как только что указывалось, R должно быть рефлексивно, транзитивно и евклидово (то есть отношением экви- валентности) . 4.5. Немонотонные логики Мак-Дермотта 4.5.1. Введение Немонотонные логики Мак-Дермотта и Доила [70], [71] отличаются от логики умолчаний Рейтера (разд. 4.3) в основном по следующим трем пунктам: • Рамки этих логик такие же, как и у модальных систем необходимости и возможности. • Предлагаемые логические системы не формали- зуют множество немонотонных правил, прису- щих данной области применения. Системы Мак-Дермотта и Доила являются универсаль- ными аксиоматическими системами. • Интересуются не построением отдельного рас- ширения теории, а присутствующими во всех ее расширениях формулами. Мак-Дермотт и Доил предложили изящный ме- тод, позволяющий избежать зацикливания при 'зада- нии правил немонотонного вывода (см. § 4.2.4). Они 246 4. Логика и модифицируемые рассуждения предложили неконструктивную характеризацию устой- чивых множеств взаимно выполнимых формул, не- монотонно выводимых из некоего набора посылок. Эти множества суть решения некоторого уравне- ния, являющиеся неподвижными точками и связан- ные с отношением выводимости, определяемым данной немонотонной системой. Соответствующая система может рассматриваться как классическая модальная аксиоматическая система, пополненная правилом вы- вода выполнимых утверждений. В настоящем разделе представим эту систему с критических позиций. Для начала уточним формаль- ный язык системы вывода, предложенной Мак-Дер- моттом (прежде чем представить и прокомментиро- вать ее первое описание). Вторая версия аксиомати- ческого описания этой системы позволит исключить зацикливание в определении немонотонного пра- вила 1). В заключение раздела будут очерчены до- стоинства и недостатки данного подхода. 4.5.2. Язык логики Мак-Дермотта Строим модальный язык первого порядка 3'. Он яв- ляется основанием немонотонной аксиоматической системы, подлежащей определению (см. также §§ 1.1.3 и 1.2.3). • Пусть 'ё', У, ST и У—множества символов ин- дивидных констант, переменных, функций и предикатов соответственно. • Множество термов из 3 определяется по ин- дукции следующим образом. Терм из 3 — либо константа из ^, либо переменная из Т, либо выражение fn{ti, ..., tn), где fn—n-ме- стная функция из У, t\, . . . , tn — термы из 2'. • Атомарная формула из Э — это выражение вида Pn{t\, ..., tn), где Рп—п-местный пре- дикат из У, a t\, .... tn — термы из 2. 1) Мы ограничимся подробным рассмотрением второй немонотон- ной логики Мак-Дермотта [71], которая лучше первой, оказав- шейся слишком слабой. 4.5. Немонотонные логики Мак-Дермотта 247 • Множество формул из 2 определяется по ин- дукции: формула из 2—либо атомарная фор- мула из 2, либо выражение (~1р), либо вы- ражение {p^)q), либо выражение Мр, либо выражение (\/v)p. Здесь р и q—формулы из 2, М—модальный оператор, и—переменная из Т. Будем использовать обозначения {р V q) для (П Р) =э q), (р А q) для -1 (Ц р) V П '?)), (Р = Ф Для ((р =з q) А (q =э р)), (3v)p для -1 ((Vo)(-1 р)) и Lp для —! М~\ р, а также обычные соглашения по исполь- зованию и опусканию скобок. Относящаяся к высказываниям часть языка 2 бу- дет в разд. 4.6 взята в качестве языка автоэпистеми- ческой логики. 4.5.3. Пример немонотонной аксиоматической системы Эта' немонотонная аксиоматическая система содер- жит три вида элементов: • «нелогические сведения», являющиеся форму- лами из 2 со статусом дополнительных ак- сиом, ® схемы логических аксиом, • логические правила вывода. Совокупность схем логических аксиом будет со- стоять из схем формул, аксиоматизирующих логику предикатов (см. разд. 1.2), а также из обсуждавших- ся в разд. 4.4 схем модальных, аксиом. Множество правил вывода будет содержать (кро- ме обычных правил: modus punens, универсального обобщения и модальной необходимости} специфиче- ское правило немонотонного вывода. Главная ценность исследований, проведенных Мак- Дермоттом, заключена в этом изящно сформулиро- ванном специфическом правиле. Какую модальную систему выбрать? Этот вопрос является поводом для дискуссии. К ней мы перейдем в разд. 4.6 — После представления автоэпистемической логики. 248 4. Логика и модифицируемые рассуждения Пусть Z. и М — двойственные модальные опера- торы. Рассмотрим следующие схемы и правила, где р, q и г—произвольные формулы из 2. 1. Схемы классических аксиом ([53], § 2.1.9): (а) р =э (q =э р), (Ь} (р =з (q => г)) =з ((р =) 9) =3 {р =) г)), (c) (-1 <7 =з -1 р) =з ((-1 9 =э р) =э a}^) =э (Lp =э Lq), (c) схема Баркан: ((Va) Lp} =з Z, (Va) р, (d) схема позитивной интроспекции: Lp ^з LLp, (e) схема негативной интроспекции: Мр =) LMp. 3. Правила вывода: (a) modus ponens: р, р => q }- q, (b) правило универсального обобщения: р\- (Va)/?, (c) правило необходимости: р I— Lp, {d) правило немонотонного вывода: "нельзя вывести ~1 р" \- Мр. Выбирая разные подмножества из списка схем модальных аксиом, получаем различные системы не- монотонного вывода. Система, включающая лишь две первые схемы, будет называться немонотонной ^-си- стемой. Системы, содержащие соответственно четыре первые модальные схемы и всю их совокупность, на- зовем немонотонной 54-системой и немонотонной 55-системой. Эти названия вполне соответствуют на- званиям модальных классических систем (разд. 4.4). Если из перечисленных немонотонных систем удалить правило немонотонного вывода, то получатся модаль- ные классические системы ST', 54 и 55. Сформулиро- ванное выше правило немонотонного вывода прием- лемым, вообще говоря, не является. Оно зацикливает определение отношения выводимости (§ 4.2.4). До 4.5. Немонотонные логики Мак-Дермотта 249 изложения способа решения этой проблемы отметим, что первоначальная формулировка правила немоно- тонного вывода хорошо высвечивает тройственную роль, предположительно им выполняемую: 1. Оно позволяет выводить, что некоторое утверж- дение возможно, т.е. выполнимо с точки зрения логики. Применяя его, можно вывести формулы вида Мр. Искомое значение для формулы Мр есть «р возможно» или же «р выполнимо». Для осуществимости этого надо, чтобы ~1 р не было выводимо, что обеспечивается проверкой усло- вия правила немонотонного вывода. Между тем для эффективной реализации этого приписанного модальному оператору М. значения надо, чтобы оно обладало свойствами модальных операторов, выраженными схемами модальных аксиом этой системы. .2. Оно косвенно позволяет принять как «.истин- ные-^ всего лишь выполнимые формулы. (На- пример, если Мр выведено по правилу немоно- тонного вывода и если в данной системе содер- жится дополнительная аксиома МР =з р, то по modus ponens можно вывести JO.) Применение этого метода означает также переход от конста- тации выполнимости некоего выражения к его утверждению. Данной системе присуща в не- котором смысле способность воспринимать как истинные формулы с установленной выполни- мостью. 3. Оно придает данной системе немонотонный характер. Например, если эта система позво- ляла вывести формулу Мр (или вообще фор- мулу <7, вытекающую из Мр) и если добавлена новая аксиома, позволяющая в этой системе вывести ~1р, то формулу q надо отвергнуть. Для решения проблемы зацикливания в определе- нии правила немонотонного вывода, а также пробле- мы характеризации множеств выводимых формул опишем неподвижные точки отображения системы вывода в множество посылок Л. Интуитивно эти не- 250 4. Логика и модифицируемые рассуждения подвижные точки представляют собой такие множе- ства формул, что никакую дополнительную (т. е. не входящую в рассматриваемое множество) формулу нельзя вывести с соблюдением свойства выполни- мости. Возьмем одну из аксиоматических систем вывода S) — немонотонную ^"-систему, либо немонотонную 54-систему, либо немонотонную 55-систему. Обозна- чим через соответствующую модальную классическую систему, получаемую удалением из 3) немонотонного правила (т. е. 5 есть либо У, либо 54, либо 55). Определим сначала Ths(A) как. множество формул из 3, выводимых в системе S из множества допол- нительных аксиом Л, т. е. Ths(A)={p^=^\Av-sp}. Итак, речь идет о множестве модальных теорем, мо- нотонно доказуемых в модальной классической си- стеме 5 с использованием множества посылок Л. Пусть В — подмножество формул из 2'. Обозна- чим через Нурд(В) множество формул, предположи- тельных относительно множества В (т. е. множество формул, выполнимых вместе с формулами из множе- ства В, но не доказуемых в модальной системе S с использованием множества посылок Л). Нурд{В)= {Mq \q ^ S? (q не имеет свободных переменных) и -1 q ф В} \ Ths (A). Нас интересуют такие множества В формул из S, которые являются неподвижными точками оператора Ths (A U Hyp A ( )), т. е. решениями рекуррентного уравнения B=Ths(A(]HypA(B)}. Правая часть этого уравнения есть множество всех модальных следствий, выводимых из объединения множества посылок Л и формул, предположительных относительно искомого множества В. Множество В является неподвижной точкой этого уравнения и на- зывается Немонотонным/,. Значит, оно устойчиво и 4.5. Немонотонные логики Мак-Дермотта 251 состоит из всех модальных следствий, выводимых из объединения множества дополнительных аксиом Л и множества формул, предположительных относительно этого Немонотонногод множества. Таким образом, решения приведенного выше ре- куррентного уравнения дают (неконструктивно опре- деляемые) максимальные множества формул, выводи- мых с использованием множества посылок А и с со- хранением свойства выполнимости. Эти множества содержат все логические следствия из множества по- сылок Л, а также все предположительные относи- тельно них формулы. Обозначим через THs{A) множество теорем, полу- чаемых в результате применения к множеству допол- нительных аксиом Л системы немонотонного вывода 2>, причем применение это осуществляется в соответ- ствии со следующим соотношением: THs(A)= 5'П(П Не монотонное л}. Таким образом, статус теорем придается формулам, принадлежащим всем неподвижным точкам из S). При отсутствии неподвижных точек THs(A) опреде- ляется как множество всех формул из 2'. В этом еще одно отличие от логики умолчаний, где «теоремами» были формулы из отдельной неподвижной точки (расширения) некоего множества умолчаний (см. разд. 4.3). Отношение немонотонной выводимости, соответст- вующее системе вывода 3), обозначается через [~ и определяется следующим образом. Пусть Qi и С?2 подмножества из 3. Имеем Qi ^sQz тогда и только тогда, когда Qs ^7V/s(Qi). Множество Qz формул становится с данного момента множеством теорем для множества посылок Qi, если и только если лю- бая формула из Qz принадлежат всем неподвижным точкам множества Qi. Как говорилось в разд. 4.2, эта логическая си- стема позволяет построить различные множества за- ключений (неподвижных точек) посредством варьи- рования порядка применения выводов. При этом бу- дет ноль, одна или больше неподвижных точек. 252 4. Логика ц модифицируемые рассуждения 4.5.4. Примеры Для иллюстрации изложенных выше понятий и поло- жений приведем два примера, взятых из [70]. • Пусть Л = {Мр =э ~} q, Mq=>~\ р}, где р и q—пропозициональные константы. У этого множества посылок две неподвижных точки — FI и Ft. Неподвижная точка Fi содержит ~1 р, но не включает ~1 q. Аналогично F-г содержит "~1 q, но не включает ~1 р. Действительно, если F\ не содержит ~\ q, то она содержит Mq, от- куда по правилу modus oonens с дополнитель- ной аксиомой Mq гз —! р вытекает, что она со- держит ~1 р. Подобное рассуждение можно применить и к F-г. •Пусть А=={Мр~^~Л р}. Неподвижных точек здесь нет. Действительно, если бы неподвиж- ная точ-ка не содержала ~~\ р, то она содержала бы Мр. Следовательно, она содержала бы ~1 р в противоречии с предположением. Если бы она содержала ~1 р, то содержала бы и Мр. Поэтому формула Мр => —! р была. бы выпол- нимой. Приходим к противоречию, ибо ~\ р и Мр не могут одновременно фигурировать в од- ном выполнимом множестве. 4.5.5. Ценность логики Мак-Дермотта Основная ценность немонотонной логики Мак-Дер- мотта заключена в методе неподвижной точки, ис- пользуемом для характеризации устойчивых мно- жеств заключений немонотонной системы, а также в применении модальной логики для формализации мо- дифицируемых рассуждении. Впрочем, выбор подходящей для рассмотрения мо- дальной системы остается проблематичным. Желая сопоставить модальному оператору М значение быть выполнимым, Мак-Дермотт заметил, что наиболее приемлемой модальной логикой является та, которая соответствует немонотонной 55-системе. Однако эта 4.6. Автоэпистемические логики 253 логическая система обнаруживает неожиданное свой- ство [71]: если Л|~д5/>, то A\-ssp. Иначе говоря, нет теоремы в немонотонной 55-си- стеме, которая не была бы теоремой в соответствую- щей монотонной классической системе 55. Мак-Дер- мотт подверг тогда сомнению полезность немонотон- ной 85-сислеиы и посоветовал (не приводя абсолютно убедительных аргументов) выбрать для формализа- ции немонотонности немонотонную 54-систему. В следующем разделе мы покажем, как можно пе- рестроить логику Мак-Дермотта, привлекая модели- рование идеально разумного субъекта, интроспектив- но рассуждающего об исходном множестве предполо- жений. Тогда удовлетворительно решится проблема выбора модальной системы. 4.6. Автоэпистемические логики 4.6.1. Введение Автоэпистемические логики имеют своим предметом формализацию интроспективных и идеально разум- ных рассуждении об исходном множестве предполо- жений. Они позволяют осуществить формализацию выражений вида: «если я не предполагаю, что р под- тверждается, то подтверждается <7». Под идеально разумными понимаются рассужде- ния, идеализированные в двух аспектах: можно выво- дить только ожидаемые логические следствия из ис- ходного множества предположений и все эти логиче- ские следствия надо принять во внимание. Таким образом, для рассуждении нужны неограниченные ресурсы. Подобные рассуждения немонотонны, ибо множе- ство основных предположений субъекта может со временем меняться, что чревато противоречиями для некоторых выводов. Такими интроспективными рас- суждениями можно моделировать многочисленные виды модифицируемых рассуждении (§ 4.2.6). 254 4. Логика и модифицируемые рассуждения Модальные логики знания и веры (разд. 4.4) под- ходят для формализации такого вида рассуждении. Они позволяют определить и аксиоматизировать различные эпистемические понятия (предположе- ние, знание, обоснованное знание и т. д.) и их свойства. Столнекер [103] и особенно Мур [78], [79], [80] развили основанный на модальной логике метод для формализации немонотонных, интроспективных и идеально разумных рассуждении. Эту автоэпистемическую логику можно рассмат- ривать как результат реконструкции немонотонной логики Мак-Дермотта (см. разд. 4.5), состоящей в за- мене парадигм выводимости и выполнимости на формализацию интроспективных способностей рас- суждений. В этом контексте модальный оператор М и двойственный ему оператор L формализуют соот- ветственно «обратное не предполагается» и «предпо- лагается» (вместо выполнимого и выводимого). Отметим, наконец, что автоэпистемическая логика и логики умолчаний (см. разд. 4.3) имеют одинако- вую формальную выразительность [57J, хотя их об- ласти применения могут быть различными. 4.6.2. Язык и семантика Рассматриваемый здесь язык Зр получается ограни- чением модального языка 2', описанного в § 4.5.2, на свою пропозициональную компоненту и использова- нием модального оператора L (двойственного М) для построения модальных формул. Формула вида Lq ин- терпретируется следующим образом: «предполагается, что q подтверждается». Назовем теорией множество формул языка Sp, автоэпистемической теорией — подмножество Т из Sp, представляющее какое-то полное и легальное множество предположений, которое идеально разум- ный субъект может построить на основе множества Л исходных предположений. Для начала уточним, ка- ковы семантические свойства, которыми должно об- ладать подобное множество формул Т. Для этого введем следующие определения [79]. 4.6. Автоэпистелшческие логики 255 • Интерпретация высказываний автоэпистемиче- ской теории Т приписывает значения истинно- сти формулам множества Т. Приписывание подчиняется классическим правилам оценки сложных формул логики высказываний. Оно придает произвольное значение истинности пропозициональным константам и формулам вида Lp («предполагается р»). • Модель высказываний автоэпистемической тео- рии Т—это интерпретация высказываний из Т, в которой подтверждаются все формулы тео- рии Т. • Автоэпистемическая интерпретация автоэписте- мической теории 7 — это интерпретация выска- зываний из Т, для которой всякая формула вида Lp подтверждается тогда и только тогда, когда р принадлежит Т. Таким образом, при автоэпистемической интерпретации формула Lp («предполагается р») подтверждается в том и только в том случае, если р принадлежит множеству Т предположений данного субъекта. • Автоэпистемическая модель автоэпистемиче- ской теории Т—это автоэпистемическая ин- терпретация, в которой подтверждается всякая формула из Т. Привьем на эти семантические рассмотрения понятия полноты и легальности (вместо выполнимости}, при- способленные к автоэпистемичности [79]. • Автоэпистемическая теория Т семантически полна тогда и только тогда, когда она содер- жит все формулы, подтверждающиеся во всех автоэпистемических моделях Т. (Интуитивно: Г полна тогда и только тогда, когда Т содер- жит все формулы, которые данному субъекту семантически позволено вывести в предположе- нии истинности всех его гипотез.) • Автоэпистемическая теория Т легальна относи- тельно множества Л основных предположений тогда и только тогда, когда любая автоэписте- 256 4. Логика и модифицируемые рассуждения мическая интерпретация Т, являющаяся мо- делью Л, является также и моделью теории Т. (Интуитивно: это позволяет гарантировать, что предположения некоего субъекта, составляю- щие автоэпистемическую теорию, истинны тогда и только тогда, когда истинны основные предположения из множества Л.) 4.6.3. Характеризация синтаксиса Посмотрим, как дать синтаксическую характериза- цию автоэпистемическим теориям Т, обладающим се- мантическими свойствами полноты и легальности от- носительно множества А исходных предположений. Ввиду трудности конструктивной характеризации множеств выводимости формул немонотонной систе- мы (проблема уже обсуждалась в §§4.2.3—4.2.4) да- дим неконструктивное определение автоэпистемиче- ских теорий Т, таких, что их максимальные и легаль- ные множества предположений идеально разумный субъект в состоянии построить на основе множества Л исходных предположений. В этом ключе будем говорить, что автоэпистемиче- ская теория Т устойчива, если Т есть множество фор- мул из Sp, удовлетворяющее следующим условиям: 1. Если {pi, ..., рп] = Т и [pi, . . ., рп} I- q (где \- представляет'отношение выводимости в логике вы- сказываний), то q е Т. 2. Если р е Т, то Lp <= Т. 3. Если р ф Т, то ~| Lp e Т. Первое правило утверждает, что мыслящий субъ- ект предполагает все логические следствия и уже предполагаемого (это обязательно, если требуем идеальной разумности субъекта). Второе правило га- рантирует, что формула «предполагается р» принад- лежит множеству Т предположений этого субъекта, если р — предположение этого субъекта. Последнее правило утверждает, что формула «р не предпола- гается» фигурирует в множестве Т предположений того же субъекта, если формулы р там нет. 4.6. Автоэпистемические логики 257 Двойственным образом определяется следующее понятие: автоэпистемическая теория Т называется теорией, основанной на множестве дополнительных аксиом Л, если все формулы из Т фигурируют среди тавтологических следствий из множества Л U (Lp I p e еЦи {-\Lp\p^T}. Справедливы следующие утверждения [79]: • Автоэпистемическая теория Т семантически полна тогда и только тогда, когда она устой- чива. • Автоэпистемическая теория Т легальна относи- тельно множества Л основных предположений тогда и только тогда, когда она основана на Л. Наконец, назовем устойчивым расширением мно- жества исходных предположений Л множество пред- положений Т, которое устойчиво и основано на Л. Устойчивые расширения являются максимальными легальными множествами предположений, которые идеально разумный субъект в состоянии вообразить на основе исходного множества предположений. 4.6.4. Анализ немонотонной логики Построенная Мак-Дермоттом теория немонотонного вывода обнаруживает некоторые странные особенно- сти, а именно: каждая теорема из немонотонной 55- системы является теоремой из монотонной системы 55 (§4.5.5). Этот факт можно объяснить, привлекая автоэпистемическую логику. Мак-Дермотт рассматри- вает неподвижные точки Т системы вывода своей не- монотонной логики, приложенной к множеству Л до- полнительных аксиом. Эти точки можно сравнить с максимальными легальными множествами предполо- жений идеально разумного субъекта. Определение Мак-Дермотта, ограниченное на про- позициональную компоненту, в сущности эквивалент- но следующему. ® Т является неподвижной точкой относительно Л тогда и только тогда, когда Т есть множе- ство модальных следствий (в системе 3==У 54 или 55) цзА[]{~\Ьр\р^Т}. 9 А. Тейз др. 258 4. Логика и модифицируемые рассуждения Правило немонотонного вывода позволяет вывести формулу вида Мр, если формула ~1 р не принадле- жит рассматриваемой неподвижной точке Т. Иначе говоря, опираясь на отношение двойственности между модальными операторами М и L, можно с помощью этого правила осуществить вывод формулы вида ~1 Ьр, если формула р не принадлежит рассматри- ваемой неподвижной точке. Но тогда в логике Мак- Дермотта неподвижная точка состоит из всех модаль- ных следствий из объединения множества формул Lp с указанной характеризацией и множества Л до- полнительных аксиом. Напротив, устойчивое расширение Т определяется следующим образом: • Т является устойчивым расширением Л тогда и только тогда, когда Т есть множество тавтологических следствий из A[j{Lp\p e Г}Ц \]{~ALp\p^T}. Легко заметить, что в определении неподвижной точки, данном Мак-Дермоттом, в совокупности аксиом нет (!) множества {Lp\p^T}. Myp [79] описывает природу этой неполноты следующим образом: «.при ввто-эпистемическом видении модального оператора L мыслящий субъект, использующий немонотонную ло- гику Мак-Дермотта, всеведущ относительно всего им не предполагаемого, но может полностью игнориро- вать им предполагаемое». В самом деле, он не вклю- чает в число аксиом формулы вида «я предполагаю, что р подтверждается», которые квалифицируют по- ложительные предположения субъекта. Теперь относительно того, что любая теорема не- монотонной 55-системы является теоремой в монотон- ной системе 55. Это можно объяснить следующи-м образом. Немонотонная 55-система содержит схему аксиомы знания, т. е. Lp гэ р (см. § 4.4.2). Для авто- эпистемического анализа немонотонности эта схема кажется слишком обременительной, так как она ут- верждает: «все, что предполагается, истинно». Это было бы приемлемо в логике знания, но не в логике веры. 4.6. Автоэпистемическис логики 259 Если мы хотим построить немонотонную систему, то использование логики знания представляется HP- ПОДХОДЯЩИМ.' Все выведенное не имеет больше стату- са общезначимого в классическом смысле, ибо есть возможность модификации. Это кажется трудно со- вместимым со схемой аксиомы, требующей истинно- сти всего предполагаемого. Поскольку ничто не позво- ляет выделить в системе Мак-Дермотта общезнаяи- мые утверждения и утверждения со статусом всего лишь выполнимых формул, эту схему аксиом, видимо, надо исключить. С другой стороны, немонотонная 55-система со- держит также схему аксиомы Мр =з LMp, применяя которую совместно со схемой аксиомы знания, можно обосновать предположение в любой формуле [79]. Следовательно, нет д-акой формулы, которая от- сутствовала бы во всех неподвижных точках множе- ства вспомогательных аксиом, получаемого с по- мощью немонотонной 55-системы. В частности, не су- ществует теоремы вида —! Lp (эквивалентной М ~1 р} ни в какой теории, базирующейся на немонотонной 55-системе, ибо такая теорема имела бы обоснова- ние, построенное с помощью правила немонотонного вывода из логики Мак-Дермотта. Myp [79] следую- щим образом толкует этот факт: «идеально разумный субъект, который предполагается не совершающим ошибок, склонен предполагать всё таким образом, что внешний наблюдатель не может сделать никаких вы- водов относительного того, что этот субъект не пред- полагает». Предлагается и еще один путь: не отвергать схему аксиомы Мр =з LMp, чтобы тем самым полу- чить немонотонную 54-систему, а лучше отбросить схему аксиомы знания Lp гз р, что приведет к немо- нотонной системе, основанной на модальной слабой Хб-системе1» (§ 4.4.2). Впрочем, Myp показал, что система вывода, со- держащая произвольное подмножество схем модаль- ных аксиом, присущих слабой 55-системе, дает всегда одни и те же устойчивые расширения (независимо от 0 Эта система иногда обозначается через /С45 [15]. 9" 260 4. Логика и модифицируемые рассуждения выбора указанного подмножества). Таким образом, автоэпистемическая логика может обойтись без явно- го упоминания схем модальных аксиом. 4.6.5. Семантика возможных миров Описанная в § 4.6.2 семантика автоэпистемической логики имеет то достоинство, что используя ее, можно характеризовать предположения субъекта, не ависи- мо от того, разумен он или нет. Между тем она ока- залась неудобной для использования, будучи некон- структивной в том смысле, что в ней нет правил, по- зволяющих оценивать предположения субъекта о сложных формулах исходя из его предположений и/или непредположений о составных частях формул. Это положение вещей вполне приемлемо для случая неразумного субъекта, ибо нельзя априори устано- вить никакой связи между его предположениями. На- против, предположения разумного субъекта подчи- няются неким отношениям, из которых можно попы- таться извлечь пользу. С этой целью Мур [78] предложил альтернативную семантическую характеризацию своей автоэпистеми- ческой логики. Эта новая семантика, основанная на понятии возможных миров, позволяет построить ко- нечные модели для автоэпистемических теорий. Она дает возможность доказать существование полных и легальных относительно некоторого множества по- сылок автоэпистемических теорий, что было бы труд- но осуществить с помощью первоначально указанной семантической характеризации. Основным результатом, на котором базируется эта новая характеризация, является следующее утвер- ждение: • Т есть множество формул, подтверждающихся во всех мирах 55-полной структуры (т. е. структуры (см. § 4.4.3) относительно системы 55, для которой любой возможный мир досту- пен из другого, неважно какого, возможного мира) тогда и только тогда, когда Т является устойчивой автоэпистемической теорией [78]. 4.6. Автоэпистемические логики 261 Таким образом, любая автоэпистемическая ин- терпретация Э устойчивой автоэпистемической теории Т может характеризоваться структурой Ж типа 55 и некой оценкой V. Структура возможных миров спе- цифицирует предположения идеально разумного субъ- екта, тогда как оценка определяет то, что действи- тельно подтверждается в реальном мире. Точнее, автоэпистемическая интерпретация 3f автоэпистемической теории Т есть пара 3 ==(Ж, У), где • Ж — 55-полная структура (представленная мно- жеством своих возможных миров, каждый из которых символизирован множеством подтверж- дающихся позитивных и негативных пропози- циональных констант), ® -У оценка истинности в реальном мире для про- позициональных констант из Зр. Автоэпистемическая теория Т является множе- ством всех формул, истинных во всех мирах из Ж. Рассмотрим пример автоэпистемической интер- претации У=(Ж, Т} с Ж ={{q, p}, [q, -I p}} и 'y==^p^q}. 55-полная структура УС составлена из двух возможных миров. В первом формулы q и р ис- тинны. Во втором истинны формулы q и ~~\ р. Оценка Т указывает, что р и q истинны в реальном мире. 3f—автоэпистемическая интерпретация автоэписте- мической теории Т, содержащей все формулы, истин- ные во всех мирах структуры Ж из У. В данном слу- чае Т сводится к единственной формуле q. 3 называется автоэпистемической моделью теории Т, составленной из множества формул, истинных во всех мирах из Ж, когда любая формула из Т под- тверждается в Э'. Второй результат дает средство проверки, являет- ся ли автоэпистемическая интерпретация У для Г автоэпистемической моделью для Т. 9 Если У == (Ж, У)—автоэпистемическая интер- претация для Т, то У является автоэпистемиче- ской моделью для Т тогда и только тогда, когда Т — элемент из Ж, что означает выполнимость 262 4. Логика и модифицируемые рассуждения оценки У вместе с данной оценкой, задаваемой в одном из возможных миров структуры Ж (т. е. что реальный мир—один из мирон, совмести- мых с предположениями данного субъекта) [78]. В нашем примере .У—автоэпистемическая модель для Т, ибо оценка У реального мира выполнима вместе с оценкой, заданной в первом возможном мире структуры Ж. Эти две теоремы интересны тем, что они индуци- руют метод проверки принадлежности формулы к устойчивому расширению исходного множества по- сылок. Напомним, что устойчивое расширение Т множе- ства Л основных предположений (посылок) есть ус- тойчивое множество предположений, основанное на А (§4.6.4). В силу первой теоремы, автоэпистемическая тео- рия Т устойчива, если ее можно представить 55-пол- ной структурой возможных миров. Чтобы автоэписте- мическая теория Т была устойчивым расширением, нужно еще, чтобы Т была основана на множестве Л исходных предположений (следовательно, чтобы Т была легальна относительно Л). Иначе говоря, любая автоэпистемическая модель посылок Л должна также быть и моделью для Т. В силу второй теоремы, оцен- ка реального мира каждой из этих автоэпистемиче- ских моделей посылок должна быть выполнимой вместе с оценкой в одном из возможных миров струк- туры Ж для автоэпистемической интерпретации. Таким образом, можно предложить разрешающую процедуру для автоэпистемической логики [80]. При- ведем один простой ее вариант. Пусть Л — множество посылок. 1. Строим все оценки, возможные для пропози- циональных констант, появляющихся в Л. Они будут характеризовать 55-полные структуры возможных миров языка для Л. 2. Выбираем структуры возможных миров, для ко- торых любая формула из Л подтверждается во всех мирах. 4.6. Авгоэпистемические логики 263- 3. Для каждой из этих структур Ж строим все автоэпистемические интерпретации (Ж, У), со- ответствующие всем оценкам У пропозицио- нальных констант, которые появляются в Л. 4. Проверяем для каждой автоэпистемической ин- терпретации (Ж, У) выполнение или невыполне- ние утверждения «любая формула из Л истинна в (Ж, У) тогда и только тогда, когда У пр-и- надлежит Ж». В случае выполнения Ж харак- теризует некое устойчивое расширение для Л. 5. Чтобы проверить принадлежность данной фор- мулы устойчивому расширению, представленно- му посредством Ж, выясняем, подтверждается ли эта формула в Ж. 4.6.6. Пример Пусть множество исходных предположений Л == == {~1 Lp =) а}. Оно содержит только одну формулу, означающую «если я не предполагаю р, то q под- тверждается». Докажем, что: • идеально разумный субъект, имеющий множе- ство исходных предположений Л, состоящее из одного элемента, получит устойчивое расшире- ние Г, содержащее высказывание q, но не р, • не может существовать ни устойчивого расшире- ния, содержащего р, но не q, ни устойчивого расширения, содержащего одновременно р и q. Предположим, что какое-то устойчивое расшире- ние Т для А содержит q, но не р. В этом случае 55-полной структурой, связанной с множеством пред- положений Т, будет Jf={{<7,p}, [q, ~\ р}}. (Эта струк- гура отражает два возможных мира: в первом под- тверждаются q и р, во втором—q и —!/?. Истинные формулы во всех мирах этой структуры соответствуют формулам, предполагаемым данным субъектом. Та- ким образом, Т — устойчивая автоэпистемическая теория.) Рассмотрим все автоэпистемические интерпрета- ции для Т Они составлены из структуры возможных 264 4. Логика и модифицируемые рассуждения миров, отражаюш.ей предположения данного субъек- та, и из произвольной оценки Т истинности в реаль- ном мире. В рассматриваемом языке лишь две про- позициональные константы; значит, оценок — четыре: {?.list(Vl,(),_), ['.'I, list (V2,Ves,Long).{Ves=—Long, Val= VI +V2}. list (Val.Ves, Long)— —> bit(Val,Ves), {Long == 1}. list (Val.Ves,Long)--> bit (VI, PI). list(V2,Ves,Ll), {Pl=Ves+H, Val=Vl +V2, Long == LI + 1}. bit(0,_)-->10],{!}. bit(Val,Ves)--> II], {!,Val=2 Ves}. s(N):-number (Val,N,[ ]),write (Val),nl.X is Val, write (X). Последнее выражение печатает результат сперва в форме исполнимого терма, а затем— в чисто число- вом виде: ?- s([l,0 1]). 2~(0 + (1 + 1)) + (0 + 2-0) 5 — — > да ?- s([l,0,'.',0,l,0]). 2'~(0 + 1) + 0 + (0 + (2"(- (1 + 1 + 1) + 1) + +0)) 2.25 ——>да У первоначальной цели s( [1,0,1]) первая подцель number (Val,[l, 0,11,[ ]). Она требует синтаксического анализа списка битов при унификации переменной Val с термом 2-(0+(!+!))+(О+2-0), после чего терм печатается. Затем он выполняется для присваивания Х значения 5. Если в БД заменить == на is, то получим сообще- ния об ошибках. Действительно, исполнимый терм будет получен лишь по завершении анализа входного списка. Многократные проходы по синтаксическому дереву Пролог заменяет последовательностью под- унификаций. Усовершенствование (обещанное) БД Литература 411 выглядит следующим образом: /* кнут */ number (Val)— —> list(Val,0,_). number(Vl + V2)——> list(Vl,0,_),['.'], list (V2, —Long, Long). list (Val,Ves,1)- -> bit(Val.Ves). list(Vl +V2, Ves, Long +1)——> bit(Vl, Ves + Long), list(V2, Ves, Long). bit(0._)--> [0],{!}. bit(2"Ves,Ves)——> [!],{!}. s(N):—number (Val, N,[ ]), write (Val), nl, X is Val, write (X). Литература 1. Abadi M. and Manna Z. Modal theorem proving. In: Proc. 8th Int. Conf. on Automated Deduction (J. H. Siekmann, ed.), L'NCS 230, Springer Verlag-, Berlin, pp. 172—189, juillet 1986. 2. Ait-Kaci H. and Nasr R. LOGIN: A logic programming with built-in inheritance, J. Logic Programming, vol. 3, no. 3, pp. 185—215, octobre 1986. 3. Barwise J. Handbook of Mathematical Logic, North-Holland., Amsterdam, 1974. Имеется перевод: Барвайс Дж. (ред.) Спра- вочная книга по математической логике.—M.: Наука, 1982 (1—3), 1983 (4). 4. Bates M. The theory and practice of augmented transition network grammars. In: Natural Language Communication With Computers (L. Bole, ed.), pp. 191—259, Lecture Notes in Computer Science, Springer-Verlag, Berlin, vol. 63, 1978. 5. Bell J. L. and Machover M. A Course in Mathematical Logic, North Holland, Amsterdam, 1977. 6. Besnard P., Quiniou R. and Quinton P. A theorem prover for a decidable subset of default logic, PFOC. AAAI-83, pp. 27—30, 1983. 7. Besnard P. and Siegel P. The preferential models approach to non monotonic logics In: Non-Standard Logics for Auto- mated Reasoning (P.' Smets et al., eds.). Academic Press, London, 1988, p. 137—161. 8. BobrotV D. and Winograd T. An overview of KRL, a know- ledge representation language. Cognitive Science, vol. 1, pp. 3—46, 1977. 9. Brachman R. J., Fikes R. E. and Levesque H. J. KRYPTON: Integrating terminology and assertion. Proc. AAAI-83, pp. 31—35, 1983. 10. Br-achman R. J. and Levesque H. J. (eds.). Readings in Know- ledge Representation. Morgan Kaufmann, Los Altos, 1985. 11. Bratko I. Prolog Programming for Artificial Intelligence, Addison Wesley, Reading, M. A. 1986. Имеется перевод: 412 Литература Братко И. Программирование на языке Пролог для искус- ственного интеллекта.—;М.: Мир, 1990. 12. Ceccato S. Linguistic Analysis and Programming for Mecha- nical Translation, Gordon and Breach, New York, 1961. 13. Chang С. С. and Keisler H. J. Model Theory, North Holland, Amsterdam, 1973. Имеется перевод: Кейслер Г., Чен Ч. Тео- рия моделей.—М.: Мир, 1977. 14. Chang С. L. and Lee R. С. Т. Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973. Имеется перевод: Чень Ч., Ли Р. Математическая логика и автомати- ческое доказательство теорем.—М.: Наука, 1983. 15. Chellas В. F. Modal Logic: an Introduction, Cambridge Uni- versity Press, Cambridge, 1980. 16. ChomsKy N. On certain formal properties of grammars. In- formation and Control., vol. 2, no. 2, pp. 137—167, 1959. Имеется перевод: Хомский H. О некоторых формальных свойствах грамматик.—В кн.: Киберн. сб., вып. 5,—М.: ИЛ, 1962, с. 279—311. 17. dark К. L. Negation as Failure: In: Logic and Data Bases (N. Gallaire et J. Minker, eds.), Plenum Press, New York, pp. 293—322, 1978. . 18. Clocksin W. F. and Mellish C. S. Programming in Prolog (2-eme ed.). Springer-Verlag, Berlin, 1984. Имеется перевод: Клоксин У., Меллиш К. Программирование на языке Про- лог.—М.: Мир, 1987. 19. Colmerauer A., Kanoui H., Roussel P. et Pasero R. Un Sys- teme de Communication Homme-Machine en Francais, Groupe de Recherche et Intelligence Artificielle, Universife d'Aix-Mar- seille, 1973. 20. Colmerauer A. Metamorphosis grammars. In: Natural Lan- guage Communication with Computers (L. Bole, ed.), pp. 139—169, Lecture Notes in Computer Science, vol. 63, Springer-Verlag, Berlin, 1978. 21. Colmerauer A., Kanoui H. et Van Caneghem M. Prolog, bases theoriques et developpements actuels, T. S. I., vol. 2, no. 4, 1983. Имеется перевод: Колмероэ А., Кануи А., ван Кане- гем М. Пролог — теоретические основы и современное раз- в'итие.—В сб.: Логическое программирование.—М.: Мир, 1988, с. 27—133. 22. Davio М., Deschamps J. P., Thayse A. Discrete and Switching Functions, McGraw-Hill, New York, 1978. 23. Davis M. Computability and Unsolvability, McGraw Hill, New York, 1958. 24. Dijkstra E. W. A Discipline of Programming, Academic Press, New York, 1976. Имеется перевод: Дейкстра Э. Дисциплина программирования.—М.: Мир, 1978. 25. Dowling W. and Gallier J. H. Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. of Logic Programmnig, vol. 1, 1984. 26. Doyle J. A truth maintenance system. Artificial Intelligence, vol. 12, no. 3, pp. 231—272, 1979. Имеется перевод: Литература 413 Доил Дж. Система поддержания истинности. — В кн.: Ки- берн. сб., вып. 20,—М.: Мир, 1983, с. 159—215. 27. Etherington D. W. and Reiter R. On inheritance hierarchies with exceptions, Proc. AAAI-83, pp. 104—108, 1983. 28. Etherington D. W., Mercer R. E. and Reiter R. On the ade- quacy of predicate circumscription for closed-world reasoning, Proc. AAAI-Workshop on Non-Monotonic Reasoning New Paltz, New York, pp. 70—81, octobre 1984. 29. Etherington D. W. Formalizing nonmonotonic systems. Artifi- cial Intelligence, vol. 31, no. 1, pp. 41—85, janvier 1987. 30. Even S., Itai A. and Shamir A. On tlie complexity of time- table and multicommodity flow problems SIAM J Comput vol. 5, pp. 691 703, 1976. 31. Fikes R. and Kehler T. The role of frame-based representa- tion in reasoning, Comm. ACM, vol. 28, no. 9, pp. 904—920, septembre 1985. 32. Froidevaux С. JSA hierarchies with exceptions, Proc. 5 ieme Congres AFCET Reconnaissance des Formes et Intelligence Artificielle, Grenoble, pp. 1127—1138, 1985. 33. Froidevaux С. Taxonomic default theory, Proc. ECAI-86, pp. 123—129, Brighton, juillet 1986. 34. Froidevaux С. and Kayser D. Inheritance in semantic net- works and in default logic, In «Non-Standard Logics for Automated Reasoning» (P. Smets et al., eds.). Academic Press, London, 1988. 35. Gabbay D. M. Theoretical foundations for non-monotonic rea- soning in expert systems. Research Report 84/11, Departa- ment of Computing, Imperial College, London, 1984. 36. Garey M. R. and Johnson D. S. Computers and Intractability; A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979. Имеется перевод: Гэри М., Джонсон Д. С- Вычислительные машины и труднорешаемые задачи —М: Мир, 1982. 37. Gregoire E. Raisonnement plausible: inference non mono- tone et logiques autoepistemiques, Proc. Int. Conf. on In- formation Processing and Management of Uncertainty in Knowledge-Based Systems, Paris, pp. 376—379, juillet 1986. 38. Gregoire E. A note on Moore's autoepistemic logic. In: «Non- Standard Logics for Automated Reasoning» (P. Smets et al., eds.). Academic Press, London, 1988, p. 132—133. 39. Gries D. The Science of Programming, Springer-Verlag, Ber- lin, 1981. Имеется перевод: Грис Д. Наука программирова- ния.—М.: Мир, 1984. 40. Halpern J. Y. and Moses Y. Towards a theory of knowledge and ignorance: Preliminary report, Proc. AAAI-Workshop on Non-Monotonic Reasoning, New Paltz New York pp 125— 143, octobre 1984. 41. Halpern J. Y. and Moses Y. A guide to the modal logics of knowledge and belief: Preliminary draft, Proc. IJCAI-85, pp. 480—490, 1985. 42. Halpern J. Y. (ed.) Proc. Conf. on Theoretical Aspects of 414 Литература Reasoning about Knowledge, Morgan Kaufmann, Los Altos, 1986. 43. Hayes P. J. In defense of logic, Proc. IJCAI-77, pp. 428— 433, 1977. 44. Hayes P. J. The logic of frame. In Frame Conceptions and Text Understanding (D. Metzing, ed.), de Gruyter, Berlin, pp. 46—61, 1979. 45. Heeffer A. (ed.) Non-classical logics !or expert systems, CC-AI, vol. 3, no. 1—2, 1986. 46. Hintikka J. Knowledge and Belief: an Introduction to the Logic of the Two Notions, Cornell University Press, Ithaca, New York, 1962. 47. Hintikka J. Impossible possible worlds vindicated, J. Philo- sophical Logic,, vol. 4, pp. 475—484, 1975. 48. Hobbs J. R. and Moore R. C. (eds.) Formal Theories of the Commonsense World, Ablex, Norwood, 1985. 49. Hopcroft J. and Ullman J. Introduction to Automata Theory, Languages and Computation, Addison-Wesley, Reading, MA, 1979. 50. Hughes G. E. and Cresswell M. J. An Introduction to Modal Logic, Methuen, London, 1972. 51. Israel D. J. What's wrong with non-monotonic logic? Proc. AAAI-80, pp. 99—101, 1980. 52. Israel D. J. A short companion to the naive physics mani- festo. In: Formal Theories of the Commonsense World (J. Hobbs et R. C. Moore, eds.), pp. 427—447, Ablex, Nor- wood, 1985. 53. Kleene S. C. Introduction to Metamathematics, North-Hol- land, Amstredam, 1952. Имеется перевод: Клини С. Введе- ние в метаматематику.—M.: ИЛ, 1957. 54. Kleene S. С. Mathematical Logic, Wiley, Chichester, 1967. Имеется перевод: Клини С. Математическая логика. — M.: Мир, 1973. 55. Knuth D. Semantics of context-free languages, J. Math. Syst. Theory, vol. 2, pp. 127—146, 1968. 56. Konolige К. A deduction model of belief and its logics, De- partment of Computer Science, Report STAN-CS-84-1022, Stanford, San Francisco, 1984. 57. Konolige К. On the relation between default theories and autoepistemic logic, Proc. IJCAI-87, Morgan Kaufmann, pp. 394—401, 1987. 58. Kowalski R. Logic for Problem Solving, North-Holland, New York, 1979. 59. Kramosil I. A note on deduction rules with negative premises, Proc. IJCAI-75, pp. 53—56, 1975. 60. Kripke S. A. Semantical considerations on modal logic. In: Reference and Modality (L. Linsky, ed.), Oxford University Press, London, pp. 63—72, 1971. 61. Levesque H. J. The interaction with incomplete knowledge bases: a formal treatment, Proc. IJCAI-88, pp. 240—245, 1981. 62. Levesque H. J. A logic of implicit and explicit belief. Proc. AAAI-84, pp. 198—202, 1984. Литература 415 63. Lloyd J. W. Foundations of Logic Programming Springer- Verlag, Berlin, 1984. 64. Lukasiewicz J. Many-valued systems of prepositional logic. In: Polish Logic (S. McCall, ed.), Oxford University Press, Oxford, 1967. 65. Manna Z. Mathematical Theory of Computation, McGraw-Hill, New York, 1974. Имеется перевод гл. 5: Манна 3. Теория неподвижной точки программ. — В кн.: Кибернетический сборник, вып. 15,—M.: Мир, 1978, с. 38—100. 66. Marchal В. Modal logic: a brief tutorial. In: Non-Standard Logics for Automated Reasoning (P. Smets et al., eds.), Academic Press, London, 1988. 67. McCarthy J. Epistemological problems of artificial intelli- gence, Proc. IJCAI-77, pp. 1038—1044, 1977. 68. McCarthy' J. Circumscription: a form of non-monotonic rea- soning, Artificial Intelligence vol. 13, no. 1—2 pp. 27—39, 1980. 69. McCartny J. Applications of circumscription to formalizing Commonsense knowledge, Artificial Intelligence, vol. 28, no. 1, pp. 89—121, 1986. 70. McDermott D. and Doyle J. Non-monotonic logic I, Artificial • Intelligence, vol. 13, no. 1—2, pp. 41—72, 1980. 71. McDermott D. Non-monotonic logic II: non-monotonic modal theories, J. ACM. vol. 29, no. 1, pp. 34—57, 1982. 72. Mendelson E. Introduction to Mathematical Logic (2-eme ed.). Van Nostrand, Princeton, 1979. Имеется перевод пер- вого издания: Мендельсон Э. Введение в математическую логику.—M.: Наука, 1976. 73. Minsky M. L. Computation: Finite and Infinite Machines, Prentice-Hall, Englewood Cliffs, NY, 1967. Имеется перевод: Минский M. Вычисления и автоматы.—M.: Мир, 1971. 74. Minsky M. L. A framework for representing knowledge. In: The Psychology of Computer Vision (P. Winston, ed.), McGraw-Hill, New York, pp. 34—57, 1974. Имеется перевод: Минский M. Структура для представления знания.— В сб. Психология машинного зрения.—M.: Мир, 1978, с. 249— 338. 75. Moisil G. Essai sur les Logiques поп Chrysippiennes, Edi- tions de L'Academie de la Republique Socialiste de Romanic, 1972. 76. Montague R. The proper treatment of quantification in ordi- nary English. In: Formal Philosophy: Selected Papers of Ri- chard Montague (R. H. Thomason, ed.), Yale University Press, London, 1974, pp. 188—221. 77. Moore R. C. The role of logic in knowledge representation and Commonsense reasoning, Proc. AAAI-82, pp 428—433 1982. 78. Moore R. C. Possible-world semantics for auto-epistemic lo- gic, Proc. AAAI-Workshop on Non-Monotonic Reasoning, New Paltz, New York, pp. 344—354, octobre 1984. 79. Moore R. C. Semantical considerations on non-monotonic logic, Artificial Intelligence, vol. 25, no. 1, pp. 75—94, 1985. 416 Литература 80. Moore R. С. Autoepistcmic logic. In: Non Standard Logics for Automated Reasoning (P. Smets et al., eds.). Academic Press, London, 1988, p. 105—136. 81. Murray N. Completely non-clausal theorem proving, Artifi- cial Intelligence, vol. 18, pp. 67—86, 1982. 82. Newell A. The knowledge level, AJ Magazine, vol. 2, no. 2, pp. 1—20, 1980. 83. Nilsson N. Principles of Artificial Intelligence, Tioga Publi- shing Company, Palo Alto, CA, 1980. Имеется перевод: Ниль- сон Н. Принципы искусственного интеллекта. — М.: Радио и связь, 1985. 84. Pereira F. and Warren D. Definite Clause grammar for language analysis—A survey of the formalism and a com- parison with ATN, Artificial Intelligence, vol. 13, pp. 231— 278, 1980. 85. Putnam H. The analytic and the synthetic. In: Mind, Lan- guage, and Reality (H. Putnam, ed), Cambridge University Press, Cambridge, "pp. 33—69, 1962. 86. Quine W. V. Methods of Logic, Henry Holt, New York, 1950. 87. Reiter R. On closed-world data base. In: Logic and Data Bases (H. Gallaire and J. Minker, eds.), Plenum Press, New York, pp. 55—76, 1978. 88. Reiter R. A logic for default reasoning, Artificial Intelli- gence, vol. 13, no. 1—2, pp. 81—131, 1980. 89. Reiter R. and Criscuolo G. On interacting defaults, Proc. IJCAI-81, pp. 270—276, 1981. 90. Reiter R. Circumscription implies predicate completion (some- times), Proc. AAAI-Workshop on Non-monotonic Reasoning, New Paltz, New York, pp. 418—420, octobre 1984. 91. Rescher N. Many-valued Logic, McGraw-Hill, New York, 1969. 92. Rich E. Artificial Intelligence, McGraw-Hill, New York, 1983. 93. Robinson J. A. A machine-oriented logic based on the resolu- tion principle J. ACM, vol. 12, no. 1, pp. 23—41, 1965. Име- ется перевод: Робинсон Дж. А. Машинно-ориентированная логика, основанная на принципе резолюции. — В кн.: Ки- бернетич. сб., нов. сер., вып. 7—М.: Мир, 1970, с. 194—218. 94. Robinson G. and Wos L. Paramodulation and theorem-prov- ing in first-order theories with equality. Machine Intelligen- ce 4, Edinburgh University Press, Edinburgh, pp. 135—150, 1969. 95. Robinson J. A. Logic: Form and Function, Edinburgh Univer- sity Press, Edinburgh, 1979. 96. Rogers H. Theory of Recursive Functions and Effective Com- putability, McGraw-Hill, New York, 1967. Имеется перевод: Роджерс X. Теория рекурсивных функций и эффективная вычислимость.—М.: Мир, 1972. 97. Sandewall E. An approach to the frame problem and its implementation. In: Machine Intelligence 7 (В. Meltzer and D. Michie, eds.), Wiley, New York, pp. 195—204, 1972. 98. Schank R. and Abelson R. Scripts, Plans, Goals and Under- standing, Lawrence Eribaum Associates, New York, 1977. 99. Schoenfield J. R. Mathematical Logic, Addison-Wesley, Read- Литература 417 ing, MA, 1967. Имеется перевод: Шенфилд Дж. Магемати- ческая логика.—М.: Наука, 1975. 100. Smcts Ph., Mandani E. H., Dubois D. and Prade N. (eds.) Non-Standard Logics for Automated Reasoning, Academic Press, London, 1988. 101. Snyers D. and Thayse A. From Logic Design to Logic Pro- gramming, Lecture Notes in Computer Science, vol. 271, Springer-Verlag, Berlin, 1987. 102. Sowa J. Conceptual Structures, Addison-Wesley Reading MA, 1984. 103. Stalnaker R. A note on non-monotonic modal logic, Note non publiee, Dept. of Philosophy. Coinell University, Ithaca, New York, juin, 1980. 104. Stefik M. and Bobrow D. G. Object-oriented programming: themes and variations, AI Magazine, vol. 6, no 4 pp 40— 61, 1986. 105. Sterling L. and Shapiro E. The Art of Prolog, MIT Press, Cambridge, MA, 1986. Имеется перевод: Стерлинг Л., Шапи- ро Э. Искусство программирования на языке Пролог. — М.: Мир, 1989. 106. Thayse A. Meet and join deratives and their use in switching theory, IEEE Trans. Computers, vol. C-27, pp. 713—720, 1978. 107. Thayse A. Implementation and transformation of algorithms based on automata, Philips J. of Research, vol. 35 pp 190— 216, 1980. 108. Thayse A. P. Functions and Boolean Matrix Factorization, Lecture Notes in Computer Science, vol. 175, Springer-Verlag 1984. 109. Tison P. Generalisation of consensus theory and application to the minimization of Boolean functions, IEEE Trans Electr. Comput., vol. EC-5, pp. 126—132, 1967. 110. Touretzky D. S. The Mathematics of Inheritance Systems, Re- search Notes in Artificial Intellingence, Pitman, London 1986 111. Turner R. Logics for Artificial Intelligence, Ellis-Horwood, Chichester, 1984. 112. Winograd Т. Language as a Cognitive Process, Vol. 1: Syn- tax, Addison-Wesley, Reading, MA, 1983. 113. Winston P. and Horn B. LISP (2-eme ed.), Addison-Wesley Reading, MA, 1984. 114. Woods W. Transition network grammars for natural language analysis. Cpmm. ACM, vol. 13, No. 10, pp. 591—606. Octobre 1970. Имеется перевод: Вудс В. А. Сетевые грамматики для анализа естественных языков. — В кн.: Киберн сб вып. 13,—М.: Мир, 1976, с 120—158. 115. Woods W. Cascaded ATN grammars, American J. Computa- tional Linguistics, vol. 6, no. 1, 1980. Предметный указатель Абстракция-^, (abstraction-^,) 161 Автомат детерминированный (automate deterministe) 303 — конечный (atomate fini) 128, 303 — недетерминированный (auto- mate поп deterministe) 303 — стековый (automate a pile) 305 — — детерминированный (au- tomate a pile deterministe) 308 Автоэпистемическая интерпре- тация (interpretation autoepis- temique) 255, 261 —логика (logique autoepistemi- que) 227, 253 — модель (modele autoepiste- •miqiie) 255, 261 — теория легальная (theorie autoepistemique legale) 255 — — -основанная (theorie au- toepistemique fontfee-) 257 — — полная (theorie antoepis- •temique .complete) 2S5 — — -устойчивая (4h'eorie au- toeprstemique etabte) 256 Аксиома (axiome) 113 Аксиоматическая система (sys- teme axiomatique) '92 — — немонотонная (systeme axiomatique non monotone) 2-47 Алгебра булева (algebre de Boole) 29 Алгоритм (algorithme) 125 — Девиса и Патнема (algo- rithme de Davis et Pu.tn.am} 33 — Куайна (algorithme de Qui- ne) 24, 83 — редукции (algorithme de re- duction) 26 — унификации (algorithme d'unification) 357 Алгоритмы Пролога (algorith- mes de Prolog) 351 Алетическая логика (logique alethique) 152 Антисимметричность (antisy- metrie) 28 Ассоциативность (associativite) 28 ATOM (atome) 59 Атрибут (attribut) 198 Ввод-вывод в Прологе (ent- ree-sortie Prolog) 384 Возврат (retour en arriere) 299, 343 Вопрос (question) 293, 337, 353 Временная логика (logique tem- porelle) 153 Вывод (inference) 103 — немонотонный (inference non monotone) 248 Выражение-Х (expression-^,) I61 — тело (corps d'une expres- sion-^) 162 Высказывание (proposition) 11 'Гипотеза (hypothese) 21 Грамматика атрибутная (gram- maire attribuee) 407 —контекстно-свободная (gram- maire hors-contexte) 49, 270, 305, 399 — определенных дизъюнктов (grammaire DCG) 278, 279, 283, 290, 330, 407 — регулярная (grammaire re- guliere) 305 —— структуры фразы (grammai- re a structure de phrase) 300 — Хамского (grammaire de Chomsky} 300 — — типа 0 (grammaire de Chomsky de type 0) 311 Предметный указатель- 419' — — типа 1 (grammaire de Chomsky de type 1) 310 — — типа 2 (grammaire de Chomsky de type 2) 305 — — типа 3 (grammaire de Chomsky de type 3) 300 Граф канонический (graphe ca- nonique) 181 — концептуальный (graphe con- ceptuel) 169 Дедукции метатеорема (metat- heoreme de la deduction) 96 — принцип (principe de deduc- tion) 22 Дедукция обратная (deduction inverse) 167 — прямая (deduction directe) 166 Деонтическая логика (logique deontique) 152 Дерево-И/ИЛИ (arbre ET/OU) 296 — семантическое (arbre seman- tique) 23 — — полное (arbre semantique complet) 23 — синтаксическое (arbre synta- xique) 274, 329 Диаграмма переходов (dia- gramme de transition) 303 — состояний (diagramme d'e- tat) 303 Дизъюнкт (clause) 30, 72 — резольвентный (clause re- solvante) 86 — хорновский (clause de Hor- ne) 45, 49, 274, 345 Дизъюнктивная нормальная форма (forme disjonctive normale) 33, 72 Дистрибутивность (distributivi- te) 28 Доказательство (demonstra- tion) 92, 103 — посредством опровержения (preuve par refutation) 163 Дополнительность (complemen- tarite) 29 Доступности отношение (acces- sibilite) 242 Завершаемость (completude) 40 Заголовок (tete) 271 Заключение (conclusion) 21 — импликации (consequent) 18 Законы де Моргана (lois de Morgan) 28 Замены правило (regle d'echan- ge) 97 Замыкание (fermeture) 268 — положительное (fermeture positive) 268 — рефлективное и транзитив- ное (fermeture reflexive et transitive) 272 — V (fermeture universelle) 69 — 3 (fermeture existentielle) 69 Знаний представление (repre- sentation de la connaissance) 141 Значение (valeur) 198 — слота (valeur de la facette) 172 Идемпотентность (idempotence) 28 Иерархия (hierarchie) 185 — типов (hierarchie des types) 185 — Хамского (hierarchie de Chomsky) 299 Имя индивидуума (пот speci- fique) 143 — предикатное (nom de predi- cat) 143 — слота (nom de la facette) 147 — совокупности (nom generi- que) 143 — функциональное (nom de fonction) 143 Интерпретация (interpretation) 16, 63 Предметный указатель 420 — высказываний (interpretation propositionnelle) 255 — область (domaine d'interpre- tation) 63 — частичная (interpretation partielle) 23 — Эрбрана (interpretation de Her brand) 77 Исчисление высказываний (cal- cul des propositions) 11, 12 — предикатов (calcul des pre- dicats) 54, 57 Категория синтаксическая (са- tegorie syntaxique) 270 Квантификация (quantification) 56 — область действия (portee d'une quantification) 61 Квантор (quantificateur) 56 — общности (quatificateur uni- versel) 56 — существования (quantifica- teur existentiel) 56 Кластер схематический (amas schematique) 190 Клаузальная форма (forme clausal) 76 Ключ (с1ё) 147 Коммутативность (commutati- vite) 28 Компактности теорема (theore- me de compacite) 54 Композиционный метод (prin- cipe do compositionnalite) 150 Конкретизация (instance) 67, 75, 143 — фундаментальная (instance fondamentale) 79 Константа (constante) 55, 143 — индивидная (constante indi- viduelle) 57 — предикатная (constante pre- dicative) 56, 57, 143 — функциональная (constante fonctionnelle) 57, 143 Конфигурация (configuration) 302, 306, 311 Концептуальное отношение (re- lation conceptuel) 172 Конъюнкт (cube) 33, 72 Конъюнктивная нормальная форма (forme conjonctive normale) 30, 72 Легальность (legalite) 255 Литера (litteral) 16, 72 Логика веры (logique des croy- ances) 153 — возможного (logique du pos- sible) 152 — высказываний (logique des propositions) 211 — немонотонная (logique non monotone) 220, 227, 245 — предикатов (logique des predicats) 211 — трехзначная (logique terna- ire) 158 — умолчаний (logique des de- fauts) 226, 227 — четырехзначная (logique quaternaire) 160 Логическое программирование (programmation logique) 89, 266, 333 Матрица (matrice) 68 Машина Тьюринга (machine de Turing) 127, 311 Множество рекурсивно пере- числимое (ensemble recursive- ment enumerable) 137 — рекурсивное (ensemble re- cursif) 14, 138 Модальная логика (logique mo- dale) 239 — нормальная система (syste- me modal normal) 239 — теорема (theoreme modal) 250 Модальный оператор (орёга- teur modal) 153 Моделей теория (theorie des modeles) 122 Модель (modele) 16, 113, 243 — высказываний (modele pro- positionnel) 255 Предметный указатель 421 Моноид свободный (monoide libre) 268 Монотонность ограниченная (monotonie restreinte) 221 Наследственное свойство (pro- priete d'heritage) 183 Неклаузальное правило резо- люций (resolution non clausa- 1е) 44, 89 —.— согласия (consensus non clausale) 89 Область Э рб рана (domaine de Herbrand) 76 Обоснование (justification) 229 Общезначимость (valide) 244 — в модели (valide. dans un modele) 244 — в структуре (valide dans une structure) 244 Общезначимые рассуждения (raisonnement valide) 217 Объявление оператора (decla- ration'd'operateur), 391 Одновременная постановка (substitution uniforme) 12, 60, 97 Оператор-Л, (operateur-A.) 160 Операции над списками (ope- ration sur les listes) 378 Операция паросочеталия (ope- ration de correspondance) 200 Остановки проблема (probleme de 1'arret) 139 Отношение порядка (relation d'ordre) 28, 117 Отрицание в Прологе (negation Prolog) 349 Отсечение (coupure) 363, 366 Оценка (valuation) 242 able quantifice) 61 — начальная (variable de de- part) 270 — свободная (variable libre) 60 Подстановка (substitution) 66, 354 Полугруппа свободная (demi- group libre) 268 Правило (regle) 165, 268, 270, 293, 345 — немонотонного вывода (infe- rence non monotone) 223 — обобщения (regle de genera- lisation) 106 — переписывания (regle de reecriture) 271 — рекурсивное (regle recursi- ve) 348 — соединения (regle d'assemb- lage) 143 — умолчания (regle de> de- faut) 229 — Modus Ponens (Modus Po- nens) 94 Предваренная форма ('forme prenexe) 70 Предикат (predicat) 59, 143 — бинарный (predicat binaire) 144 — встроенный (predicat prede- fini) 362 — унарный (predicat unaire) 144 Префикс (prefixe) 70 Принцип двойственности (prin- cipe de dualite) 29, 65 — монотонности (principe de monotonie) 104 Продукция (production) 268, 270 Пролог (Prolog) 290 Прототип (prototype) 187, 189, 191 Процедура (procedure) 125 Переменная (variable) 55, 57 143, 270 — анонимная (variable anony- me) 344 — квантифицированная (vari- Разрешимая теория (theorie decidable) 120 Разрешимость (decidabilite) 123 Рассуждения модифицируемые 422 Предметный указатель (raisonnement revisable) 217 — с умолчаниями (raisonne- ment par defaut) 206, 228 Расширение (extension) 232 — устойчивое (extension stable) 257, 258, 262 Резольвента (resolvante) 38 Резолюций принцип (resolu- tion) 38, 42, 87, 99 Резолюция фундаментальная (resolution fondamentale) 84 Рефлексивность (reflexivitc) 28 Решетка (treillis) 28 — Лшденбаума (treillis de Lindenbaum) 28 — множеств (treillis des en- sembles) 186 — типов (treillis des types) 186 Слот (facette) 147, 198 Совокупности поле (champ ge- nerique) 176 Совокупность—ссылка (gene- rique—referent) 175, 188 Согласие (consensus) 43, 89 Сортировка (tri) 380 Список (liste) 275, 376 Ссылки поле (champ referent) 176 Стратегия (strategic) 298 — Девиса и Полнена (strate- gic de Davis et Pufnam) 83 Структура (structure) 113, 242 Схема (schema) 190 Сцепка (unite) 197 Свойство унаследованное (рго- priete heritee) 183 Связанная переменная (variab- le liee) 60 Связка (connecteur) 57 Семантика (semantique) 15, 62, 150, 157, 162 — возможных миров (semanti- que des mondes possibles) 158, 242 Сеть базовая переходов (гё- seau BTN) 316 — рекурсивная переходов (ге- seau RTN) 320 — семантическая (reseau se- mantique) 172 — усиленная переходов (re- seau ATN) 325 Сигнатура (signature) 113 Символ исходный (symbole ini- tial) 270 — нетерминальный (symbole поп terminal) 270 Синтаксис (syntaxe) 15 Система натурального вывода (deduction naturelle) 102, 107 Сколемовская форма (forme de Skolem) 73 Следствие логическое ^sonse- quence logique) 21 Тавтология (tautologie) 21 Тезис Чёрча (these de Church} 133 Тело (corps) 271 Теорема (theoreme) 92, 113 Теория (theorie) 113 — категоричная (theorie cate- gorique) 121 — нормальная (theorie погтпа- le) 233 — первого порядка (theorie du premier ordre) 111, 113 — полная (theory complete) 121 — полунормальная (theory se- mi-normale) 236 — с умолчаниями (theorie avec defauts) 229 Терм (terme) 56, 58 — индивидный (terme fonda- mental) 337 — константный (terme con- stant) 337 Точка неподвижная (point fixe) 250 Транзитивность (transitivite) 28 Требование (prerequis) 229 Узел — индивид (noeud specifi- que) 176 Предметный указатель 423 — концепт (noeud concept) 172 — связывающий (noeud rela- tionnel) 172 — совокупность (noeud generi- que) 176 — ссылка (noeud referent) 176 Умолчание (defaut) 229 — нормальное (defaut normal) 234 Универсум (univers) 242 Унификатор (unificateur) 355 — наиболее общий (unificateur le plus general) 86, 356 Унификация (unification) 85 Унифицируемые литеры (litte- raux unifiables) 85 — общезначимая (formule va- lide) 20, 64 Фрейм (cadre) 197 — функциональный (cadre fon- ctionnel) 199 — явный (cadre explicite) 198 Фундаментальная форма (for- me fondamentale) 78 Функциональная форма (forme fonctionnelle) 58 Функция (fonction) 59, 149 — — примитивно рекурсивная (fonction primitive recursive) 136 — рекурсивная (fonction recur- . sive) 137 Факт (fait) 46, 165, 201, 293, 337 Финитно выполнимое подмно- жество (sous-ensemble fini- ment consistant) 51 Форма предикатная (forme predicative) 56, 59, 144 Формализм усиленных сетей переходов (formalisme ATN) 314 Формула (formule) 13, 59 — выполнимая (formule son- sistante) 20, 64 — невыполнимая (formule in- consistante) 20, 64 с- — нейтральная (formule con- tingente) 21, 64 Цель (but) 46, 165, 201, 293, 341, 353 .Элиминация (elimination) 28 Эпистемическая логика (logique epistemique) 153 Язык (langage) 113 — алгоритмический Гёделя (langage algorithmique de Godel) 131 — контекстно-свободный (lan- gage hors-contexte) 272 Оглавление Предисловие редактора перевода ........... 5 Предисловие . ......—•••••••••• ' 1. Логика • . ...•......,.••••• 11 1.1. Исчисление высказываний ............ 11 1.1.1. Введение . ............... 11 1.1.2. Словарь . ........... .... 11 1.1.3. Синтаксис исчисления высказываний ..... 12 1.1.4. Семантика исчисления высказываний ..... 15 1.1.5. Исчисление высказываний и естественный язык 16 1.1.6. Выполнимые и общезначимые формулы .... 20 1.1.7. Алгоритмическая точка зрения . . . . . ... 23 1. .8. Алгоритм редукции . ........... 26 1. .9. Алгебраический подход ........... 27 . .10. Дизъюнкты и нормальные формы ....... 30 . .11. Алгоритм Девиса и Патнема ........ 33 . .12. Принцип резолюций . ........... 37 . .13. Доказательства невыполнимости, основанные на принципе резолюций ........ .... 38 .1.14. Приложения и примеры использования метода резолюций . ........... .... 42 .1.15. Неклаузальное правило резолюций ...... 44 .1.16. Хорновские дизъюнкты . . ........ 45 .1.17. Хорновские дизъюнкты и КС-грамматики ... 49 .1.18. Теорема компактности . .......... 51 1.2. Исчисление предикатов ............. 54 .2.1. Введение . ............... 54 .2.2. Словарь . ............... 57 .2.3. Синтаксис исчисления предикатов ...... 58 .2.4, Свободные и связанные переменные, область дей- ствия .... ............. 59 .2.5. Семантика исчисления предикатов ...... 62 .2.6. Подстановка и конкретизация ........ 66 .2.7. Предваренная и нормальные формы ...... 69 .2.8. Сколемовские и клаузальные формы ..... 72 .2.9. Эрбранова интерпретация и компактность ... 76 .2.10. Два простых примера ........... 80 .2.11. Алгоритм Куайна, Девиса и Патнема ..... 83 .2.12. Фундаментальная резолюция . ....... 84 .2.13. Унификация . .............. 85 .2.14. Метод резолюций . ............ 87 .2.15. Принцип логического программирования ... 89 Оглавление 425 2. Аксиоматические системы ......... 92 2.1. Аксиоматический подход к логике ......... 92 2. .1. Введение ............... 92 2. .2. Свойства аксиоматических систем ...... 93 2. .3. Простая аксиоматическая система исчисления вы- сказываний . .............. 94 2. .4. Несколько интересных теорем ........ 95 2. .5. Полнота . ............... 98 2. .6. Польза аксиоматических систем ....... 100 2. .7. Система натурального вывода ........ 102 2. .8. Классические аксиомы для квантификации . . . 105 2. .9. Натуральный вывод в логике предикатов . . . 107 2. .10. Равенство в исчислении предикатов ...... 108 2.2. Теории первого порядка .......... .111 2.2.1. Введение . . . . . . . ........ Ill 2.2.2. Неформальные и формальные теории ..... 112 2.2.3. Польза теорий . . . . . . . . . . . . . .114 2.2.4. Теория частичного порядка . . . . . . . . .117 2.2.5. Модели теории . ............. 119 2.2.6. Алгоритмы и разрешимость ......... 123 2.2.7. Алгоритмический язык Тьюринга . . . . . . .127 2.2.8. Алгоритмический язык Гёделя ........ 131 2.2.9. Кодирование и тезис Чёрча ......... 133 2.2.10. Класс вычислимых функций . . . . . . . . 136 2.2.11. Проблема остановки ........... .139 '3. Представление знаний и рассуждении • . . • HI 3.1. Логическое представление ............ 141 3.1.1. Введение . ............... 141 3.1.2. Синтаксис логики предикатов ........ 142 3.1.3. Примеры . ............... 144 3.1.4. Преобразование унарных предикатов в бинарные 144 3.1.5. Примеры . ............... 145 3.1.6. Преобразование от-арных предикатов в произве- дение бинарных .............. 146 3.1.7. Явное представление ссылок ......... 148 3.1.8. Представление функциями ......... 149 3.1.9. Примеры ............... .149 3.1.10. Семантика логики предикатов ........ 150 3.1.11. Модальная логика предикатов ........ 152 3.1.12. Модальные операторы . .......... 153 3.1.13. Примеры модальных операторов ....... 154 3.1.14. Синтаксис модальной логики предикатов .... 155 3.1.15. Примеры , ............... 155 3.1.16. Трехзначная семантика для модальной логики предикатов . .............. 157 3.1.17. Семантика возможных миров ........ 158 3.1.18. Ламбда-исчисление , ........... 160 3.1.19. Рассуждения, использующие логические формулы 162 426 Оглавление 3.1.20. Пример .............. 163 3.1.21. Рассуждения по поводу знаний ...... 165 3.1.22. Системы прямой дедукции ........ 166 3.1.23. Системы обратной дедукции ....... 167 3.2. Сетевое представление ........... .168 3.2.1. Введение . ............... 168 3.2.2. Концептуальные графы ........... 169 3.2.3. Пример и терминология . . . . ..... 170 3.2.4. Семантические сети . ........... 172 3.2.5. Правила конъюнкции и упрощения ...... 173 3.2.6. Представление контекста ......... 173 3.2.7. Представление «совокупность-ссылка» ..... 175 3.2.8. Пример . ................ 177 3.2.9. Пример введения кванторов ........ 177 3.2.10. Временные и модальные операторы ...... 179 3.2.11. Канонические графы . ........... 181 3.2.12. Правила построения . ........... 182 3.2.13. Унаследованные свойства . ......... 183 3.2.14. Решетки типов; иерархии типов ........ 185 3.2.15. Решетки множеств и решетки типов ...... 186 3.2.16. Определение типа посредством рода и различия 188 3.2.17. Прототипы .....'........... 189 , 3.2.18. Схемы и схематические кластеры ....... 190 3.2.19. Рассуждения, использующие семантические сети 192 . 3.2.20. Заключение . ............... 194 3.3. Объектное представление ............ 196 3.3.1. Введение . ............... 199 3.3.2. Сцепки . ................ 197 3.3.3. Фреймы и слоты "............. 197 . 3.3.4. Явные фреймы . ............. 198 3.3.5. Функциональные фреймы . ......... 199 3.3.6. V -квантификация ............ 199 3.3.7. Рассуждения, использующие объектное представ- ление .................. 200 3.3.8. Паросочетание . . ..... ..... 200 3.3.9. Функциональные атрибуты ........ 202 3.3.10. Автоматические рассуждения, использующие фреймы . ................ 203 3.3.11. Иерархические рассуждения, использующие фреймы 204 3.3.12. Рассуждения с умолчаниями ........ 206 3.3.13. Заключение . .............. 208 4. Логика и модифицируемые рассуждения • • . 209 4.t. Многочисленные роли логики .......... 209 4.1.1. Введение ................. 209 4.1.2. Логика как средство для представления знаний и рассуждении .............. 209 4.1.3. Логика как формализм ссылок ....... 213 4.1.4. Неизбежность логики . ........... 214 4.1.5. Анализ знаний и рассуждении . . . . . . . .215 4.1.6. Заключение . .............. 216 Оглавление 427 4.2. Логика и модифицируемые рассуждения ...... 217 4.2.1. Формализация модифицируемых рассуждении . . 217 4.2.2. Классическая логика и общезначимые рассуждения 217 4.2.3. Характеристики немонотонных логик ...... 220 4.2.4. Зацикливание правил немонотонного вывода . . 223 4.2.5. Полирасшнряемость немонотонной системы . . . 225 4.2.6. Различные формы немонотонных рассуждении . . 225 4.3. Логики умолчаний ............... 227 4.3.1. Введение ................. 227 4.3.2. Теории с умолчаниями ........... 229 4.3.3. Примеры применения умолчаний ..'..... 229 4.3.4. Расширения теории с умолчаниями ...... 231 4.3.5. Примеры расширений теорий с умолчаниями . . . 232 4.3.6. Нормальные теории ........... 233 4.3.7. Теория доказательств для нормальных теорий . . 234 4.3.8. Полунормальные теории ........... 236 4.3.9. Наследственные системы с исключениями . . . 237 4.4. Модальные логики знания и веры ......... 239 4.4.1. Введение ................. 239 4.4.2. Некоторые элементарные модальные системы . . 239 4.4.3. Семантика возможных миров ........ 242 4.5. Немонотонные логики Мак-Дермотта ....... 245 4.5.1. Введение . ................ 245 4.5.2. Язык логики Мак-Дермотта . ........ 246 4.5.3. Пример немонотонной аксиоматической системы . 247 4.5.4. Примеры . ................ 252 4.5.5. Ценность логики Мак-Дермотта ....... 252 4.6. Автоэпистемичесхие логики ........... 253 4.6.1. Введение ................. 253 4.6.2. Язык и семантика ............. 254 4.6.3. Характеризация синтаксиса . ........ 256 4.6.4. Анализ немонотонной логики ......... 257 4.6.5. Семантика возможных миров ........ 260 4.6:6. Пример . ................ 263 4.6.7, Области применения . ........... 265 5, Формальные грамматики и логическое програм- мирование . ......... ........ 266 5.1. Формальные грамматики и логика ......... 266 5.1.1. Введение . ............... 266 5.1.2. КС-грамматики . ............. 268 5.1.3. Формальное определение КС-грамматики .... 270 5.1.4. КС-грамматика и хорновские дизъюнкты .... 274 5.1.5. ОК-грамматики . ............. 278 5.1.6. ОК-грамматики и логика .......... 283 5.1.7. Построение синтаксического дерева ...... 287 5.1.8. ОК-грамматики в Прологе ......... 290 5.1.9. Пример .... ............ 293 5.1.10. Графическое представление и стратегии .... 295 428 Оглавление 5.2. Иерархия Хомского .............. 299 5.2.1. Введение . ............... 299 5.2.2. Регулярные грамматики . ......... 300 5.2.3. Конечные автоматы . ........... 301 5.2.4. Пример . ................ 304 5.2.5. КС-грамматики и стековые автоматы ..... 305 5.2.6. Пример . ................ 308 5.2.7. Грамматики и языки Хомского типа 1 .... 310 5.2.8. Машины Тьюринга и грамматики типа 0 . . . .311 5.3. Формализм усиленных сетей переходов . . . . . . . 314 5.3.1. Введение , ............... 314 5.3.2. Конечные автоматы и диаграммы переходов . .315 5.3.3. Базовые сети переходов .......... 316 5.3.4. Пример . ................ 318 5.3.5. Рекурсивные сети переходов ........ 320 5.3.6. Пример ................. 323 5.3.7. Усиленные сети переходов ......... 325 5.3.8. Пример . ................ 327 5.3.9. Построение синтаксического дерева ...... 328 5.3.10. УП-сети и ОК-грамматики ........ 330 6. Пролог и логическое программирование • . .333 6.1. Основы языка ................ 333 6.1.1. Введение . ............... 333 6.1.2. Термы и объекты ............. 335 6.1.3. Факты и элементарные вопросы ....... 337 6.1.4. Конъюнкция . .............. 340 6.1.5. Переменные , .............. 340 6.1.6. Анонимные переменные ........... 344 6.1.7. Правила . ............... 345 6.1.8. Рекурсивные правила . .......... 348 6.1.9. Дизъюнкция . .............. 348 6.1.10. Отрицание ................ 349 6.1.11. Области действия имен .......... 350 6.1.12. Операторы ................ 351 6.2. Алгоритмы Пролога .............. .352 6.2.1. Введение . ............... 352 6.2.2. Соответствие и унификация ......... 354 6.2.3. Вычисление ответа . ........... 358 6.2.4. Встроенные предикаты .......... 362 6.2.5. Отсечение . ............... 366 6.3. Инструментарий и пример ........... 371 6.3.1. Введение . ............... 371 6.3.2. Вычислительные процедуры ........ 371 6.3.3. Списки . ................ 376 6.3.4. Операции над списками .......... 378 6.3.5. Перестановки и сортировки ........ 380 6.3.6. Представление списка в виде разности списков 384 6.3.7. Ввод-вывод . .............. 385 6.3.8. Примеры ввода-вывода ........... 387 Оглавление 429 6.3.9. Анализ и построение термов ......... 389 6.3.10. Объявление оператора . ........ 391 6.3.11. Поиск в пространстве решений ....... 394 6,4. Пролог и КС-грамматики ............ 399 6.4.1. Введение ........... 399 6.4.2. Распознавание КС-фраз . ........ 399 6.4.3. Анализ КС-фраз . ........... 403 6.4.4. ОК-грамматики и атрибутные грамматики 407 Литература . ............. . . ' 411 Предметный указатель ........... . . 418 Уважаемый читатель! Ваши замечания о содержании кни- ги, её оформлении, качестве перевода и другие просим присылать по адре- су: 129820, Москва, И-110, ГСП, 1-й Рижский пер., издательство «Мир». Научное издание Андре Тейз. Паскаль Грибомон, ?К&рж Луи и др. ЛОГИЧЕСКИЙ ПОДХОД К ИСКУССТВЕННОМУ ИНТЕЛЛЕКТУ: ОТ КЛАССИЧЕСКОЙ ЛОГИКИ К ЛОГИЧЕСКОМУ ПРОГРАММИРОВАНИЮ Заведующий редакцией академик В. И. Арнольд Зам. эав. редакцией А. С. Попов 'Ст. научи, 'редактор А. А. Бряндннская Мл. научи, редактор Р. И. Пяткина Художник В. С- Потапов Художественный редактор В. И. Шаповалов Технический редактор О. Г. Лапко Корректор А. ф. Рыбальченко И Б № 7329 Сдано а набор. 2.04.90. Подписано к печати 26.11.90. Формат в4х108'/з». Бумага офсет. № 2. Печать высокая. Гарнитура литературная. Объем «,75 •бум. л. Усл. печ. л. 22,68. Усл. кр.-отт. 22,68. Уч.-изд. л. 19,45. Иад. № 1/7059. Тираж 20 000 экз. Зак. 493. Цена 2 р. 90 к. Издательство «Мир» В/О «Соаэкспорткнига» Государственного комитета СССР по печати. 129820, ГСП, Москва, И-110, 1-й Рижский пер., 2 Ленинградская типография № 2 головное предприятие ордена Трудового Красного Знамени Ленинградского объединения «Техническая книга» им, Евгении Соколовой Государственного комитета СССР по печати. 198052i г, Ленинград, Л-52, Измайловский проспект, 29, СОВЕТСКО-ФРАНКО-ИТАЛЬЯНСКОЕ ПРЕДПРИЯТИЕ «ИНТЕРКВАДРО» Отдел математических разработок АНАЛИТИЧЕСКИЙ ОБЗОР «Программное обеспечение в области охраны окружающей среды» Обзор позволит Вам: • сориентироваться в программном обеспечении проблемы окру- жающей среды; • определить перспективные направления Ваших исследований; • выбрать хорошо зарекомендовавшее себя программное обеспе- чение для решения Ваших практических задач. Обзор включает анализ следующего программного обеспечения: • информационных систем; •• обучающих программ; • экспертных систем; • программ в области математического моделирования распро- странения загрязняющих веществ в окружающей среде. Раздел, посвященный системам и базам данных, дает инфор- мацию о тематике и местонахождении всех уществующих баз данных по охране окружающей среды и смежным проблемам. Обзор полезен разработчикам программного обеспечения, на- учным работникам, преподавателям вузов соответствующих спе- циальностей. Цена 1100 руб., для учебных и академических учреждений— 800 руб. Заказы следует направлять по адресу: 125130, Москва, 2-и Новоподмосковный пер., 4, СП «Интерквадро», Отдел мате- матических разработок, тел. (095) 259-92-01, телекс (871) 413560 KVINT SU, телетайп 20732Г ВАЙЛЕ, телефакс (095) 9430059.