Существенное продвижение в этом направлении предпринял Грин [11], продемонстрировавший в качестве генератора планов законченную систему доказательства теорем методом резолюции. Согласно этому подходу, начальная ситуация, целевая ситуация и результаты применения имеющихся операторов описываются в виде множества аксиом исчисления предикатов первого порядка. Далее с помощью принципа резолюции доказывается предположение, что существует ситуация, удовлетворяющая описанию цели. Побочным результатом успешно проведенного доказательства является план последовательного преобразования начальной ситуации в целевую. [c.391]
Приведенных примеров, по-видимому, достаточно. Отметим только, что исчисление предикатов и формальные грамматики, широко используемые в языках программирования, суть конструктивные формальные системы. Но в общем случае они не являются разрешимыми формальными системами. [c.35]
Как уже говорилось, исчисление предикатов и другие чисто логические исчисления обладают тем преимуществом, что в них часто можно сформировать процедуры вывода, имеющие целенаправленный характер, позволяющие за конечное число шагов либо получить нужное преобразование, либо показать, что интересующий нас вывод построить невозможно. К сожалению, ЯСУ и в этом отношении уступает языку логических исчислений. УСК обладает набором правил преобразования цепочек друг в друга. Однако пока еще не доказана ни полнота этого набора, ни эффективность процедуры преобразования, определяемой способностью через конечное число шагов прекратить преобразования, если цель недостижима. [c.71]
Метод построения доказательства. При таком подходе описания исходной и целевой ситуации рассматриваются как формулы некоторого исчисления. Все элементы, входящие в исходное описание, трактуются как аксиомы этого исчисления, а все элементы, образующие целевое описание,— как формулы, которые необходимо вывести из данного набора аксиом с помощью имеющейся системы правил вывода. Обычно в качестве такого исчисления используется исчисление предикатов первой степени. Правила вывода делятся на два типа правила вывода универсального характера, используемые в традиционном исчислении предикатов, и правила вывода, верные только в рамках той проблемной области, которая описывает данный объект управления, особенности его функционирования и специфику управления им. Правила второго типа принято называть эвристическими правилами вывода. В качестве процедуры поиска вывода используется какая-нибудь достаточно мощная процедура типа метода резолюций или обратного метода вывода Маслова. Эти процедуры будут описаны ниже. [c.226]
В работе [4.45] под понятием понимается некоторая формула узкого исчисления предикатов, записанная в предваренной нормальной форме. Задача формирования понятия рассматривается в виде двух последовательно решаемых задач формирование префиксной части формулы, т. е. определение объема понятия, и формирование матричной части формулы, т. е. определение содержания понятия. [c.267]
Ефимов Е. И. Автоматическое формирование понятий, описываемых замкнутыми формулами узкого исчисления предикатов.— В кн. Семиотика и [c.276]
М а с л о в С. Ю. Обратный метод установления выводимости в классическом исчислении предикатов.—ДАН СССР, 1964, т. 159, № 1, с. 17—20. [c.277]
Материал этой книги неоднократно апробировался как на рабочих семинарах, так и на основных курсах лекций. Сначала он был задуман в качестве семестрового спецкурса по технологии программирования, хотя большая его часть может быть изложена на последнем и даже на втором году общего курса по информатике. Перечень исходных знаний ограничивается некоторым знакомством со школьной алгеброй, понятиями теории множеств и символикой исчисления предикатов. Книга может быть использована также в качестве интенсивного недельного курса для профессиональных программистов. В таком курсе следует делать упор на примеры и определения, оставляя математические обоснования для последующей самостоятельной работы. Материал первых двух глав вполне пригоден и для более компактного курса, и даже часовой обзор книги может быть полезен при условии тщательного отбора материала, достаточного для разбора весьма поучительной истории о пяти обедающих философах. [c.7]
Декларативный подход к Обработке реляционных баз данных основан на интерпретации понятий и методов математической логики, В частности, реляционное исчисление базируется на исчислении предикатов. Перечислим необходимые для реляционного исчисления понятия математической логики. [c.72]
Известны и другие разновидности моделей смыслового уровня. Например, широко применяется язык исчисления предикатов, достоинство которого состоит в принципиально отличном от традиционных подходе к описанию способа решения некоторой управленческой задачи дается описание логической модели предметной области (некоторые факты относительно свойств предметной области и отношений между этими [c.42]
К недостаткам языка исчисления предикатов можно отнести трудность (неоднозначность) перевода предложений естественного языка в конструируемые формулы сложность учета в процедурах вывода частных знаний о предметной области отсутствие эффективных процедур для исчислений более высоких порядков, чем первый отсутствие взаимодействия (взаимосвязи) между формулами языка. [c.43]
Логическое исчисление специального вида (исчисление предикатов), о котором говорилось выше, реализовано в языке программирования Пролог. Обычно логика используется для выражения высказываний, отношений между высказываниями и правил вывода одних высказываний из других. Пролог - это первая попытка разработки языка, который позволял бы программисту описывать свои задачи средствами математической логики, а не с помощью традиционных для программирования конструкций, указывающих, что и когда должна делать вычислительная машина. Способы, используемые для представления объектов в Прологе (термы), соответствуют способам, имеющимся в языке исчисления предикатов. Чтобы делать высказывания об объектах, необходимо иметь возможность описывать отношения между объектами. Это делается с помощью предикатов. Формула (атомарное высказывание) состоит из предикатного символа и соответствующего ему упорядоченного множества термов, являющихся его аргументами. В Прологе структура может быть использована и в качестве целевого утверждения, и в качестве аргумента для другой структуры. [c.43]
Язык исчисления предикатов разработан для отражения большого количества связей типа "если..., то. ..", и в нем имеется строгое разделение между функциональными символами, используемыми для построения аргументов и высказываний (в отличие от Пролога). Однако логику, основанную на транзитивности, например, родо-видовых связей, такие языки могут осуществлять лишь косвенно. [c.44]
Дайте характеристику языку исчисления предикатов, какой системой программирования он реализуется [c.55]
Техника сопоставления с образцом широко применялась уже в первых программах, созданных специалистами по искусственному интеллекту [1]. Достаточно ясно, однако, что значение сопоставления шире, чем чисто программистский прием на нем так или иначе основаны очень многие действия, предпринимаемые системами искусственного интеллекта при манипулировании данными. Так в системах доказательства теорем, основанных на исчислении предикатов первого порядка, использовался алгоритм унификации, который представляет собой более сложный вариант сопоставления. Подобное же сопоставление является обязательным элементом [c.210]
Наконец, модели в виде систем продукций охватывают широкий класс различных порождающих моделей, в который входят такие известные модели, как формальные грамматики, исчисления высказываний и предикатов, сетевые модели и многие другие. Во всех известных на сегодня моделях ситуационного управления для решения задачи пополнения использовались именно продукционные системы. [c.98]
Исследованию и применению аналогии в процессе выработки плана решения задачи посвящена представленная в данном разделе работа Клинга. В ней вывод по аналогии рассматривается как механизм, резко повышающий общую эффективность работы решающей системы. Сначала автором дается общая постановка проблемы вывода по аналогии, применимого для поиска решения задачи, в определенном смысле аналогичной какой-либо из ранее решенных задач. Однако описание реальной системы дается на примере более частного вида аналогии в применении к системам типа QA3 (Грин [11]), в которых в основу положен язык исчисления предикатов первого порядка, а в качестве систем принятия решений используется система автоматического доказательства теорем. Специфика выбранного вида аналогии как раз и предопределяется типом системы принятия решений. Целью работы программы вывода по аналогии в [c.375]
Проблемная среда для системы STRIPS определяется путем задания двух типов информации модели, состоящей из множества предложений, описывающих исходное состояние среды, и множества операторов для воздействия на эту среду. Каждый оператор характеризуется заранее установленным правилом, описывающим условия, при которых он может быть применен, и списком предложений, описывающих результат его действия. В частности, результатом применения оператора будет устранение из модели всех предложений, совпадающих по форме с предложениями из списка вычеркиваний оператора, и добавление в модель всех предложений, содержащихся в его списке добавлений . Все предложения, задаваемые системе STRIPS, выражены на языке исчисления предикатов. [c.407]
Существует несколько путей формулирования задач в подобной среде. В экспериментах с системой STRIPS цель представлялась в виде требования добиться истинности некоторой (одной) правильно построенной формулы (ппф) исчисления предикатов. Случай многих целей можно было бы определить как наличие множества целевых ппф, снабженных коэффициентом срочности или весом , указывающим его относительную важность. Ппф, обладающие отрицательным весом, будут тогда описывать состояния, которых следует избегать. Далее следует точно определить общую задачу системы. В случае одной целевой ппф задача робота — достигнуть цели (возможно, путем минимизации условных стоимостей планирования и исполнения). В среде со многими целями определить общую задачу системы столь же четко уже не так просто. Но можно предположить, что такое определение должно включать максимизацию каких-то отношений типа выгода/затраты. При вычислении конечной выгоды для некоторого частного плана нужно определить способ оценки веса каждой целевой ппф, которая удовлетворяется в процессе продвижения плана от текущей к конечной ситуации. В любом случае расчет планов и их выполнение в среде со многими целями потребуют сложной вычислительной схемы для оценки и сравнения относительной выгоды и веса различных целей и стоимости их достижения. [c.411]
Здесь среда является синонимом информационной базы. Но она может также включать допустимое функциональное упорядочивание (в исчислении предикатов) и другие типы ограничивающей информации. Каждое правило, ограничивающее среду , может быть переведено в новое эквивалентное решающее правило, ограничивающее применение процедур вывода решателем задач- Однако я считаю, что проще вести обсуждение системы ZORBA в терминах модифицированных сред, чем (что эквивалентно) в терминах модифицированных решающих правил. [c.478]
Внутренним стержнем системы ZORBA-1 является эвристическая программа для получения аналогий между парами теорем, представленными на языке исчисления предикатов. Чтобы облегчить понимание и сделать возможными обобщения, она была сконструирована и построена главным образом на модульной основе. Следовательно, большую часть системы можно описать в терминах алгоритмов. В этом разделе при описании работы программы я надеюсь сочетать некоторые представления эвристического программирования с алгоритмической точностью. ZORBA-1 использует интересное множество поисковых и согласующих подпрограмм, которые были построены эмпирически, а затем обобщены и испытаны на наборе пар задач. (Т1—Т2 и ТЗ—Т4 прекрасно представляют этот набор.) Управляющая структура подсистем ИСХОДНОГО ОТОБРАЖАТЕЛЯ и РАСШИРИТЕЛЯ построена с расчетом на обработку различными сопоставляющими подпрограммами (описываемыми ниже) весьма сходных структур. Последующее описание [c.487]
ИСХОДНЫЙ ОТОБРАЖАТЕЛЬ построен таким образом, что для двух правильно построенных формул исчисления предикатов первого порядка он получает отображение между переменными и входящими в них предикатами. Информация, касающаяся отображения переменных, используется в ИСХОДНОМ ОТОБРАЖАТЕЛЕ при отображении предикатов в случаях, кажущихся неясными. ИСХОДНЫЙ ОТОБРАЖАТЕЛЬ выдает на выходе множество ассоциированных предикатов, которые входят в формулировки теорем Т и ТА. Эта ограниченная аналогия используется далее в качестве исходной РАСШИРИТЕЛЕМ, который находит полное отображение для всех предикатов, использованных в ргоопТ]. Дополнительно РАСШИРИТЕЛЬ находит аналогии для всех аксиом из множества AXSET В отличие от РАСШИРИТЕЛЯ ИСХОДНЫЙ ОТОБРАЖА- [c.488]
Для распространения метода аналогий на области, описываемые исчислением предикатов с константами, потребовались бы совершенно другие алгоритмы анализа. Рассмотрим робот, которому задано перейти из Стэнфордского исследовательского института 1) в лабораторию 5 на том же этаже, 2) в Стэнфорд-ский университет, 3) в Сан-Франциско, 4) в Нью-Йорк, 5) в Чикаго. Эти пять задач могут быть представлены для QA3 следующим образом [c.510]
Второй язык для описания ситуаций, который до сих пор пользуется популярностью среди специалистов по ситуационному управлению,— язык исчисления предикатов первого порядка. В этом языке. можно выразить все то, что выразимо и в ЯСУ, если не учитывать модификаторы и все квантификаторы, кроме принятых в исчислении предикатов кванторов V и 3. У исчисления предикатов есть свои преимущества, связанные с наличием развитых процедур вывода. Об этом мы будем говорить в дальнейшем. Предполагая, что большинство читателей знакомо с классическим исчислением предикатов, не будем тратить здесь место для его описания и ограничимся лишь примером. [c.69]
УСК реализует принцип независимости от предметной области. При различных интерпретациях символов, входящих в цепочки, можно получать описания, пригодные для любых мыслимых предметных областей. Это обстоятельство носит принципиальный характер. В языке ситуационного управления принцип полной экспликации смысла реализован не полностью, отношения из базового множества как бы свалены в одну кучу . Они конкретизованы до различного уровня общности, что требует введения модификаторов на отношения. В языках типа языка исчисления предикатов не реализован принцип экспликации смысла. Записи в этих языках не дают возможности сопоставить им смысл ни на каком уровне общности. [c.70]
Та семантика, которая реализуется в УСК на метауровне, т. е. без интерпретации символов, входящих в цепочку, является недоговоренной. Она жестко задается семантикой простых ядерных конструкций и синтаксисом производной цепочки. Такое свойство УСК также отличает этот язык от языка исчисления предикатов, в котором смысл предикатных формул зависит от той или иной договоренности. Язык ситуационного управления при заданном списке базовых отношений и их интерпретации приближается в этом смысле к возможностям УСК. [c.71]
Метод резолюции, предложен в середине 60-х годов. Он относится к той группе методов поиска вывода, которую обычно называют методами опровержения. Это название вызвано тем, что в этих методах вместо поиска вывода некоторого утверждения F ищется доказательство невыводимости отрицания данного утверждения F. Эквивалентность обеих задач вытекает из замкнутости исчисления предикатов первого порядка, в котором используется метод резолюции, т. е. в силу закона исключенного третьего в таких исчислениях из ложности F следует истинность F. [c.227]
Сопоставление особенностей представления ситуаций в ЯСУ и яьыке RX-кодов впервые было проделано Л. Б. Нисенбоймом. Сопоставление ЯСУ и языка исчисления предикатов было начато (но не закопчено) в работе [2.24]. Более подробное знакомство с использованием языка исчисления предикатов для целей управления можно осуществить по монографии [1.1], а также по монографии [2.25]. [c.261]
Модификации системы STRIPS, система ABSTRIPS, а также дедуктивные вопросно-ответные системы QA-3 и QA-4, идеи которых легли в основу многих планирующих систем, описаны в монографии [5.4]. Пионерской работой в области метода резолюции была работа [5.5]. Различные способы повышения эффективности стратегий, используемых при нахождении резольвент, описаны в монографии [5.6]. Поиск таких улучшений все время продолжается, так как метод резолюции остается одним из самых популярных среди разработчиков многих практических систем. Однако он не единственно возможный или самый эффективный. Например, обратный метод поиска доказательства, предложенный в свое время известным советским логиком С. Ю. Маеловым [5.7], во многих отношениях превосходит метод резолюции. Этот метод реализован, например, в системе планирования СФИНКС, описанной в уже упоминавшейся монографии [5.4]. Трудности, характерные для имеющихся сейчас процедур вывода, и возможность совмещения этих процедур с некоторыми эвристическими приемами обсуждалась многими авторами. Сводка соответствующего материала приведена в [5.8] и [5.9]. В монографии [5.4] проводится сравнение чисто логических стратегий планирования с теми стратегиями, которые мы обсуждали в 5.7. Некоторые дополнительные соображения по поводу методов планирования, опирающихся на вывод в исчислении предикатов, можно найти в работе [1.1]. Рассуждения о необходимости нелинейных планов, приведенные в конце 5.2, заимствованы из работы [5.10], где излагается описание планирующих систем, допускающих построение немонотонных планов. [c.268]