Документ взят из кэша поисковой машины. Адрес оригинального документа : http://www.intsys.msu.ru/staff/podkolzin/obzor.pdf Дата изменения: Sat Apr 5 18:13:30 2014 Дата индексирования: Sat Apr 9 23:18:46 2016 Кодировка: Windows-1251

О самообучении интеллектуальной системы
А.С.Подколзин

Введение
Легенда о самообучающемсяD саморазвивающемся искусственном интеллекте зароE дилась в недрах научной фантастики очень давноD и с тех пор стала в произведениях этого жанра чемEто совсем обыденнымF Мы редко задумываемся о томD что по отноE шению даже к естественному интеллекту понятия 4самообучение4 и 4саморазвитие4 следует использовать с большой осторожностьюF Человек обучаетсяD впитывая в себя знания и уменияD накопленные человечеством на протяжении многовекового развиE тияF Этот искусственно созданный мир знаний и является подлинным источником человеческого интеллектаF Нейросистема человеческого мозга становится естественE ным интеллектомD лишь адаптируясь к данному искусственному мируF ФактическиD мы имеем единственную интеллектуальную системуD подлинно саморазвивающуюся и самообучающуюся E это интеллект всей человеческой цивилизацииF ПоэтомуD говоE ря о 4самообучающемся искусственном интеллекте4D поначалу следует ограничиться установкой на создание компьютерной системыD способнойD как и человекD 4самообуE чаться4 по книгам и другим носителям знанийF Если же ориентироваться на создание искусственного интеллектаD саморазвиваE ющегося в абсолютном смыслеD то следует ясно отдавать себе отчетD что оъектом изучения здесь является не архитектура нейросистемы E естественной либо искусE ственнойD а логические процессыD обеспечивающие развитие упомянутого выше 4миE ра знаний4F Даже создание идеальной искусственной нейросистемы не отменит необE ходимости развития науки о логических процессахD как не отменила потребности в развитии теоретической механики способность естественных нейросистем управлять динамическими процессамиF К сожалениюD на сегодняшний день науки о логичеE ских процессах мы не имеемF Математическая логикаD предпринимая попытки найти какиеEто эффективные общие принципы автоматического решения задачD столкнуE лась с проблемой экспоненциальной трудоемкости перебораD и вынуждена была отE ступитьF В этой ситуации единственным подходом к изучению логических процессов оказывается компьютерное моделирование реальных процессов рассужденийF КомE пьютер становится своего рода микроскопомD позволяющим нарисовать детальную картину мира логических процессов во всем ее разнообразииF Уже первые попытки такого рода ясно показываютD насколько велико данное разнообразиеF Оно выглядит не меньшимD чем разнообразие физических или химических явленийD и развитие наE уки о логических процессахD а вместе с ней и создание искусственного интеллектаD затянется на весьма длительный периодF Настоящая статья посвящена исследованию логических процессовD предпринятоE му с помощью компьютерной логической системы 4Искра4F Чтобы промоделировать в системе решение задачи человекомD оно разбивалось на атомарные шагиD и для каждого шага создавалась несложная программаD способная выполнять его в анаE логичных ситуацияхF Такие программы получили название приемовF Были прорабоE таны многие предметные областиD в первую очередь математическиеD и накоплена I


база приемовD имеющая более RHHHH элементовF ФактическиD она представляет соE бой огромную коллекцию 4фотоснимков4 с траекторий решения задачD взятых из задачниковF В ряде областей база приемов оказалась способной функционировать как автоматический решатель задачD неплохо имитирующий действия человекаF НоD что гораздо более важноD она стала исходным сырьем для анализа тогоD как баE зисные теоремы предметной области преобразуются в приемыD иными словамиD для анализа процесса самообучения 4по книгам4F Были предприняты стандартизация и оптимизация приемовD создана их классификацияF Почти для каждого приема укаE зан источник E некоторая базисная теорема предметной областиF Изучена последоваE тельность действий при переходе от теоремы к приемуD и предложены предварительE ные версии алгоритмовD воспроизводящих такие действияF Среди данных алгоритмов имеются процедуры адаптации приемов к обучающим задачамF Результатом явился некоторый прототип 4генератора приемов4D позволяющий в простых случаях сразу получать вполне осмысленные приемыD в более сложных E приходить к ним после автоматической доводки по задачникуF gовсем сложные случаи дают хороший матеE риал для продолжения исследованийF Данный генератор приемов можно уподобить пирамидеD в основании которой лежит база приемовD вершиной служит множество базисных теоремD а промежуточные слои соответствуют этапам синтеза приемаF В целомD проделанная работа подтвердила эффективность использования комE пьютерной логической системы как 4микроскопа4 для изучения логических процесE сов и наметила пути создания интеллектуальной системыD способной быстро обуE чаться по традиционным источникам научноEтехнической информацииF

Архитектура решателя задач
Задачи формулируются в решателе на специальном логическом языкеD пополняемом по мере обученияF Этот же язык используется для формулировки теоремD приемов и тFпF Он может рассматриваться как вариант языка исчисления предикатовD ориE ентированный на сближение с реальной математической практикойF Вместо традиE ционных для математической логики терминов 4формула4и 4терм4 используются термины 4утверждение4 и 4выражение4F Все эти конструкции имеют скобочный вид f (a1 . . . an )F Обычным образом вводятся связанные переменныеD которые возникают лишь в связи с кванторами 4существует4D 4длялюбого4D 4существует единственный4D а также описателями 4класс4 и 4отображение4D задающими множества и функцииF Каждое новое понятие регистрируется в системе и сопровождается справочной инE формациейD уточняющей его синтаксис и семантикуF Для удобства обучения создан формульный редакторD конвертирующий скобочную запись в привычную математиE ческую формулу и обратноF Введена несложная общелогическая классификация задачD и зафиксированы струкE туры данных для представления таких задачF Задачи делятся на следующие четыре типаX IF Задача на доказательствоF Такая задача имеет список посылок A1 , . . . , An и условие A0 F Если удается установитьD что утверждение A0 является следствием утверждений A1 , . . . , An D то задача имеет ответ 4истина4F В противном случае решатель выдает символ 4отказ4F PF Задача на преобразованиеF Как и вышеD имеются список посылок A1 , . . . , An и условие A0 D которое уже является не утверждениемD а выражениемF Кроме тогоD задан список целейD уточняющихD каким именно образом должно быть P


преобразовано выражение A0 F Одни цели накладывают строгие органичения на вид ответаD другие E указывают тенденцииD учитываемые решателем @наприE мерD 4упростить4AF Преобразования проводятся в предположении истинности посылок A1 , . . . , An F Ответом задачи служит результат преобразований выраE жения A0 F Он выдается по достижении требуемого вида ответаD а в допустимых случаях E по исчерпании средств решателяF QF Задача на описаниеF Имеются список посылок A1 , . . . , An D а также список услоE вий B1 , . . . , Bm F Задан список целей C F Требуется преобразовать условия в предE положении истинности посылокD учитывая цели задачиY напримерD разрешить условия относительно неизвестныхD заданных в списке C F В этом списке может содержаться указаниеD нужен ли полный ответ или достаточен частичныйD нужE но ли упрощать его относительно известных параметровD и тFпF Обычно задача на описание сопровождается вспомогательной задачей на исследование @смF ниE жеAF Эта вспомогательная задача является накопителем общих следствий услоE вий и посылокD вывод которых иногда позволяет получит явные выражения для неизвестныхF RF Задача на исследованиеF Имеется список посылок A1 , . . . , An D и задан список целей C F Решение задачи заключается в выводе следствий из посылок с учетом целевой установкиF Оно обрывается при получении результатовD интересных для внешней задачи @усмотрение противоречияD нахождение равнства для неизE вестной и тFпFAD либо по исчерпании лимита трудоемкостиF Найденные важные следствия передаются во внешнюю задачуF Кроме перечисленных логических компонент задачиD введены технические комE понентыD используемые решателемF Во E первыхD все условия и посылки задач сопроE вождаются 4весами4 E целыми числами от H до PHD регулирующими концентрацию внимания при просмотре задачиF Во E вторыхD каждый терм задачи @условие лиE бо посылкаA сопровождается списком технических пометок E комментариев к этому термуF Такими же списками сопровождаются весь набор посылок и вся задачаF ТехE нические пометки позволяют сопровождать логические структуры данных сетевыми конструкциями различной природыF Они же регулируют взаимодействие между приE емамиF Преобразования задачиD а также ввод и рассмотрение различных вспомогательE ных задач в процессе решения обеспечиваются приемами E процедурамиD обобщаюE щими атомарные шаги рассуждений человекаF Таких приемов в процессе обучения накапливаются многие тысячиD и возникает проблема быстрого поиска нужного приE емаF В принципеD здесь возможны два подходаF Первый из них состоит в сканировании древовидного каталога базы приемовD позE воляющего отсекать ветвиD заведомо не содержащие нужного приемаF Если после отE сечения осталось более одной ветви рассматриваемой вершиныD то далее поиск предE принимается независимо в каждой из оставшихся ветвейF После тогоD как нужный прием найденD он реализуетсяD и далее цикл поиска повторяется зановоF Недостатком этого подхода оказалось тоD что в реальном многообразии приемов не удалось найти скольEнибудь хороших принципов отсеченияF Кроме тогоD по мере обучения и увеE личения числа приемов время поиска будет увеличиватьсяF ЭтоD безусловноD создаст @а при плохом отсечении E достаточно скороA сильные ограничения на объем базы приемовD при котором возможна эффективная работа решателяF Q


Второй подход основан на цикле сканирования задачиF Большинство приемовD используемых при решении задачD допускает явное указание такого понятияD что для возможности применения приема необходимо появление этого понятия в задачеF Это позволяет организовать базу приемов по принципу энциклопедииX за каждым понятием логического языка закрепляется сравнительно небольшая группа его приE емовF Как показывает опытD исключение составляет лишь крайне незначительная группа приемовD для которых не выделяется какогоEлибо естественного 4инициалиE зирующего4 понятияF Очередной шаг решения задачи при втором подходе состоит в последовательномD понятие за понятиемD просмотре всего текста задачиD с обращениE ем для каждого текущего понятия к поиску внутри группы его приемовF Эта группа невеликаD и во многих случаях ее можно организовать по древовидному принципуD получая таким образом дополнительное ускорение поискаF Преимуществом данного подхода является тоD что при обучении системы новым разделам мы практически не уменьшаем скорости ее работы на ранее проработанных разделахF Так получается потомуD что 4новые4 понятия не встречаются в 4старых4задачахD и наличие даже очень большого числа 4новых4 приемов никак не сказывается на времени поиска 4старых4D связанных с другими понятиямиF ФактическиD здесь снимаются скольE нибудь сильные ограничения на рост числа приемов и появляется принципиальная возможность создавать гигантские логические системыD имеющие фундаментальное разностороннее образованиеF Именно этот подход и был реализован в логической системе 4Искра4F Таким образомD рабочий цикл решателя состоит в сканировании текста задачи E последовательном просмотре встречающихся в ней понятий и обращении для текуE щего понятия к его программеD объединяющей в себе все закрепленные за понятием приемыF Эта процедура представляет собой чтоEто типа внутреннего 4логического зрения4D обеспечивающего контроль за развитием событийF Как и человекD в проE цессе решения система предпринимает мысленное 4рассмотрение4 объектов задачи и связей между ними для выработки плана ближайших действийF Чтобы выбрать из всех возможных действий наилучшееD необходимо какимEто образом сравнивать между собой результаты применения различных приемов в теE кущем контекстеF Для этого естественно ввести числовые оценки приоритетностиD выбирая каждый разD напримерD прием с наименьшей такой оценкойF Вообще гоE воряD нерационально при сканировании задачи находить все возможные варианты применения приемов и лишь по окончании сканирования отбирать лучший E это может потребовать рассмотрения слишком большого числа вариантовD причем по своей априорной ценности анализируемые варианты тоже будут сильно различатьE сяF К меньшим вычислительным затратам можно прийтиD если разбить все приемы на группы или уровниD объединяя болееEменее равноценныеD и поиск нужного приеE ма вести с последовательным увеличением номера уровняD обрывая егоD как только найден применимый в текущей ситуации приемF ФактическиD здесь оценкой приоE ритетности приема становится номер уровняF Так как обработка каждого уровня приемов требует своего цикла сканирования задачиD то число уровней целесообразE но сделать не очень большимY в решателе это число равно ITD причем как правило срабатывание приема происходит на первых SET уровняхF В действительностиD один и тот же прием может в различных ситуациях относиться к различным уровням E номер уровня определяетсяD в зависимости от контекстаD самой программой приемаF Если этот уровень не соответствует томуD для которого выполняется текущее скаE нирование задачиD то дальнейшие действия по рассмотрению приема обрываютсяD и система переходит к другим приемамF R


Важную роль при сканировании задачи играет управление переключением вниE манияF Вообще говоряD различные элементы описания задачи неравноценны при поE иске очередного приемаF Одни из них находятся в задаче давноD другие E только что занесены либо измененыF Вероятность обнаружить при рассмотрении первых ситуаE циюD требующую немедленных действийD обычно значительно нижеD чем для вторыхF Чтобы учесть такую статистическую неоднородность элементов задачи и уменьшить среднее время поиска приемаD элементы задачи @посылки и условияA снабжаются веE сами E целыми неотрицательными числамиD указывающими номер того уровня скаE нированияD до которого ранее доходило рассмотрение элементаF Как только элемент изменяетсяD его вес уменьшается до HY веса новых элементов также полагаются равE ными HF При сканированииD связанном с приемами i E го уровняD игнорируются все посылки и условияD веса которых больше i E они образуют 4теневую4 часть задачиF По мере прохождения i E го уровня веса тех элементов задачиD для которых не произошло срабатывание приемаD автоматически увеличиваются до i + 1F Как только срабатыE вает какойEлибо прием и возникают элементы задачи с весом HD сканирование задачи возобновляется начиная с нулевого уровняF При этом в 4зону внимания4 попадут только те элементы задачиD которые имеют вес HD тFеF только что были изменены либо введеныF Эта простая автоматика уже обеспечивает в большинстве случаев разумную стратегию переключения внимания и значительно увеличивает быстродействие сиE стемыF В особенности это ощутимо для задач геометрического типаD имеющих сотни посылок и условийF КонечноD необходим ряд дополнительных средствD обеспечиваE ющих переключение внимания в специальных случаяхF Некоторые из этих средств включены в 4общую автоматику4 решателяY другие E реализованы непосредственно в приемахD которые могут избирательно изменять веса различных элементов задачи и таким образом управлять зоной вниманияF В самых общих чертахD процесс обучения компьютерного решателя можно предE ставить происходящим по следующей схемеF Рассматривается некоторая обучающая последовательность задачF Для очередной задачи анализируется траектория ее решеE нияF Она разбивается на простейшие шагиD и формулируются эвристические объясE нения целесообразности текущего шага в текущем контекстеF На основе таких объясE нений программируется прием E программаD которая в аналогичных ситуациях будет выполнять аналогичные действияF Приемы накапливаются в компьютерной моделиD так что в новой задаче некоE торые из них могут сработать и предложить свою версию развития решенияF КажE дое такое срабатывание анализируется на предмет целесообразностиD и в решающие правила приема вводятся необходимые коррективыF Эта процедура повторяется для многих сотен задач предметной области E до тех порD пока сложившаяся система приемов не обнаружит достаточно устойчивого и эффективного поведенияF В целомD процесс напоминает обучение нейросистемы методом 4поощрений и наказаний4Y отE личие состоит лишь в более сложной процедуре коррекцииD которая не сводится к изменению какихEлибо числовых параметровD как у нейрокомпьютераD а требует приE влечения логики для очередного перепроектирования приемовF Обучение логической системы 4Искра4 было предпринято для таких предметных областейD как алгебра множеств и комбинаторикаD элементарная алгебраD элеменE тарная геометрияD математический анализD аналитическая геометрияD дифференциE альные уравненияD комплексный анализD теория вероятностейF Проработаны многие разделы линейной алгебрыD общей алгебрыD дискретной математикиD интегральных уравненийD элементарных физики и химииF Рассматривались нематематические обE ластиX шахматыD понимание естественного языкаD анализ рисунковF Сразу заметимD S


что главным образом изучались стандартные задачи вычислительного характераD хотя и для многих теоретических задач тоже создавались приемыD обеспечивающие их решениеF В некоторых предметных областях @напримерD элементарные алгебра и геометрияA удалось добиться достаточно стабильного решения стандартных задачD в других E лишь предложены объяснения отдельных траекторий решенияF При сравнении с обычными системами компьютерной математики становятся очеE видны преимущества предлагаемого подхода в тех случаяхD когда логика начинает играть существенную рольF По существуD логическую систему 4Искра4 можно расE сматривать как экспериментальную систему компьютерной математики нового типаD допускающую постепенное перерастание в интеллектуальную математическую систеE муF Общее число приемов сейчас превышает RPHHHD число проработанных задач E свыE ше IHHHHF При этомD даже без архивацииD система занимет всего около IPH МбF Это означаетD что стандартные размеры внешнего твердого диска в IТб позволяют увеE личить объем решателя в VHHH разD без существенного замедления его в тех областяхD где обучение уже завершеноF

Алгоритмический язык ЛОС
Следующий важный вопросD возникающий после выбора механизма сканирования задачи как диспетчераD организующего работу базы приемовD E это вопрос о языE ке для записи приемовF В приеме выделяются такие основные частиD как описание ситуацииD в которой логически допустимы реализуемые им действияY описание сиE туацииD в которой эти действия целесообразныD и описание процедурыD собственно реализующей действия приемаF Первые две части предполагают использование некоторого логического языкаD на котором формулируются соответствующие условияF Эти условия относятся не к объектам предметной областиD рассматриваемым в задаче @числамD точкамD вектоE рам и тFпFAD а к тем структурам данныхD с помощью которых задача представлена в системеX к термам логического языкаD вхождениям в эти термыD к спискам термовD к различного рода техническим пометкам и конструкциямD вводимым решателем для управления процессомF Чтобы формулировать такие условияD необходимо обеспечить достаточно богатый набор понятий логического языкаD ориентированных на испольE зуемые в решателе структуры данныхD и прежде всего E на задачи и их элементыF Именно этот набор и составил основную часть нового языка ЛОС @Логический Описатель СитуацийA для записи приемовY чтобы задавать те действияD которые должны быть выполнены приемом в уже 4опознанной4 им ситуацииD оказалось доE статочно присоединить к логической части языка сравнительно небольшое количеE ство кодирующих типовые преобразования конструкцийF После тогоD как на логическом языке сформулирована ситуацияD в которой приE менение приема возможно и целесообразноD необходимо обеспечить некоторый алE горитмD реализующий в задаче поиск этой ситуацииF В описании ситуации должны фигурировать объектыD идентифицированные еще до начала поиска E сама задачаY выделенное в ней при сканировании вхождение понятияY текущий уровень сканироваE нияD и тFпF Описание представляет собой последовательность утверждений P1 , . . . , Pn F Некоторые Pi определяют условия на ранее идентифицированные объектыF Так как все эти объекты относятся к текущим структурам данных решателяD истинность условий проверяется непосредственно и не требует какогоEлибо логического выводаF Для проверки этой истинности в интерпретаторе языка имеются специальные подE T


программыF Другие Pi вводят в рассмотрение новые объектыD связанные заданным образом с уже введенными до этого объектамиF Если такие объекты определяются неоднозначноD то при поиске ситуации необходимо перечислять все возможные вариE антыF При программировании на обычном алгоритмическом языке здесь нужно было бы использовать операторы циклаD причем вложенность циклов была бы равна числу неоднозначно определенных переходов к 4новым4 объектам в цепочке P1 , . . . , Pn F ЧтоE бы избежать таких громоздких конструкцийD в языке ЛОС выделен ряд специальных отношений между объектамиD для которых перечисление реализуется автоматическиF При обработке 4перечисляющего4 утверждения Pi сначала рассматривается первая версия выбора новых объектовD и предпринимается попытка для выбранных объекE тов продвинуться вправо по цепочке P1 , . . . , Pn F Если в некоторый момент дальнейшее продвижениеD ввиду ложности условияD становится невозможнымD то происходит отE кат к последнему 4перечисляющему4 утверждению и определение очередной версии выбора объектовF Этот принцип 4перечисления по умолчанию4 позволяет в качестве исполняемого текста программы ЛОСа использовать само логическое описание искоE мой ситуации и таким образом существенно упростить понимание текста программыF ЗаметимD что из совсем других соображений принцип реализации операторов с перечислением значений их выходных переменных возник в известном алгоритмичеE ском языке ПРОЛОГF В отличие от ЛОСаD ПРОЛОГ изначально ориентирован на работу с объектами предметногоD а не структурного уровняF Поэтому центральное место в ПРОЛОГе занимает логический выводD основанный на процедуре унифиE кацииF Этот логический вывод становится совершенно излишним при работе с элеE ментами структуры данныхD допускающими непосредственную проверку условийD и какогоEлибо аналога его в ЛОСе не предусмотреноF С другой строныD в ПРОЛОГе отсутствует целый ряд важных возможностейD предусмотренных в ЛОСе для эфE фективной работы со сложными логическими описаниями образов 4структурного4 уровня и для использования режима сканирования задачиF ЛОС ориентирован на создание автоматикиD управляющей логическими процессамиD в то время как при разработке ПРОЛОГа эта автоматика осталась почти 4за кадром4F В ЛОСе выделяются следующие основные типы объектовD обрабатываемые проE граммойX IF Символы переменных и логические символыF К последней категории относятся логические связкиD кванторыD константыD символы отношений и операций и тFпF PF ТермыD построенные из переменных и логических символовF Заголовок терма E произвольный логический символD число его операндов E любоеF QF Наборы (a1 , . . . , an ) ранее определенных допустимых объектовF RF Вхождения символов в термы и разрядов в наборыF ФактическиD вхождение E это адрес позиции в терме либо набореF Программа решателя организована по энциклопедическому принципу и распадаE ется на программы отдельных логических символовF Программа логического симE вола имеет древовидную структуру и состоит из совокупности пронумерованных натуральными числами текстовD называемых фрагментами этой программыF КажE дый фрагмент программы логического символа представляет собой последоваE тельность P1 , . . . , Pn операторов ЛОСаF К моменту реализации оператора Pi часть значений программных переменных уже определенаD а часть E еще не определенаF U


Обычно номера определенных переменных образуют начальный отрезок натуральноE го рядаF Оператор либо обеспечивает проверку истинности некоторого условияD либо определяет значения своих @пока не определенныхA выходных переменныхF Иногда определение значений выходных переменных реализуется в режиме перечисленияF При откате к перечисляющему оператору все переменныеD которые были определеE ны после его первой реализацииD снова оказываются не определеннымиF НаконецD оператор может изменять текущие структуры данныхF Связь между фрагментами программы организуются с помощью операторов 4инаE че N 4 и 4ветвь N 4F Первый используется обычным образомX если условие P ложноD то после оператора 4P иначе N 4 будет реализован переход к фрагменту с номером N F Оператор 4ветвь N 4 является вырожденным перечисляющим операторомF При первом попадании на него никаких действий не предпринимаетсяD и выполняется переход к следующему операторуF Если при продвижении по цепочке операторов вправо встретилось ложное условиеD то откат к оператору 4ветвь N 4 вызывает пеE реход к фрагменту с номером N F Данный оператор удобен для склейки начальных частей программ нескольких независимых приемовF Обращение к программе символа бывает следующих типовX IF Обращение из сканирования задачиF Тогда программе передается информация о координатах вхождения текущего символа в задачуF PF Обращение при реализации программы вспомогательного оператора либо опеE раторного выраженияD написанной на ЛОСеF Тогда текущий логический символ E заголовок программируемого программного термаF QF Обращение при обработке справочного запросаF Такие обращения оказываются нужныD чтобы разбросать характеризующую логические символы информацию заданного типа по программам конкретных символовF НапримерD информациюD уточняющую тип значений операцииD либо число ее операндовD и тFпF Для уточнения типа обращения имеются соответствующие операторыF В качестве простого примера рассмотрим программу приемаD усматривающего в задаче утверждение вида 4или@A1 . . . P . . . ѓ(P ) . . . An A4 и заменяющего его на конE станту 4истина4F Эта программа имеет видX 4операнд@хP хTA символ@хT неA операнд@хP хUA равныетермы@первыйоперанд@хTAхUA заменавхождения@хP хQ хR хI истина пустоесловоA4F Программа относится к символу 4или4D причем при обращении к ней значением переменной хP является вхождение данного символа в текущий терм задачиF ОпеE ратор 4операнд@хP хTA4перечисляет всевозможные операнды дизъюнкцииD присваиE вая их вхождения переменной хTF Оператор 4символ@хT неA4 отфильтровывает лишь те операндыD заголовком которых служит символ 4не4F Таким образомD хT будет идентифицироваться с вхождением операнда 4ѓ(P )4F Оператор 4операнд@хP хUA4 выполняет повторный просмотр операндов дизъюнкцииF НаконецD оператор 4равE ныетермы@первыйоперанд@хTAхUA4 отфильтровывает те хUD которые суть вхождения утверждения P F Завершающий оператор реализует замену дизъюнкции на константу 4истина4F В этом примере оказались 4спрятаны4 два оператора циклаD соответствуE ющих выделению первого и второго операндовF Если расписать их явным образомD то программа оказалась бы более длинной и менее понятнойF V


Еще одна интересная особенность ЛОСа E использование кванторов в качестве операторов алгоритмического языкаF НапримерD оператор 4длялюбого@хP если вхоE дит@хP хIA то заголовок@хP илиAA4 проверяетD что каждый элемент набора хI имеет своим заголовком символ 4или4F Оператор 4существует@хP и@подчинено@хI хPA симE вол@хP синусAAA4 проверяетD что текущее вхождение хI расположено внутри термаD имеющего своим заголовком символ 4синус4F В обоих случаях мы имеет 4спрятанE ный4 циклF Если реализовать его традиционным образомD то понимание смысла опеE ратора затруднитсяF При программировании со 4спрятанными4 циклами длина программ существенE но уменьшаетсяD и становится сравнительно простым непосредственное их чтениеF Режим перечисления сильно упрощает также программирование на ЛОСе перечисE ляющих процедур рекурсивного характераF Чтобы еще больше упростить работу с программами ЛОСаD предусмотрен ряд средств интерфейсаD компенсирующих проE чие недостаткиF ВпрочемD в действительности ЛОС оказывается лишь языком промеE жуточного уровняD редко используемым при обучении решателяF Обычно программы на ЛОСе пишет компиляторF ЛОС E программы выполняются интерпретаторомD реализованным на СИF Это обеспечивает возможность автоматического перепрограммирования системой самой себя в процессе решения задачF Все интерфейсы системы тоже реализованы на ЛОСеF

? Язык для записи приемов ГЕНОЛОГ
Как правилоD значительную часть программы приема на ЛОСе составляет описаE ние вида тех утверждений или выраженийD которые могут быть идентифицированы с фрагментами заданной теоремы предметной областиF На практике редко бываE ет такD чтобы идентифицируемые логические конструкции в точности совпадали с темиD которые имеются в теоремеF НапримерD при идентификации квадратного трехE члена ax2 + bx + c коэффициент a может оказаться равным единицеD и тогда в задаче вместо произведения ax2 будет записана степеньY сама эта степень может не иметь в точности вида квадратаD а лишь иметь четный коэффициент показателя степеE ниD и тFдF ЧтобыD несмотря на эти различияD идентифицировать теоремуD приходитE ся фактически в программе приема описывать не ее видD а вид некоторого класса теоремD получающихся из нее различными вариациямиF В результате текст програмE мы оказываетсяD воEпервыхD весьма громоздкимD иD воEвторыхD достаточно удаленE ным от исходной записи теоремыF Еще большую громоздкось этому тексту придают различные вставкиD связанные с решающими правилами приемаF ПоэтомуD несмотE ря на все предоставляемые ЛОСом и интерфейсом его редактора возможности для быстрого чтения и понимания логических описаний ситуацийD все же в скольEнибудь невырожденных случаях описания приемов оказываются трудночитаемымиF ЗамеE тимD что хотя ПРОЛОГD казалось быD и ориентирован на запись программы в виде совокупности теорем предметной областиD однако он тоже не позволяет преодолеть указанную трудностьF Если теоремы идентифицируются без учета возможных вариE ацийD то программа оказывется заведомо слабойY если начинается их учетD то и на ПРОЛОГеD для задания общего вида класса теоремD придется от предметного уровE ня перейти к структурному @к которому ЛОС более приспособленAD и таким образом полностью утратить наглядность исходного текста теоремыF Чтобы восстановить утерянную при погоне за эффективностью работы програмE мы приема наглядность и компактность записиD был создан новый языкD уровень коE торого существенно вышеD чем у ЛОСа или ПРОЛОГаF Прием на этом языке задается W


как теорема предметной областиD снабженная некоторой 4алгоритмизирующей4 разE меткойF На основе разметки компилятор осуществляет необходимое обобщение вида теоремыD формулирует описание на ЛОСе ситуацийD в которых она должна быть примененаD и добавляет к нему операторы ЛОСаD реализующие применениеF ФакE тически этот язык имеет два независимых логических уровняX предметный уровеньD на котором представлена теоремаD и структурный уровеньD на котором формулируE ются условия целесообразности применения теоремыF Оба эти уровня предполагают использование полноценного логического языкаD однако логические записи структурE ного уровняD в отличие от записей уровня предметногоD не участвуют в какомEлибо логическом выводе E они используются только для проверки условий при приняE тии решенияF Роль 4алгоритмизирующей4 разметки приема весьма разнообразна E это и указание способа применения теоремыD и определение необходимых правил ее обобщенияD и указание условий целесообразности примененияD и уточнение алE горитмических средствD используемых для обработки посылок теоремыD и указание на 4технические4 сообщенияD передаваемые при срабатывании данного приема друE гим приемамD и указатели переключения вниманияD и многое другоеF Эта разметка представляет собой чтоEто вроде генотипа приемаD элементы которого допускают независимое варьирование в достаточно широких пределах и по которому компиляE тор создает фактически реализуемую программу приема на ЛОСеF Такая аналогия ? позволила назвать новый язык ГЕНОЛОГом @ГЕНетический язык ЛОГического проE граммированияAF ? Описание приема на ГЕНОЛОГе оказалось значительно более компактным и поE нятнымD чем на ЛОСеF На экране изображается в стандартной математической запиE си теорема приемаD под которой размещается в нескольких окнах сопровождающая теорему информацияF Во многих случаях эта информация занимает всего несколько строчекD в то время как текст создаваемой компилятором программы на ЛОСе соE ставляет несколько полных экрановF Трудоемкость чтения приема и его коррекцииD по сравнению с ЛОСомD уменьшилась на порядокF ? В отличие от обычных языков программированияD ГЕНОЛОГ не представляет собой скольEнибудь завершенного явленияF По существуD он является коллекцией типовых алгоритмических конструкцийD используемых при переходе от теоремы к программеF Эта коллекцияD достаточно богатая на текущий моментD продолжает @хоE тя все реже и режеA пополняться при рассмотрении новых предметных областейF СоответственноD при переходе к новой предметной области обычно приходится заE ? трачивать некоторые усилия на развитие компилятора ГЕНОЛОГаF Как показывает опытD эти затраты несопоставимо малы в сравнении с той последующей экономиейD ? которую дает применение ГЕНОЛОГа при обучении решателя в данной областиF Описание приема на ГЕНОЛОГе состоит из следующих компонентX IF Теорема предметной областиD на которой основан приемF Эта теорема вводится при помощи формульного либо текстового редактораD в стандартной матемаE тической либо скобочной записиF Для большей наглядности предусмотрено соE провождение теорем с геометрическими объектами чертежомY компилятор этот чертеж никак не используетF ЗаметимD что хотя ГЕНОЛОГ и приближен к логическому языку предметной областиD все же он представляет собой язык программированияF Настоящие теоE ремы предметной области содержатся в базе теоремF В теореме приема же доE пустимы @как правилоD небольшиеA отклонения от логических стандартов предE метного уровняF Эта теорема обычно преобразуется к видуD более удобному для IH


практического использования E напримерD в посылках могут вводиться вспоE могательные обозначения для объектовD упоминаемых в утверждении теореE мыY часть посылокD которые в обычных 4разумных4контекстах автоматически бывают выполненыD отбрасываетсяD и тFпF В особых случаях теорема приема вообще может представлять собой техническую заглушку E 4псевдотеорему4F PF Заголовок приемаF Он указывает на общую схему использования теоремы в приеме @напримерD тождественная замена слева направоY вывод следствия и тFпFAF QF Список фильтров приемаF Элементы этого списка суть сформулированные с помощью несколько модифицированного логического языка условия на целесоE образность применения приема в текущем контекстеF Это E второй логический уровень описания приемаY первым уровнем является сама теоремаD также заE даваемая на логическом языкеF ОднакоD в случае теоремы логический язык используется для описания ситуаций на предметном уровнеD а в случае фильE тров E для описания ситуаций на структурном уровнеF В этом он близок ЛОE Су и может рассматриваться @с рядом существенных оговорокA как 4ЛОС в теоремных переменных4F В действительности многие операторы ЛОСа имеют своих одноименных двойников в языке фильтров приемовD хотя эти двойники используются уже поEдругому E у них часто отбрасываются однозначно восE станавливаемые из контекста описания приема операндыF Кроме тогоD в языке фильтров приема возникают конструкцииD совершенно не имеющие аналогов в ЛОСеF RF Список указателейD адресуемых компилятору @далее называем их просто указаE телями приемаAF Элементы этого списка уточняют способ формирования ЛОСE программы приема компилятором ГЕНОЛОГаF По существуD это основная часть 4генотипа4 приемаF Здесь уточняютсяX средстваD используемые для усмотрения в задаче 4замаскированных4 возможностей применения теоремыY способы обE работки отдельных посылок теоремыY технические комментарииD вводимые в задачу либо удаляемые при применении приемаY логика переключения внимаE ния после применения приемаD и дрF SF Список нормализаторовF При формировании результирующих @включаемых в структуру данных задачиA либо вспомогательных @рассматриваемых в процессе работы приемаA термов могут применяться процедуры для их упрощения лиE бо какихEлибо иных специальных преобразованийF Такие процедуры задаются последовательным применением нормализаторов E либо специальных пакетов приемов для тождественных и эквивалентных преобразованийD либо вспомогаE тельных задачF Использование небольшого пакета приемов вместо общей базы приемовD активизируемой при сканировании задачиD во многих случаях на поE рядок ускоряет вычисленияF Эти 4локальные4 приемы отличаются от приемов сканирования задачи E они применяются не в контексте задачиD а в некотором другом специальном контекстеD состоящем из преобразуемого термаD списка поE сылокD в предположении истинности которых ведутся преобразованияD и списка технических комментариевF Задаются ониD как и приемы сканирования задачD на ГЕНОЛОГеF Специальный интерфейс позволяет достаточно быстро вводить обращения к нормализаторам путем указания в теореме @либо в сопровождающих теорему II


термах описания приемаA подлежащих нормализации точекF В результате исE пользования нормализаторов и вспомогательных процедур обработки посылок теоремыD срабатывание приема оказывается иногда чрезвычайно сложным выE числительным процессомD основанным не на единственной теореме предметной областиD а на десятках и даже сотнях @с учетом прменяемой рекурсииA различE ных теоремF TF Шаблоны сопровожденияF Здесь хранятся текстEформульные шаблоныD испольE зуемые при создании текстовD объясняющих срабатывания приемовF Способ их применения регламентируется специальными указателями приемаF Для примера описания приема по данной схемеD рассмотрим простейший прием реE шения уравнения ax = bF Теорема приема имеет в этом случае видX

abx(число(a) & число(b) & число(x) (ax = b (ѓ(a = 0) & x = b/a) (a = 0 & b = 0)))
Заголовком приема служит логический символ 4второйтерм4D указывающийD что теоE рема будет применяться для эквивалентной замены слева направоF Фильтры приема указывают следующий контекстD в котором выполняется заменаX IF Тип решаемой задачи E на описаниеY PF Преобразуемое равенство входит в условие задачиD причем это вхождение E корневоеY QF Текущий уровень сканированияD при котором происходит срабатывание приемаD равен IY RF Выражение b не содержит неизвестных задачиD а x E содержитF Указания компилятору уточняют следующие подробностиX IF Переменная x идентифицируется как совокупность всех множителей рассматE риваемого произведенияD содержащих неизвестные задачи @это автоматически предопределяетD что переменная a будет идентифицирована с выражением без неизвестныхAY PF При идентификации выражения ax возможен учет стоящего перед ним знака 4минус4D который относится программой приема к коэффициенту aY QF Посылки теоремы проверяются при помощи специального пакета приемовD обесE печивающего быстрое усмотрение условий вида 4число@. . .A4F В приеме используются следующие обращения к нормализаторамX IF Предпринимаются обращения к вспомогательному пакету приемов для разлоE жения на множители выражений a, bF Если такие разложения не находятся сраE зу жеD до преобразования рассматриваемого уравненияD то впоследствии может возникнуть разбор случаевD приводящий к дублирующим попыткам разложеE ния на множители в различных подслучаяхY IP


PF Выполняется обращение к пакету стандартизации дробных выражений для выE ражения b/aF Этот пакет состоит из нескольких десятков простых продукцийD выполняющихD в частностиD сокращение дробейD деление и умножение дробных выраженийD учет констант H и ID и тFпFY QF Для уравнений a = 0, b = 0 выполняются обращения к пакетам приемовD станE дартизирующим уравнения данного вида @сокращение левой части на множитеE лиD не обращающиеся в HY усмотрение тождественной ложностиY преобразование равенства нулю произведения в дизъюнкцию равенств нулю сомножителейD и тFпFAY RF К заменяющей дизъюнкции применяется пакет общелогических приемов @устраE нение логических констант 4истина4 и 4ложь4Y стандартизация конструкций с логическими связками и кванторамиAF В результате выполнения указанных преобразований заменяющий терм в данном приеме приобретает достаточно устойчивый видD не вызывающий немедленного сраE батывания цепочки простейших нормализующих приемовF ЗаметимD что трудоемE кость одного цикла сканирования задачи обычно возрастает пропорционально сумE марной длине находящихся в активной области ее термовD а всего времени решения задачи E пропорционально квадрату средней такой длиныF Поэтому вынесение во вспомогательные задачи преобразований подтермов сложного выражения приводитD если эти преобразования достаточно интенсивныD к значительному ускорению решеE ния задачиF СоответственноD стандартом программирования на ГЕНОЛОГе является как можно большее использование нормализаторовF ПриемыD применяемые при сканировании задачиD могут обращаться к вспомогаE тельным процедурам E так называемым пакетным операторамF Эти операторы предE ставляют собой небольшие группы приемовD записываемых на ГЕНОЛОГе и комE пилируемых в программы ЛОСаF В приеме пакетного оператора допускаются обE ращения к другим пакетным операторам и рекурсивные обращенияF Использование пакетных операторов позволило существенно ускорить работу решателяF Имеются R основных типа пакетных операторовD аналогичных R основным типам задач @на доказательствоD описаниеD преобразование и исследованиеAX IF Аналогом задачи на доказательство является проверочный операторD получаE ющий в качестве входных данных проверяемое утверждение @точнееD набор выE раженийD подставляемых вместо переменных в шаблонD задающий вид такого утвержденияAY список посылокD в предположении истинности которых провоE дится проверкаD а также список комментариев управляющего характераF ПомиE мо проверки истинностиD проверочный оператор также выдает список посылокD фактически использованных при проверкеF Пример проверочного оператора E оператор 4усмменьше4D получающий в качестве входных данныхX выражения a, bD для которых проверяется условие a < bY список посылокD в предположении истинности которых происходит проверкаY набор комментариев @в частностиD в нем могут содержаться ограничения на применяемые при проверке средстваAF PF Аналогом задачи на описание является пакетный операторD названный синE тезаторомF Он предназначен для решения задач на описание с единственным условиемD имеющим строго ограниченный видD определяемый некоторым шабE лономF Часть переменных шаблона выделена как 4известные4D а часть E как IQ


4неизвестные4F Синтезатор определяет значения неизвестныхD получая в качеE стве входных данныхX набор выраженийD подставляемых вместо 4известных4 переменных в шаблонY список посылокD в предположении истинности которых предпринимается подбор значений неизвестныхD и набор комментариевD имеE ющих управляющий характер @целевая установка и тFпFAF Результатом работы синтезатора служат набор искомых значений неизвестных и список фактичеE ски использованных посылокF В зависимости от своего типаD синтезатор либо находит единственный пример допустимых значений неизвестныхD либо переE числяет такие примерыF Пример синтезатора E оператор 4верхняяоценка4D реаE лизующий утверждения вида a x для известной переменной a и неизвестной xD который перечисляет представляющие интерес @с учетом комментариевA конE стантные верхние оценки x выражения aF QF Аналогом задачи на преобразование является пакетный операторD названный нормализаторомF Он получает в качестве входных данных преобразуемый терм @выражение либо утверждениеAD список посылокD в предположении истинности которых выполняются преобразованияD и набор комментариевD имеющих управE ляющий характерF Прием нормализатора выполняет некоторое преобразование его 4условия4F Это преобразование @в зависимости от предназначения нормалиE затораA не обязательно должно быть тождественным @напримерD при получении асимптотической оценки какогоEлибо выраженияAF В отличие от проверочного оператора и синтезатораD представляющих собой операторы ЛОСаD нормалиE затор является операторным выражением E его значением служит возникший после цепочки преобразований термF Пример нормализатора E операторное выE ражение 4нормдробь4D осуществляющее общую стандартизацию дробных выE ражений @отбрасывание знаменателя ID деление дробиD деление на дробьD выE несение минуса из числителя либо знаменателяD и тFпFAF RF Аналогом задачи на исследование является пакетный операторD названный анаE лизаторомF Он обрабатывает копию списка посылок текущей задачи Z D оформE ленную в виде вспомогательной задачи на исследование Z F Анализатор не обE ращается для сканирования Z к основной базе приемовD а использует свои собE ственные приемыF Так как их существенно меньшеD то удается за сравнительно небольшое время получить значительное число следствийF Иэ этих следствий отбираются лишь ценные для внешней задачи Z D которые по окончании рабоE ты анализатора переносятся в ее список посылокF Обращение к анализатору обеспечивается специальными приемамиD указывающими лимит времени его работыF Передача отобранных утверждений происходит по исчерпании этого лимитаF При получении особо важных следствий возможен немедленный обE рыв работыF Перечисленные пакетные операторы предназначены для работы с логическими структурами данныхF ОднакоD ГЕНОЛОГ можно использовать и для создания проE граммD работающих с 4обычными4 техническими структурами данных E числамиD массивамиD таблицами и тFпF Эти программыD разумеетсяD тоже имеют своими исE точниками теоремы или группы теоремD так что естественным образом возникает задача компиляции их непосредственно с теоремного уровняF Для задания нелогиE ческих вычислений на ГЕНОЛОГе используются так называемые вычислительные пакетыF IR


ГЕНОЛОГ является языком пограничного слоя между теоремами и алгоритмамиF Так как все программы E логические либо традиционные вычислительные E возниE кают в конечном счете из теоремD то ГЕНОЛОГ или подобные ему языки приобE ретают универсальный характерF Они должны будут присутствовать в любой самоE программирующейся системеF Поэтому запись на ГЕНОЛОГе даже давно известных алгоритмов оказывается вполне оправданнойF Она позволяет проследить логические источники программ и приближает к подлинной автоматизации программированияF

Анализатор решений
Интерфейс логической системы позволяет прослеживать ход решения задачи по шаE гамF Прием можно сопровождать текст E формульным шаблономD с помощью коE торого на экран выдаются пояснения смысла выполняемых действийF Несмотря на этоD полная трассировка действий решателя на семантическом уровне обычно переE гружена множеством излишних шаговF Она отображает не столько решение задачиD сколько процесс его поискаF Чтобы отбрасывать ненужные действия и оптимизиE ровать оставшиесяD предусмотрен режим решения задачи с сохранением протокола срабатываний приемовF По окончании решения предпринимается анализ протоколаX создается граф использования промежуточных результатовD и выдается сокращенная последовательность действийD в которой отброшены не использованные логические выводыF Такой режим назван анализатором решенийF Он создает предпосылки для последующей оптимизации цепочки рассуждений с точки зрения ее простоты и наE глядностиF Анализатор решений полезен также как отладочное средствоD ибо дает возможность прослеживать траекторию решения в обоих направлениях и получать различные статистические данные об этой траекторииF ВероятноD анализатор решений можно будет использовать и для оптимизации отE дельных приемовF ОднакоD попытки изменить прием для сокращения решения одной задачи обычно приводят к ухудшению хотя бы части решений других задачF ПоэтоE му основным источником оптимизации приема оказывается анализ его поведения на всем подразделе задачникаF

База объектов
Логические процессы интеллектуальной системы взаимодействуют с внешним миром через различные нелогические структуры данныхX битмэпы изображенийD численные массивыD схемыD таблицыD тексты естественного языкаD географические картыD комE пьютерные программыD планы действийD технические проектыD задания на проектиE рование и тFпF Часть этих структур данных имеет статический характер и пополняет общие знания системы о внешнем миреD часть E динамически изменяется и позвоE ляет системе реагировать на текущие процессы окружающей средыF Для представE ления в логической системе такой 4нелогической4 информационной среды создана структураD названная базой объектовF Технически она организована в виде оглавE ленияD концевыми пунктами которого служат различные технические конструкцииX числаD многочленыD численные массивыD наборы и таблицыD сетевые объектыD фрагE менты синтезируемых либо анализируемых СИEпрограммD шахматные позиции и дрF В оглавлении выделен разделD через который решатель может работать с файлами произвольной природыD помещенными в поддиректорию pvF Пока база объектов представляет собой заготовку для будущего подключения логики решателя к приE кладным задачамF На текущий момент созданы лишь простейшие интерфейсы для IS


ввода объектов перечисленных типовF Предусмотрен также интерфейс для создания ссылки на объект из хранящейся в задачнике задачиF Он позволит работать с базой объектов в полуавтоматическом режимеD выполняя с помощью решателя различные операции над ее элементамиF По мере обучения системыD эти операции будут укрупE нятьсяF Проработаны простейшие задачиD связанные с сетевыми даннымиD хранящиE мися в базе объектов E поиск кратчайшего пути в графе и определение максимального потока через сетьF Программы для работы с сетями реализованы на ГЕНОЛОГеF

Усиленный режим решения задач
Процесс решения задачи человеком редко имеет прямолинейный характерF После первойD зачастую неудачнойD попытки решить задачу 4в лоб4D предпринимается возE вращение к исходному условию и реализуются повторные попыткиD в которых кажE дый шаг анализируется более глубоко и связан с привлечением дополнительных средствF ФактическиD на каждом шаге здесь имеет место определенный переборD наE правленный на усмотрение какогоEто локального выигрышаF Трудоемкость перебора на повторных попытках может достигать весьма значительной величиныD а привлеE каемые средства могут оказаться весьма удаленными от исходных понятий задачиF Иногда для решения задачи приходится временно отвлекаться от нее и развивать примыкающие разделы теорииF СоответственноD и при обучении решателя нет смысла ограничиваться только лоE бовым подходом к решению задачиF ВпрочемD при первичном обучении проще всего начинать всеEтаки именно с негоF Когда эксперт разбивает ход решения задачи на шаE гиD ему уже известны все подводные камни предметной областиD и вполне естественE ным является желание вводить такие приемыD срабатывание которых являлось бы хорошо мотивированнымF К сожалениюD часто хорошо мотивированным оказывается применение сразу целого блока логических переходовD в то время как мотивировка отдельных шагов внутри блока трудно объяснимаF В результате появляются приеE мыD имеющие характер 4заготовок4 для специальных ситуацийF В задачниках это явление хорошо известноX предыдущая задача иногда может рекомендоваться как прием для решения следующейF ЕстественноD ее имеет смысл запомнить и сохранить в базе приемов решателяF Такое накопление 4стандартных заготовок4 может выгляE детьD как некоторый обманD однако он подсказан самой логикой усиления лобового режима решателяF Результатом оказывается существенное ускорение получения отE ветов для стандартных задачF Оправданием может служить и тоD что эксперты тоже обычно располагают большим запасом стандартных заготовок и сразу усматривают их в задачахF С другой стороныD решатель все же должен справляться с задачами и без искусE ственных заготовокD которые для всех случаев жизни заранее запасти в базе приемов не удастсяF Поэтому какиеEто слабо мотивированные приемы ему нужныF Чтобы подE ключить их к решению задачиD имеются две возможностиF Первая E поднять уровень срабатывания слабо мотивированных приемовF В обE щемD иногда это удается сделать безболезненноD и за счет таких приемов решаются многие задачиF ОднакоD здесь имеются две трудностиF Первая заключается в томD что на высоких уровнях срабатывания часто размещаются и сильно мотивированE ные действияF Они попадают туда изEза проблемD связанных с переключением вниE манияX проще бывает не понижать веса посылок для обеспечения срабатывания приE емаD так как это всегда притормаживает процесс решенияD а продублировать приемD чтобы он мог сработать и на высоком текущем уровне сканированияF В этой ситуаE IT


ции поднятые даже на очень высокий уровень слабо мотивированные приемы будут сильно 4зашумлять4 работу системыF Вторая трудность заключается в томD что иноE гда локальный переборD использующий слабо мотивированные переходыD необходимо применять в самом начале решения задачиF Он позволит найти какойEто ключевой моментD без которого стандартными средствами задача быстро окажется заведенE ной в тупикD и тогда подключение того же перебора на последующих этапах уже не поможетF Вторая возможность подключения слабо мотивированных приемов заключается в томD чтобы после неудачной лобовой попытки решения возвратиться к исходной формулировке задачи и повторить попыткуD разрешая теперь пользоваться дополниE тельными приемамиF Такие приемы не должны предпринимать какихEлибо скоропаE лительных изменений задачиD тем более слабо мотивированныхF ОднакоD они могут обращаться к различного рода циклам локального перебора для поиска очередного 4сильного4 хода решенияF Внутри этих циклов и будут допускаться слабо мотивироE ванные попыткиF Данный режим решенияD в отличие 4обычного4 лобового режима решателяD будем называть усиленнымF Хотя пока рассматривается только один уроE вень усиленияD впоследствииD видимоD понадобится целая шкала таких уровнейD с постепенным подключением все более мощных дополнительных средствD но и со все более медленным временным масштабом процессовF Еще раз подчеркнемD что смысл усиленного режима состоит не в ослаблении фильтрации срабатываний приемов E такое ослабление сделает систему неспособной решать даже простые задачиF Эффект усиления достигается за счет более осмотE рительногоD с анализом на достаточно большую глубинуD каждого отдельного шага преобразований задачиF Хотя эти шаги могут оказаться весьма трудоемкими и в разы замедлят решение задачиD но замедление не будет иметь экспоненциального характераD а списки посылок и условий не окажутся захламлены огромным числом ненужных утвержденийF Развитие усилителя было начато на примере геометрических вычислительных задачF Чтобы подключить усиленный режимD вводится комментарий 4усиление4 к посылкам исходной задачиF Он может появитьсяD если изначально задача из задачE ника имела в качестве дополнительной посылки символ 4усиление4D либо если имел место откат к повторной попытке после неудачной лобовой попыткиF Для геометриE ческих задач такой откат предпринимается автоматически E если был получен отказ либо если был превышен заданный лимит трудоемкостиF Наиболее эффективным средством усиления решателя в планиметрии оказались пакетные анализаторыF Они получают в качестве входного данного копию текущей задачи на исследование и преобразуют ее с помощью собственного списка приемовD существенно меньшегоD чем вся база приемов сканирования задачF Это обеспечиваE ет значительное ускорение и позволяет провести перебор на сравнительно большую глубинуF Источником усиления здесь является ограничение применяемых средствF В одном анализаторе акцент делается на применение теоремы косинусовD в другом E на анализ равных углов и фигурD в третьем E на соотношения пропорциональностиD и тFдF Обращения к пакетным анализаторам реализуются приемами сканирования задачD срабатывающими на различных уровняхD в том числе на совсем маленькихF По мере повышения уровня увеличиваются ресурсыD отводимые на попытку обращеE нияF При завершении работы анализатора в его списке посылок отбираются новые ценные фактыD которые переносятся в список посылок текущей задачиF Таким обраE зомD несмотря на большое количество выводимых анализаторами вспомогательных утвержденийD размеры списка посылок основной задачи растут умеренным образомF IU


При первичном обучении решателя планиметрическим задачам было создано знаE чительное число приемовD имеющих характер искусственных 4заготовок4F ВпоследE ствии те задачиD ради которых они создавалисьD были переработаны для усиленного режимаD уже без подобных заготовокF РазумеетсяD время решения при этом значиE тельно увеличилосьF ВсеEтакиD подавляющее большинство отказов решателя оказалось связано не с увязанием в перебореD а с отсутствием на текущий момент одного E двух простых приE емовD легко извлекаемых из обычной теорииF Поэтому главными средствами усилеE ния являютсяD воEпервыхD заблаговременное создание достаточно полной коллекции простейших приемовD иD воEвторыхD пополнение этой коллекции в процессе решения задачиF Чтобы получить такое усилениеD необходим анализ цепочки превращений на пути от теоремы к приемуF

Логический ассемблер
Ручное обучение решателя дает огромный материал для анализа процессов извлечеE ния приемов из теоремF ОднакоD этот материал чрезвычайно сыройX каждый прием решателя был подсказан контекстом одной или нескольких конкретных задачD и ниE каких попыток стандартизации приемов не предпринималосьF Как следствиеD приеE мы иногда оказывались слишком частнымиD иногда E неоправданно общимиD а в ряде случаев и вовсе неадекватнымиD так как задачу следовало решать совсем другими средствамиF Помимо не очень высокого качества работы решателяD такое положение вещей создало принципиальные трудности для автоматического синтеза приемовF Поэтому следующим этапом работыD необходимым для выхода на новый техноE логический уровеньD оказалась переработка всей базы приемовD ориентированная на создание единой системы стандартных типов приемовF Как и многим другим естеE ственным наукамD начинавшимся с общей классификации изучаемых объектовD науE ке о логических процессах тоже приходится начинать с такого этапаF ВпрочемD речь здесь идет не просто о классификацииD а о создании языка для задания приемовD имеE ющего более высокий уровеньD чем ГЕНОЛОГF В то времяD как ГЕНОЛОГ подробно описываетD каким образом теорема применяется при решении задачиD новый язык определяет приемD сопровождая теорему лишь указанием той целиD ради которой она применяетсяF Это достигается заданием типа приема и нескольких уточняющих параметров @термовD переменных и тFпFA Каждый тип предполагает свой конкретный набор параметровF Ситуация до некоторой степени напоминает язык ассемблераD где вместо типа приема имеется тип операцииF Поэтому новый язык получил название логического ассемблераF Само задание приема на данном языке названо его специE фикациейF Для развития логического ассемблера был создан несложный интерфейсD позвоE ляющий пролистывать базу приемов и выполнять предварительную их классифиE кацию E выявление типов приемовF Предпринят также предварительный цикл проE листывания этой классификации и ее уточненияF Если удавалось найти более естеE ственную траекторию решения задачиD сомнительные приемы отбрасывалисьF Часть приемов была скорректирована для стандартизации и уменьшения числа типовF При этом преследовалась цель сохранения лишь достаточно сильно мотивированных дейE ствийF Система типов организована древовидным образомX для заданного типа иноE гда рассматриваются его подтипыD имеющие более сильную мотивировку срабатыE ванияF Это необходимоD чтобы решатель мог адаптироваться к предметной областиD выбирая для каждого приема свой необходимый уровень мотивированностиF IV


На текущий момент в системе зарегистрированы IQQS типов приемовF Из них лишь UWW типов связаны более чем с одним приемомD SWH E более чем с двумяD и PPR типа E не менее чем с десятьюF ВероятноD в процессе дальнейшей проработки многие 4одноразовые4 типы будут исключеныD прочие E уточненыF ВпрочемD имеется достаточное количество типов приемовD которые были введены ради единственного приемаD ноD безусловноD необходимыF Приведем несколько десятков выбранных наугад примеров типов приемовF КажE дая спецификация состоит из терма 4тип@AA4D указывающего тип приема AD и нескольE ких сопровождающих термов либо символовF Здесь A E логический символD выбираеE мый для ссылок на тип приема достаточно случайным образомF В оглавлении типов приводится текстD поясняющий смысл соответствующих действийF Далее вместо наE звания типа A будем приводить лишь поясняющий текст из оглавленияF IF Общая стандартизация выраженияF Теорема приема представляет собой тождествоD применяемое для общей станE дартизации выражений в любых ситуацияхF Заменяемая и заменяющая чаE сти тождества не имеют связанных переменныхF Дополнительный элемент спеE цификации 4направл@N A4 уточняет направление замены @слева направо либо справа налевоAF Пример приема данного типаX

ab (a b a b = b)
PF Исключение описателя 4класс4F Теорема приема E тождествоD в заменяемой части которого расположено выE ражение вида setx A(x)D а заменяющая не имеет связанных переменныхF Здесь setx A(x) E множество всех элементов либо наборов xD удовлетворяющих услоE вию A(x)F Направление замены уточняется элементом 4направл@. . .A4F Пример приема данного типаX

f A (setx (x hom(f ) & f (x) A) = прообраз(f , A))
QF Непосредственное определение характеристики отображенияF Теорема приема E тождествоD в заменяемой части которого расположено выраE жение вида f (x (t(x), A(x)))D а заменяющая не имеет связанных переменныхF Здесь x (t(x), A(x)) E функцияD определенная на множестве всех значений xD удовлетворяющих условию A(x)D причем значение ее определяется выражением t(x)F Направление замены уточняется элементом 4направл@. . .A4F Пример приеE ма данного типаX

abcdf (образ(x (arctg x, f (x)), [a, b]) = [arctg a, arctg b])
RF Сведение операции над семейством к операциям над семействамиD имеющими более простой вид общего членаF Теорема приема E тождествоD позволяющее выносить константные подвыражеE ния за знак операции над семействомF Единственный дополнительный элемент спецификации E 4направл4F Пример приема данного типаX

af gh (
x,f (x)

ag (x) =a h(x)

x,f (x)

g (x) ) h(x)

IW


SF Применение нормализатора общей стандартизации для вычисленияF Теорема приема имеет вид xy (x = t(y ) t(y ) = x)F Здесь x E переменнаяD y E набор переменныхD t(y ) E выражениеD для которого соответствующий нормалиE затор общей стандартизации обеспечивает 4вычисление4 его значенияF АнтецеE дент теоремы реализует обращение к данному нормализаторуD и далее t(y ) заE меняется на xF Спецификация имеет элемент 4направл@. . .A4D а также элементD уточняющий вид выражения t(y )D для которого гарантирована возможность вычисленияF Пример приема данного типаX

abc (c = a Ч b a Ч b = c)
Здесь Ч E прямое произведение множествF Дополнительные условия на вид заE меняемого выражения состоят в томD что a и b имеют вид конечных списков {p1 , . . . , pk }F В этой ситуации нормализатор 4нормпрямоепроизведение4 преобE разует выражение к виду конечного списка парF TF Переход в задаче на преобразование к уже имевшимся подтермамF Теорема приема E тождествоD позволяющее таким образом проварьировать 4сложE ное4 подвыражение условие задачи на преобразованиеD что новая его версия уже встречается в другой части условияF Спецификация имеет элемент 4наE правл@. . .A4D элемент 4исключение@t1 A4D указывающий на исключаемое сложное подвыражение t1 D и элемент 4терм@t2 A4D указывающий новую его версиюF ПриE мер приема данного типаX

abcd (0 < a a

d logb c

=c

d logb a

)

Тождество применяется слева направоF Исключается выражение logb cD вводитE ся новая его версия logb aF ПроверяетсяD что она уже встречается в условии задачиF Для блокировки обратной замены вводится специальный комментарийF UF Сокращенная переформулировка выражений при завершающем редактироваE нииF Теорема приема E тождествоD позволяющее переформулировать выражение боE лее компактным образом перед выдачей ответаF ПредполагаетсяD что применеE ние его на более ранних этапах решения задачи либо противоречит используE емой на этих этапах стандартизацииD либо не представляет особой ценностиF Единственный дополнительный элемент спецификации E 4направл@. . .A4F ПриE мер приема данного типаX

abcde (a - рациональное & ѓ(числитель(a) - четное) & ѓ(знаменатель(a) - четное) -(b - c)a d/e = (c - b)a d/e)
Этот прием позволяет 4втягивать4 внешний минус в сомножитель числителяD имеющий вид разностиF Он применяется только при редактировании ответов задач на преобразование либо на описаниеF VF Группировка относительно выражения с неизвестнымиF Теорема приема E тождествоD выполняющее группировку относительно неизE вестныхD тFеF 4вынесение за скобку4 общего неизвестного фрагмента некольE ких подвыраженийF При этом в скобках остается выражениеD не содержащее неизвестныхF Спецификация имеет элемент 4направл@. . .A4D а также элемент 4неизвестные@x1 . . . xk A4D перечисляющий переменные xi D идентифицируемые с содержащими неизвестные выражениямиF Пример приема данного типаX PH


abcdef

g hij

(0 a & 0 d a

e+cj /f g i+bj /f h

d

= ae di (a

c/g b/h j /f

d

)

)

Замена выполняется слева направоD спецификация имеет элемент 4неизвестE ные@j f A4F Остальные переменные идентифицируются с выражениямиD не соE держащими неизвестныхF WF ПреобразованиеD приводящее к возможности упрощения надтермаF Теорема приема E тождествоD которое позволяет так преобразовать выражениеD что после этого можно выполнить сильное упрощение его надвыраженияF СпеE цификация имеет элемент 4направл@. . .A4D а также элементD уточняющий вид надвыраженияF Простейший пример приема данного типаX

a (

sin a = tg a) cos a

Замена выполняется слева направоD причем заменяемая дробь является опеE рандом арктангенса либо аркконангенсаF Несколько более сложный прием E попытка усмотрения в сумме с радикалами полного квадратаD если эта сумма сама находится под радикаломF IHF Стандартизация с помощью вычисленийF Теорема приема E тождествоD позволяющее упростить выражение с помощью вычисления значений операций над встречающимися в нем константамиF СпеE цификация имеет элемент 4направл@. . .A4D а также элементD уточняющийD какие именно переменные идентифицируются с константамиD и задающий типы этих константF Пример приема данного типаX

abcdef pq (p = bf + de & q = df ab/cd + ae/cf = pa/q c)
Замена выполняется слева направоF Переменные b, d, e, f идентифицируются с десятичными константамиF Антецеденты теоремы выполняют вычисление ноE вых константных значений p, q F IIF Свертка условного выраженияF Теорема приема E тождествоD позволяющее преобразовать условное выражеE ние в безусловноеF Спецификация имеет единственный дополнительный элеE мент 4направл@. . .A4F Пример приема данного типаX

ab (ѓ(a = 0) & b - число (b при 0 < a, иначе - b) = bsg(a))
IPF Непосредственное исключение сложной операцииF Теорема приема E тождествоD уменьшающее эвристическую оценку сложности встречающихся в выражении операцийF Рассматривается максимум таких оцеE нок для всех операцийD имеющихся в заменяемом выраженииD и он оказывается строго больше аналогичного максимума для заменяющего термаF СпецификаE ция имеет единственный дополнительный элемент 4направл@. . .A4F Пример приE ема данного типаX a (0 a + 1 & 0 1 - a cos(3 arcsin a) = (1 - 4a2 ) 1 - a2 ) Преобразование выполняется слева направо и позволяет исключить тригоноE метрические операцииF

PI


IQF Декомпозиция сложной операцииF Теорема приема E тождествоD выражающее сложную в эвристическом смысле операцию через несколько операций той же сложностиD но зависящих лишь от части переменных исходной операцииF Спецификация имеет единственный дополнительный элемент 4направл@. . .A4F Пример приема данного типаX

abc (0 a & 0 b logc (ab) = logc a + logc b)
Здесь происходит декомпозиция логарифмаF ЗаметимD что прием имеет фильтрD блокирующий преобразованиеD если выражения a, b известныD а c содержит неизвестныеD либо если логарифм используется при определении значения некоE торой функцииD и c содержит варьируемую переменнуюD а a, b не содержатF Этот и другие фильтры порождаются по спецификации приема автоматическиF IRF Группировка сложных операцийF Теорема приема E тождествоD позволяющее сгруппировать несколько 4сложE ных4 операций в одну равноценную операциюF Спецификация имеет единственE ный дополнительный элемент 4направл@. . .A4F Пример приема данного типаX

abcd (c

a +d b

(ac + bd) a/b b = ) a a

Здесь два радикала группируются в одинF ISF Специальная стандартизация условия задачи на преобразованиеF Теорема приема E тождествоD используемое для стандартизации выражений в специальном контекстеD определяемом свойствами понятий предметной облаE стиF Кроме элемента 4направл@. . .A4D спецификация имеет элементыD уточняюE щие контекстF Пример приема данного типаX

abcde (p = a sin b sin c/d + e a sin b sin c/d + e = p)
Преобразуемая сумма является условием вспомогательной задачи на упрощеE ние подынтегрального выраженияF Переменная интегрирования входит в выE ражения b, c и не входит в dF Кроме тогоD она не встречается под логарифмом либо под обратной тригонометрической функциейF Антецедент обращается к пакетному нормализаторуD определяющему результат p раскрывания скобок и преобразования тригонометрических произведений в суммыF Принятие решения о контекстной стандартизации требует предварительного анализа не одной теоремыD а целой группы теорем предметной областиF По итоE гам такого анализа в базе теорем фиксируются 4протоколы стандартизации4D являющиеся источниками соответствующих приемовF ITF Безусловная общая стандартизация одного утвержденияF Теорема приема E эквивалентностьD обеспечивающая упрощение элементарного утверждения и применяемая в любых ситуацияхD кроме техD когда она заведомо нарушает принятую стандартизациюF Единственный дополнительный элемент спецификации E 4направл@. . .A4F Простейший пример приема данного типаX

ab ({a} = {b} a = b)
ДругойD чуть более сложный примерX PP


abc (a b c a \ b c)
Замена выполняется справа налевоF Применение приема сопровождается раE дом стандартных ограниченийF НапримерD если c E неизвестнаяD а выражения a и b известныD то преобразование отменяетсяF Эти ограничения автоматически создаются по спецификацииF IUF Конъюнктивная декомпозиция элементарного утвержденияF Теорема приема E эквивалентностьD преобразующая элементарное утверждение в конъюнкцию элементарных утвержденийF Переменные каждого конъюнктивE ного члена заменяющей части образуют собственное подмножество переменE ных заменяемой частиF Единственный дополнительный элемент спецификации E 4направл@. . .A4F Пример приема данного типаX

abc (a b \ c ѓ(a c) & a b)
IVF Общая стандартизация группы посылокF Теорема приема E эквивалентностьD позволяющая заменить несколько элеменE тарных посылок задачи на одну такую посылкуD без какогоEлибо ущерба для поE следующего решенияF Единственный дополнительный элемент спецификации E 4направл@. . .A4F Аналогичный тип введен для стандартизации группы условийF Пример приема данного типаX

ab (a = b a b & b a)
Замена выполняется справа налевоF IWF Дизъюнктивно E конъюнктивная свертка в условии задачи на компактную пеE реформулировку утверждения @4свертку4AF Теорема приема E эквивалентностьD позволяющая преобразовать дизъюнктивно E конъюнктивную конструкциюD составленную из элементарных утвержденийD в одно элементарное утверждениеF Единственный дополнительный элемент спеE цификации E 4направл@. . .A4F Пример приема данного типаX

abc (a b c a b a c)
Замена выполняется справа налевоF Прием применяется в задачах на описаE ниеD целевая установка которых явно указывает на необходимость компактной переформулировки условийF PHF Кванторная сверткаF Теорема приема E эквивалентностьD позволяющая переформулировать бескванE торным образом квантор общности либо существованияF Единственный дополE нительный элемент спецификации E 4направл@. . .A4F Пример приема данного типаX

ab (непересек(a, b) c (c a ѓ(c b)))
Замена выполняется справа налевоF Прием сопровождается группой стандартE ных фильтровD блокирующих преобразованиеD если оно противоречит текущей целевой установкеF Все эти фильтры генерируются автоматическиF ИсключеE ние квантора обеспечивается даже в тех случаяхD когда требуются неслоежные предварительные преобразования E переход от квантора существования к отриE цанию квантора общности либо группировка части антецедентов под внутренE ний квантор общностиF PQ


PIF Кванторная расшифровка в условии задачи на доказательствоF Теорема приема E эквивалентностьD позволяющая перейти к кванторной расE шифровке элементарного утвержденияF Прием применяется к подутверждению условия задачи на доказательство E корневому либо находящемуся под корE невым отрицаниемF Единственный дополнительный элемент спецификации E 4направл@. . .A4F Пример приема данного типаX

ab (a - set & b - set a = b c (c a c b))
Замена выполняется справа налевоF Фильтры приемаD уточняющие контекст его примененияD генерируются по спецификации автоматическиF PPF Попытка использования явного параметрического описания при получении чаE стичного ответаF Теорема приема E эквивалентностьD дающая явное параметрическое описание для значений переменнойD при которых истинно заданное элементарное утверE ждениеF Единственный дополнительный элемент спецификации E 4направл@. . .A4F Пример приема данного типаX

bc (b c a (c = a {b} & a - set))
Левая часть эквивалентности идентифицируется с условием задачи на описаE ниеD причем c E неизвестная этой задачиD не входящая в выражение bF В задаче требуется найти лишь пример значений неизвестныхF PQF Разрешение условия задачи на описание либо посылки задачи на исследование относительно заданных неизвестныхF Теорема приема E эквивалентностьD заменяющая часть которой дает явное разE решение заменяемой части относительно заданных переменныхF ДополнительE ные элементы спецификации E 4направл@. . .A4 и 4неизвестные@x1 . . . xk A4D где x1 , . . . , xk E переменныеD относительно которых происходит разрешениеF ПриE мер приема данного типаX

abc (b < ac c < 0 & a < b/c 0 < c & b/c < a c = 0 & b < 0)
Замена выполняется слева направоD неизвестной считается переменная aF PRF Свертка группы неизвестных условий в одно условиеD явно разрешенное отноE сительно неизвестныхF Теорема приема E эквивалентностьD позволяющая объединить несколько услоE вий задачи на описаниеD явно разрешенных относительно неизвестнойD в одно условиеD явно разрешенное относительно этой неизвестнойF Дополнительные элементы спецификации E 4направл@. . .A4 и 4неизвестные@xA4D где x E неизвестE наяF Пример приема данного типаX

abc (a b c a c & b c)
Замена выполняется справа налевоF Переменная c идентифицируется с неизE вестнойD переменные a, b E с выражениямиD не содержащими неизвестныхF PSF Преобразование условия задачи на описаниеD исключающее сложное выражеE ние с неизвестнымиF

PR


Теорема приема E эквивалентностьD позволяющая исключить наиболее сложE ное в эвристическом смысле подвыражение заменяемой частиF ДополнительE ные элементы спецификации E 4направл@. . .A4 и 4терм@tA4D где t E исключаемое подвыражениеF Пример приема данного типа E возведение уравнения в квадрат для исключения неизвестного радикалаX

abcdp (0 d adp/2 + b = c a2 dp - b2 + 2bc = c2 & 0 (c - b)a)
Переменная p идентифицируется с натуральной константойF Выражение d соE держит неизвестныеD c E не содержитF Исключается подвыражение dp/2 F PTF Переход к дизъюнктивной посылкеD определяющей значение переменнойD вхоE дящей в условиеF Теорема приема E эквивалентностьD позволяющая преобразовать элементарную посылку к виду дизъюнкцииD один из членов которой явно выражает некоE торую переменнуюD входящую в условие задачиF Таким образом подготавлиE вается полезный разбор случаевF Дополнительные элементы спецификации E 4направл@. . .A4 и 4переменная@xA4D где x E переменнаяD для которой находится явное выражениеF Пример приема данного типаX

abc (a {b; c} a = b a {; c})
Замена выполняется слева направоF Здесь {b; c} E конечный списокD в котором выделен некоторый элемент bD причем c E остальные элементы спискаF В специE фикации указана переменная aF ПроверяетсяD что она не входит в выражение bD но встречается в условии задачиF Фильтры приема генерируются по специE фикации автоматическиF PUF Развертка квантора существования в дизъюнкциюF Теорема приема представляет собой эквивалентностьD в обеих частях котоE рой находятся кванторы существованияF Заменяющий квантор явно указывает конечное множество A допустимых значений своей варьируемой переменнойF Прием разворачивает его в дизъюнкциюD члены которой соответствуют элеE ментам множества AF Единственный дополнительный элемент спецификации E 4направл@. . .A4F Пример приема данного типаX

f mkpx (p = k - m & k - целое & m - целое n (n - целое & x = f (n) & m n & n k ) l (l {0, . . . , p} & x = f (m + l)))
Замена выполняется слева направоF Первый антецедент находит результат p упрощения разности выражений k , mF ПроверяетсяD что этот результат E натуE ральная константаD меньшая WF Правый квантор существования разворачиваE ется в дизъюнкцию для значений l = 0, . . . , pF PVF Разрешение неконстантного выражения относительно константF Теорема приема E эквивалентностьD позволяющая разрешить элементарное утверE ждение относительно некоторой переменнойD в предположенииD что эта переE менная идентифицирована с неконстантным выражениемD а прочие переменE ные E с константными выражениямиF Дополнительные элементы спецификаE ции E 4направл@. . .A4 и 4терм@xA4D где x E переменнаяD относительно которой выполняется разрешениеF Пример приема данного типаX

ab (a < -b b < -a)
PS


Замена выполняется слева направоF Выражение b неконстантноеD a E константE ноеF PWF Непосредственное усмотрение истинности либо ложностиF Теорема приема не имеет вида x1 ...xn A(x1 . . . xn )D где A(x1 . . . xn ) E элементарное утверждениеF Если в задаче встречается утверждение вида A(t1 . . . tn )D быть моE жетD с отброшенным корневым отрицаниемD то прием заменяет его на константу 4истина4 либоD соответственноD 4ложь4F Спецификация не имеет дополнительE ных элементовF Пример приема данного типаX

a (a a)
QHF Усмотрение истинности либо ложности с помощью проверочного оператораF Теорема приема имеет вид кванторной импликации x1 ...xn (A1 & . . . & An A0 )D где консеквент A0 E элементарное утверждениеD а антецеденты A1 , . . . An допускают проверку с помощью пакетных проверочных операторовF Прием исE пользует эти операторы для усмотрения истинности утверждения A0 D которое заменяется на константу 4истина4F Спецификация не имеет дополнительных элементовF Пример приема данного типаX

ab (b a ѓ(a < b))
Прием усматривает ложность строго неравенстваD проверяя истинность встречE ного нестрогогоF QIF Вывод одноместного предикатаF Теорема приема E кванторная импликацияD консеквент которой имеет вид P (x)D где x E переменнаяD P E символ одноместного отношенияF Часть антецедентов теоремы приема идентифицируются с посылками задачиD остальные E провеE ряются с помощью вспомогательных средствF После этого выводится новая посылка P (x)F Дополнительные элементы спецификации отсутствуютF Пример приема данного типаX

AB C (A отрезок(B C ) A - точка)
QPF Вывод равенства двух числовых атомовF Теорема приема E кванторная импликацияD имеющая консеквент вида t1 = t2 D где t1 , t2 E атомарные числовые выраженияD не являющиеся переменнымиF Здесь и далее называем числовое выражение f (A1 . . . Am ) атомарнымD или числовым атомомD если хотя бы одно из подвыражений Ai принимает нечисловые знаE ченияF Численные переменные называем вырожденными числовыми атомамиF Примеры невырожденных числовых атомов E 4расстояние@A B A4D 4масса@AA4D 4угол@AB C A4D 4скорость@A tA4D и тFпF Часть антецедентов теоремы приема иденE тифицируются с посылкамиD остальные E проверяются вспомогательными средE ствамиF После этого к посылкам задачи присоединяется равенство t1 = t2 F ДоE полнительные элементы спецификации отсутствуютF Пример приема данного типаX

AB C D (прямая(AC ) прямая(B D) & B прямая(AC ) & (ADB ) = (B DC ) & разныеточки(B , D) l(AB ) = l(B C ))
Прием усматриваетD что B D E высота треугольника ADC и одновременно его биссектрисаF Из этого выводится следствиеD что B D E медианаF PT


ЗаметимD что в приемах данного типа не накладывается никаких дополнительE ных ограничений на рассматриваемые числовые атомыF Иногда неограниченE ный вывод следствий нежелателенD и тогда используются подтипы этого типаD в которых действия более мотивированыF НапримерD возможен следующий подE типX QQF Вывод равенства двух старых числовых атомовF Теорема приема E такого же видаD как в предыдущем случаеD но перед выводом соотношения t1 = t2 проверяетсяD что числовые атомы t1 , t2 уже рассматриваE ются в задачеF Дополнительных элементов спецификации нетF Пример приема данного типаX

AB C DE (актив((DAE )) & актив((B AC )) & A отрезок(B E ) & A отрезок(C D) (B AC ) = (DAE ))
Выводится равенство вертикальных углов B AC и DAE D которые уже встречаE ются в посылках задачиF Посылка 4актив@X A4 означаетD что расстояние либо угол X уже встречаются в задачеF Такие посылки заблаговременно создаются другими приемами решателяF Как уже замечалось вышеD выбор необходимой степени мотивированности @иныE ми словамиD подтипа в ветви дерева типовA происходит при доводке приемов на задачникеF QRF Общий случай соотношения для числовых атомовF Теорема приема позволяет вывести некоторое уравнение для невырожденных числовых атомовF Вывод реализуется в посылках задачи на исследование либо на доказательствоD причем никаких дополнительных ограничений на срабатыE вание приема не накладываетсяF Спецификация состоит только из указателя типа приемаF Пример приема данного типаX

AB C DE (прямая(AB ) прямая(AC ) & окружность(DE )вписана в фигура(AB C ) 2l(DE ) = l(AB ) + l(AC ) - l(B C ))
Всякий разD как только в задаче усматривается окружностьD вписанная в пряE моугольный треугольникD выводится равенствоD выражающее ее радиус через длины сторон треугольникаF Рассматриваемый тип приемов является корнем большой ветви подтиповF Эти подтипы возникли после анализа приемов решения планиметрических задачD используемых решателемF Выбор необходимого подтипа при обучении системы происходит после 4примерки4 приема на задачникеF Для автоматизации такой примерки создана процедура доводчика приемовF Приведем несколько примеE ров подтипов данного типаF QSF Соотношение для старых числовых атомовF Теорема приема позволяет вывести некоторое соотношение для невырожденE ных числовых атомовF Вывод реализуется только в том случаеD если все эти атомы уже встречаются в задачеF Дополнительные элементы спецификации отсутствуютF Пример приема данного типаX

AB C (актив(l(AB )) & B отрезок(AC ) l(AC ) = l(AB ) + l(B C ))
СоотношениеD связывающее длину отрезка с длинами двух подотрезков вывоE дитсяD если все эти длины уже встречаются в задачеF PU


QTF Определение старого числового атомаF Теорема приема позволяет вывести некоторое соотношение для невырожденных числовых атомовF Вывод реализуется только в том случаеD если все эти атомы уже встречаются в задачеD причем один из них не известенD а остальные E изE вестныF Дополнительные элементы спецификации отсутствуютF Пример приема данного типаX

AB C (прямая(AB ) прямая(AC ) & актив((AB C )) l(AC ) = sin((AB C ))l(B C ))
Соотношение связывает длину катета с длиной гипотенузы и синусом острого углаF Оно выводитсяD если одна из величин l(AC )D l(B C )D (AB C ) не известнаD а две другие E известныF QUF Определение числового атома 4неизв4F Теорема приема позволяет вывести некоторое соотношение для невырожденE ных числовых атомовF Вывод реализуется только в том случаеD если все эти атомы уже встречаются в задачеD причем один из них не известен и встречаетE ся в уравнениях с численными неизвестнымиD а остальные E известныF ЗаметимD что невырожденные числовые атомыD встречающиеся в уравнениях с численныE ми неизвестнымиD называются атомами типа 4неизв4F Определение их значения позволяетD в конечном счетеD получить для численной неизвестной 4обычное4 уравнениеD имеющее только численные параметрыF Данный тип приемов отE носится в геометрии к наиболее мотивированнымF Дополнительные элементы спецификации отсутствуютF Пример приема данного типаX

AB C DE F (прямая(AB ) прямая(DE ) & прямая(AC ) прямая(DF ) & прямая(B C ) прямая(E F ) & актив(l(AB )) & актив(l(B C )) & актив(l(DE )) & актив(l(E F )) & разныепрямые(прямая(AB ), прямая(B C )) l(AB )l(E F ) = l(B C )l(DE ))
Здесь усматривается подобие треугольников AB C и DE F D имеющих параллельE ные соответственные стороныD и выводится соотношение пропорциональности длин сторонF Одна из этих длин имеет тип 4неизв4D а три оставшиеся E известE ныF В некоторых случаях ограничение на невырожденные числовые атомыD встреE чающиеся в выводимом равенствеD имеет асимметричный характерF Иногда это вызвано асимметричным характером самого соотношенияD иногда E необходимоE стью ускорить отсечение ненужных ситуаций при идентификацииF Такое ускоE рение объясняется темD что проверять условиеD накладываемое на числовой атомD можно сразу же после его идентификацииD не дожидаясь идентификации остальных атомовF Приведем пример типа приема с асимметричным ограничеE ниемX QVF Определение заданного старого числового атомаF Теорема приема позволяет вывести некоторое соотношение для невырожденE ных числовых атомовF Вывод реализуется только в том случаеD когда заданный числовой атом этого соотношения не известенD но уже встречается в задачеD а все остальные атомы E известныF Дополнительный элемент спецификации E 4терм@pA4D указывающий определяемый числовой атом pF Пример приема данE ного типаX PV


AB C (актив((B AC )) 2l(AB )l(AC ) cos((B AC )) = l(AB )2 + l(AC )2 - l(B C )2 )
Спецификация имеет элемент 4терм@угол@B AC AA4F Прием выводит соотношеE ние теоремы косинусов для определения неизвестного угла B AC D который уже рассматривается в задачеF QWF Вывод двуместного отношения в задаче на исследование либо на доказательE ствоF Теорема приема позволяет выводить утверждение вида P (a, b)D где P E символ отношенияD отличного от равенства и числового неравенстваY a и b E переменныеD идентфицируемые с уже рассматриваемыми в задаче объектамиF ДополнительE ный элемент спецификации E либо отсутствуетD либо имеет вид 4антецедент@iA4 и указывает номер i антецедентаD идентифицируемого с посылкой задачиF ПриE мер приема данного типаX

abc (a b & b c a c)
RHF Разбор случаев в задаче на исследованиеF Теорема приема E кванторная импликация с дизъюнкцией в консеквентеF Прием реализует вывод этой дизъюнкции в посылках задачи на исследованиеD сопровоE ждая ее комментариемD инициирующим разбор случаевF Дополнительные элеE менты спецификации уточняют контекст срабатыванияF Пример приема данE ного типаX

abx (x {a; b} a x ѓ(a x))
Здесь x E неизвестная внешней задачи на описаниеD a E известноF RIF Усмотрение противоречия в посылках задачи на исследованиеD возникшей при разборе случаевF Теорема приема E кванторная импликацияD имеющая своим консеквентом симE вол 4ложь4F Прием усматривает в посылках задачи на исследование ситуациюD описываемую антецедентами теоремыD и выводит новую посылку 4ложь4F Он применяется только в задачахD возникших после разбора случаевD тFеF если имеE ется некоторая вероятность нереализуемости рассматриваемого подслучаяF ТаE кие задачи распознаются по цели 4контроль4F Дополнительные элементы спеE цификации отсутствуютF Пример приема данного типаX

AB a (l(AB ) = a & a < 0 ложь)
При усмотрении в посылках равенства l(AB ) = aD где выражение a не содержит неизвестныхD предпринимается быстрая попытка проверки отрицательности aF RPF Вывод утверждения существованияF Теорема приема имеет вид кванторной импликацииD консеквентом которой слуE жит квантор существованияF Часть антецедентов идентифицируются с посылE камиD остальные E проверяются вспомогательными средствамиF Прием выводит квантор существованияD ориентируясь на тоD что сразу вслед за этим для его связанных переменных в задаче будут введены вспомогательные обозначенияD а сам квантор преобразован в конъюнкцию подкванторных утвержденийF ДоE полнительные элементы спецификации отсутствуютF Пример приема данного типаX

PW


f gAB (Отображение(f , A, B ) & Отображение(g , A, B ) & ѓ(f = g ) a (a A & ѓ(f (a) = g (a))))
Если в посылках задачи рассматриваются различные отображения f и g с одиE наковыми областью определения и областью значенийD то вводится в рассмотE рение точка aD на которой эти отображения принимают различные значенияF RQF Вывод определенияF Теорема приема имеет вид кванторной импликацииD консеквент которой являE ется расшифровкой по определению некоторого антецедента AF Обычно этот консеквент является кванторной импликациейF Часть антецедентов @включая AA идентифицируются с посылкамиD часть E проверяются вспомогательными средствамиF Прием выводит расшифровку посылкиD идентифицированной с AD сохраняя также ее исходную версиюF Он бывает полезен на ранних этапах исE пользования нового понятияD когда не созданы средстваD позволяющие работать с ним без расшифровки по определениюF Дополнительные элементы специфиE кации отсутствуютF Пример приема данного типаX

A (A R & замкнутое(A) x (предельнточка(x, A) x A))
Посылка 4замкнутое@AA4 сопровождается своей квантрной расшифровкойD коE торая может понадобиться для вывода следствийF ЗаметимD что эквивалентная замена рассматриваемой посылки привела бы к отключению приемовD реагиE рующих на утверждение о замкнутости множества AF RRF Вывод условияD ограничивающего значения неизвестного подвыражения конечE ным множествомF Теорема приема имеет вид кванторной импликацииD консеквент которой ограE ничивает значения некоторой переменной x конечным множествомF Прием усматE ривает истинность антецедентовD идентифицируя x с выражениемD содержащим неизвестные задачи на описаниеF Затем ограничение на значения x присоединяE ется к списку условий задачиD чтобы далее предпринять разбор случаев по коE нечному множеству альтернативF Единственный дополнительный элемент спеE цификации E 4неизвестная@xA4F Пример приема данного типаX

abcdmn (n - натуральное & 0 < a & d = [(c - m)/a] & m b & an + b = c n d)
В условиях задачи на описание усматриваются уравнение an + b = c и утверE ждение 4n - натуральное4D где выражение n содержит неизвестныеF ПеременE ные a, c идентифицируются с целочисленными константамиF Проверяется услоE вие 0 < aF При помощи пакетного синтезатора находится константная нижняя оценка m значений выражения bF НаконецD вычисляется целочисленное значеE ние dD равное [(c - m)/a]D и в список условий заносится неравенство n dF Таким образомD значения выражения n ограничиваются конечным множеством {1, . . . , d}F RSF Исключение несущественных неизвестных в задаче на описание при невырожE денном ограниченииF Теорема приема имеет вид эквиваленостиD в заменяемой части которой нахоE дится квантор существования x1 ...xn (A1 & . . . & Am )Dа в заменяющей E некоE торое элементарное утверждение B F Переменные x1 , . . . , xn идентифицируются

QH


с несущественными неизвестными задачи на описаниеF Значения таких неизE вестных не обязательно указывать в ответеD а достаточно лишь убедиться в их существованииF ПроверяетсяD что все содержащие данные неизвестные услоE вия задачи идентифицируются в точности с утверждениями A1 , . . . , Am F Затем эти условия удаляютсяD а вместо них добавляется условие B F Дополнительные элементы спецификации отсутствуютF Пример приема данного типаX

ae (d (d - set & a d & d e) a e)
Если на несущественную неизвестную d накладываются лишь условия 4d - set4D a d и d eD то эти условия отбрасываютсяD а вместо них вводится условие a eF RTF Подбор примера значений неизвестныхD не входящих в невырожденные услоE вияF Теорема приема имеет вид кванторной импликацииD один из антецедентов коE торой E равенство x = aD где a не содержит xD а консеквент E элементарное утверждение B F Прием усматриваетD что неизвестная x задачи на описание встречается только в условии B D а такжеD быть можетD в простейших сопроE вождающих утверждениях E одноместных предикатах P (x) либо отрицаниях равенств ѓ(x = t)F Если в задаче нужно найти лишь пример значений неизвестE ныхD то прием предпринимает попытку свести ее к вспомогательной задачеD в которой значение x положено равным aF Единственный дополнительный элеE мент спецификации E 4неизвестная@xA4F Пример приема данного типаX

ax (x = ѓ(a x))
Чтобы реализовать условие ѓ(a x) с неизвестной xD прием предпринимает попытку положить x равным F RUF Прием проверочного оператораF Теорема приема E кванторная импликацияD позволяющая усматривать истинE ность утверждений заданного видаD соответствующего рассматриваемому проE верочному операторуF Единственный дополнительный элемент спецификации E 4оператор@AA4D где A E название проверочного оператораF Пример приема данE ного типаX

ab (0 < b & 0 < a 0 < ab)
Элемент спецификации E 4оператор@усмменьшеA4F Проверочный оператор 4усмE меньше4 усматривает истинность строгих неравенствF Прием сводит проверку положительности произведения к проверке положительности каждого из соE множителейF RVF Прием нормализатора общей стандартизацииF Теорема приема E тождествоD выполняющее простейшую стандартизацию выраE жений с заданным заголовкомF Прием применяется в пакетном нормализаторе общей стандартизацииF Дополнительные элементы спецификации E 4оператор@AA4 и 4направл@. . .A4F Здесь A E название нормализатораF Прием примеа данного тиE паX

a (a + 0 = a)
Элементы спецификации E 4оператор@нормплюсA4 и 4направл@второйтермA4F QI


RWF Прием синтезатораF Теорема приема E кванторная импликацияD позводяющая подобрать значения переменныхD при которых реализуемое пакетным синтезатором утверждение становится истиннымF Единственный дополнительный элемент спецификации E 4оператор@AA4D где A E название синтезатораF Пример приема данного типаX

a (cos a 1)
Дополнительный элемент спецификации E 4оператор@верхняяоценкаA4F Данный синтезатор реализует утверждения вида a xD где a E входное данноеD x E выходная переменнаяF Прием предлагает выбрать единицу в качестве верхней оценки косинусаF Для каждого типа приема создана программаD инициирующая компиляцию специфиE кации в описание приема на ГЕНОЛОГеF После инициализации используется цепочE ка блоковD выполняющих стандартные действия компилятораX уточнение способов обработки антецедентов теоремы приемаD уточнение способов идентификацииD уточE нение способов обработки новых подтермовD создаваемых приемомD уточнение списE ка дополнительных фильтров приемаF ЗаметимD что создание основных фильтровD предопределяемых типом приемаD обеспечивается стартовой программой компиляE тораF Вообще говоряD результат работы компилятора требует некоторой доводки E примерки на разделе задачника и необходимых коррекцийF В первую очередьD здесь уточняется уровень срабатывания приемаF Создание коллекции типов приемов находится лишь на начальной стадииF Часть этих типов можно смело создавать по теореме сразу жеD другие E лишь по мере надобностиD в процессе решения нестандартных задачF В последнем случае логичеE ский ассемблер играет роль 4генератора идей4F Он может предложить множество потенциально интересных приемовD из числа которых после решения задачи будут отбираться лишь действительно полезныеF

Создание спецификации приема по теореме
Как правилоD заданный на ГЕНОЛОГе прием имеет своим источником некоторую теорему предметной областиF Ее не следует путать с теоремой приемаD составляE ющей часть описания приемаF Источником приема служит истинное утверждениеD заданное на логическом языкеF Теорема приема задается на языкеD который являE ется 4первым шагом4 от логического к алгоритмическомуD и вид ее может сильно отличаться от источникаF От нее требуется лишьD чтобы она была понятна компиляE тору ГЕНОЛОГаF Перечислим некоторые возможные различия между источником приема и его теоремойF Прежде всегоD в теореме приема отбрасываются те антецедентыD истинность коE торых предполагается в контексте по умолчанию E ввиду стандартных условий на области допустимых значенийF ТакD источник приемаX

ab (a - число & b - число -ab = (-a)b)
преобразуется в теорему приемаX

ab (-ab = (-a)b). ДалееD в теореме приема могут появиться антецеденты вида 4актив@AA4D которые означают лишьD что в задаче уже рассматривается выражение AD и имеется явно
QP


указывающая на это фиктивная посылка 4актив@AA4F Пример может служить слеE дующая теорема приемаD выводящего соотношение для суммы углов треугольникаX

AB C (актив((AB C )) & актив((B C A)) (AB C ) + (B C A) + (B AC ) = )
В некоторых случаях технически проще оказывается компилировать проверку исE тинности антецедента источникаD перенеся его в фильтры приемаF СоответственноD из теоремы приема этот антецедент исключаетсяF Если теорема приема обращается к некоторой вспомогательной процедуре E задаче либо пакетному нормализаторуD то в ее антецедентах может появиться равенствоD организующее данное обращениеF В этой ситуации источником приема может оказаться вообще не теорема предметной областиD а некоторый технический протоколD указывающий на необходимость решеE ния вспомогательной задачиF После тогоD как для приема ГЕНОЛОГа уточнена спецификацияD следующим шаE гом анализа процесса создания этого приема становится указание в базе теорем его источникаF Первоначально база теорем возникает не за счет перенесения информаE ции из учебниковD а как своеобразная 4проекция4 базы приемовD извлеченной из задачниковF Таким образомD из базы приемов извлекается обучающий материал для развития процедурD синтезирующих спецификации приемов по заданной теоремеF Создание спецификаций начинается с характеризации теоремы E сопровождения ее набором характеристикD указывающих особенностиD существенные для алгоритмизацииF На текущий момент выявлено более полутора сотен полезных характеристикF Приведем несколько их примеровX IF 4нормализация@nA4F Теорема представляет собой тождествоD обпспечивающее общую стандартизациюF Логический символ n указывает направление заменыF Усмотрение тождества общей стандартизации имеет эвристический характерF При анализе примеров были найдено множество ситуацийD когда тождество естественно относить к данной категорииF Приведем несколько таких ситуацийX @A В заменяемом терме выделяется подтермD из которого заменяющий терм получен отбрасыванием части операндовF @A Заменяемый терм неконстантныйD а заменяющий E константныйF @A Заменяющий терм бесповторный и имеет единственную переменнуюF ЗаE меняемый терм тоже содержит эту переменнуюD но имеет и другие переE менныеF Эвристическая оценка сложности символов заменяющего терма не больше чем у заменяемогоF @dA Заменяемый и заменяющий термы имеют вид f (A1 , . . . , An ) и g (A1 . . . , An )F Операция f не коммутативнаяD а g E коммутативнаяF PF 4свертка@nA4F Теорема представляет собой тождествоD позволяющее переходить к более короткой записиF n E направление заменыF QF 4описатель@nA4F Теорема представляет собой тождествоD которое можно испольE зовать для перехода к более простым описателям либо для исключения описаE телейF n E направление заменыF RF 4дистрибразвертка@nA4F Теорема представляет собой обобщенное тождество дисE трибутивности @допускается изменение знака внутренней операцииAF QQ


SF 4и@nA4 либо 4или@nA4F Теорема представляет собой эквивалентностьD преобраE зующую элементарное утверждение в конъюнкцию @соответственноD дизъюнкE циюA бескванторных утвержденийF TF 4кванторнаясвертка@nA4F Теорема представляет собой эквивалентностьD позвоE ляющую переходить от квантора к бескванторному утверждениюF UF 4глуб@x nA4F Теорема представляет собой эквивалентностьD заменяемое утверE ждение которой элементарноD причем глубина вхождений в него переменной xD с отбрасыванием внешнего отрицанияD больше единицыD а аналогичная глубиE на для элементарного заменяющего утверждения E равна IF Такие эквивалентE ности интересны для порождения приемов явного разрешения относительно неизвестной xF VF 4пример4F Теорема представляет собой кванторную импликацию без существенE ных посылокD консеквент которой E элементарное утверждение f (A1 . . . Ak ) либо отрицание такого утвержденияF Все Ai D кроме одногоD суть попарно различные переменныеF На таких теоремах основаны приемыD подбирающие в простейших случаях пример значения неизвестнойF WF 4разделение@nA4F Теорема представляет собой эквивалентностьD позволяющую переносить в разные части двуместного отношения две переменныеD ранее расE положенные в одной частиF n E направление заменыF Источники приемов можно разделить на два классаF В первом случае источник получается из 4обычных4 теорем предметной области с помощью специализированE ного логического выводаD причем заранее известен тип приемаD ради которого этот вывод реализуетсяF Тогда характеризация предпринимается процедурами логическоE го выводаF Такой вывод далее называем 4программирующим4F Примеры программиE рующих выводов будут рассмотрены в следующем разделеF Во втором случае исE точник сам является 4обычной4 теоремой либо близок к нейF Тогда характеризация теоремы предпринимается специальной процедуройD рассматривающей весь спектр возможных направлений синтеза приемовF После тогоD как теорема снабжена набором характеристикD начинается собственно создание спецификацийF Оно реализовано как процесс сканирования характеристик и обращения к приемам спеицификатораD распределенным между различными назваE ниями характеристикF Эти приемы представляют собой тривиальные переходники от характеристики теоремы к типу приемаD хотя иногда учитываются и дополниE тельные свойства теоремыF Часть спецификаций создаются по теореме сразу E они соответствуют наиболее сильно мотивированным и часто используемым типам приE емовF Другие E создаются лишь при наличии специальных опцийD уточняющих целеE вую установку при создании приемовF НапримерD эти опции могут быть подсказаны задачейD для решения которой запускается синтез дополнительных приемовF

Программирующий логический вывод
Источник приема часто представляет собой теоремуD полученную из 4обычной4 теоE ремы цепочкой модификаций и обобщенийD направленных на расширение области применимости приемаF Рассмотрим простой примерF Среди базисных теорем тригоE нометрии имеется тождествоD связывающее между собой значения синуса и косинусаX QR


a ((sin a)2 + (cos a)2 = 1)
Это тождество подсказывает прием общей стандартизацииD применяемый слева наE правоF Чтобы такой прием срабатывал в ситуацияхD когда перед квадратами нахоE дятся одинаковые коэффициентыD тождество следует несколько обобщитьX

ab (b(sin a)2 + b(cos a)2 = b)
Следующий шаг обобщения E учет случаевD когда коэффициент b имеет сомножитеE лями некоторые степени синуса и косинуса aX

abcdef (c - d = 2 & e - b = 2 f (cos a)c (sin a)b + f (cos a)d (sin a)e = f (sin a)b (cos a)d )
ЗаметимD что прием обеспечивает усмотрение вырожденных нулевых значений поE казателей степени b, eF НаконецD если коэффициенты при слагаемых различныD но 4подобны4D тFеF имеют вид pK и q K D где p, q E десятичные константы одинаковоE го знакаD то можно так обобщить тождествоD чтобы оно применялось к слагаемому с меньшим по модулю численным коэффициентом p и части другого слагаемогоD имеющей такой же численный коэффициентF В результате получаем окончательную версию теоремыD являющуюся источником приема решателяX

abcdef ghij k (a - b = 2 & c - d = 2 & (0 < e & 0 < f & g = min(e, f ) e < 0 & f < 0 & g = mx(e, f )) & h = e - g & i = f - g ej (cos k )c (sin k )b + f j (cos k )d (sin k )a = hj (cos k )c (sin k )b + ij (cos k )d (sin k )a + g j (cos k )d (sin k )b )
Этот пример показывает типичную ситуациюX хотя источник приема и является логиE чески корректным истинным утверждениемD он может сильно отличаться от базисной теоремы предметной области за счет ввода большого числа обобщающих 4техничеE ских4 параметровF Иногда таких параметров нетD а источник приема представляет собой просто результат варьирования базисной теоремы с помощью некоторых друE гих ранее освоенных теоремF Чтобы проследитьD каким образом источники приемов возникают из 4обычных4 теоE ремD последние тоже заносятся в базу теоремF При этом все источники приемовD полученные из одной и той же обычной теоремыD регистрируются в общем концеE вом подменю базы теоремF Первый пункт подменю соответствует базисной теореме @иногда она тоже может быть использована как источник приемаAD остальные E поE лученным из нее источникам приемовF Такая организация базы теорем превращает ее в задачник для обучения системы программирующему выводу E получению источE ников приемов из базисных теоремF Процедура программирующего вывода анализирует список исходных теорем и пополняет его новыми элементамиF Исходные теоремы суть базисные тоеремыD изE влекаемые из первого пункта некоторого подменю базы теоремF Чтобы получить следствия текущей теоремы спискаD последовательно просматриваются ее характеE ристикиD и предпринимаются обращения к программе справочника 4прогрвывод4 на логическом символеD являющемся заголовком характеристикиF Эта программа объE единяет некоторую группу приемов вывода теоремF Для упорядочения применения приемовD как и в случае решателя задачD испольE зуются веса теоремF Изначально веса теорем нулевыеF После каждой попытки полуE чения следствий теоремы ее вес увеличивается на единицуF На каждом шаге выбираE ется теорема с минимальным весом v F При ее рассмотрении срабатывают только те приемыD у которых допустимый уровень срабатывания равен v F Цикл вывода следE ствий обрывается либо по исчерпании возможностейD либоD в особых случаяхD по исчерпании лимитов времени или длины спискаF QS


На текущий момент программирующий вывод был проработан лишь для алгебры логикиD алгебры множеств и части разделов элементарной алгебрыF При этом было создано PIP приемовF Приведем некоторые из нихF IF Обобщение сверточного тождества путем ввода бесповторного дополнительного параметра операндаF Рассмотрим следующее тождествоX

abc (a - число & b - число & c - число & 0 < a & 0 < b ac bc = (ab)c )
Одна из его характеристик имеет вид 4свертка@второйтермA4D тFеF в направлеE нии слева направо тождество может быть использовано для сжатой перезаписи выраженияF Если использовать вспомогательное тождество

acd (a - число & c - число & d - число & 0 < a (ad )c = acd )D
то нетрудно вывести следствиеD обобщающее первое тождество относительно характеристики 4свертка@второйтермA4X

abcd (a - число & b - число & c - число & d - число & 0 < a & 0 < b acd bc = (ad b)c )
При получении его мы подставили вместо переменной a первого тождества выE ражение ad и воспользовались вторым тождествомF Такой обобщающий переход нетрудно сформулировать в виде следующего приE ема программирующего выводаF Если в заменяемой части A тождества свертки встречается выражение f (x, t)D где x E переменнаяD не имеющая других вхождеE ний в AD то при помощи специального справочника поиска теорем находятся всевозможные тождества вида f (g (u, v ), w) = f (u, h(v , w))D где u, v , w E переE менныеD h E коммутативноD g имеет единицу по переменной v F Приемы данного справочника создаются заблаговременноD при просмотре базы теоремF В нашем примере роль этого тождества играет повторное возведение в степеньF ПроE веряетсяD что выражение t не имеет вида h(. . . y . . .)D где y E переменнаяD не имеющая других вхождений в AF Затем выбирается новая переменная v D и в обобщаемое тождество вместо x подставляется g (x, v )F После применения вспоE могательного тождества получаем тождествоD у которого в заменяемой части вместо f (g (x, v ), t) расположено f (x, h(v , t))F Легко видетьD что оно обобщает исходное тождество свертки за счет нового коэффициента v F PF Обобщение сверточного тождества путем ввода бесповторного внешнего параE метраF Чтобы продолжить обобщение тождестваD полученного в предыдущем пункE теD достаточно подставить вместо переменной d выражение d/e и использовать следующее вспомогательное тождествоX

cde (ѓ(e = 0) & c - число & d - число & e - число c(d/e) = (cd)/e)
В результате получимX

abcde (ѓ(e = 0) & a - число & b - число & c - число & d - число & e - число & 0 < a & 0 < b a(cd)/e bc = (ad/e b)c )
Этот переход обеспечивается следующим приемом программирующего выводаF Если в заменяемой части A тождества свертки встречается выражение f (x, t)D

QT


где x E переменнаяD не имеющая других вхождений в AD то при помощи спраE вочника поиска теорем находятся всевозможные тождества вида f (g (u, v ), w) = h(f (u, w), v )D где u, v , w E переменныеD причем g и h имеют единицу по переменE ной v F В нашем примере роль такого тождества играет умножение на дробьF Затем выбирается новая переменная v D и в обобщаемое тождество вместо x подставляется g (x, v )F После применения вспомогательного тождества и триE виальных упрощений получается тождествоD у которого в заменяемой части вместо f (x, t) расположено h(f (x, t), v )F Перед выдачей результата проверяется неизбыточность добавленного параметра v F Несколько применений описанных двух приемов обобщают рассматриваемое тождество до следующего видаX

abcdef g (ѓ(e = 0) & ѓ(g = 0) & a - число & b - число & c - число & d - число & e - число & f - число & g - число & 0 < a & 0 < b acd/e bcf /g = (ad/e bf /g )c )
QF Обобщение сверточного тождества путем ввода повторного дополнительного параметра операндаF Продолжим цепочку обобщенийF Для этого подставим в предыдущее тождество вместо переменной c выражение c/h и используем следующее вспомогательное тождествоX

ade (ѓ(a = 0) & ѓ(e = 0) & a - число & d - число & e - число (d/a)/e) = d/(ae)
Получим следующий результатD который является окончательным и служит источником приема решателяX

abcdef gh (ѓ(e = 0) & ѓ(g = 0) & ѓ(h = 0) & a - число & b - число & c - число & d - число & e - число & f - число & g - число & h - число & 0 < a & 0 < b acd/(eh) bcf /(gh) = (ad/e bf /g )c/h )
Строго говоряD здесь приходится использовать два вспомогательных тождества E кроме тождества деления дробиD нужно также тождество умножения на дробьF Соответствующий прием программирующего вывода может быть сформулироE ванD напримерD следующим образомF В заменяемой части тождества свертки усматривается подвыражение f (g (x, t), s)D где x E переменнаяD имеющая в этой части несколько вхожденийD причем каждое E в контексте f (g (x, p), q )F ОпеE рация g E ассоциативная и коммутативнаяF При помощи справочников поиска теорем находятся тождества вида g (h(x, y ), z ) = u(g (x, z ), y ) и f (u(x, y ), z ) = f (x, v (y , z ))F Здесь операция h имеет единицу по переменной y Y операция v E ассоE циативна и коммутативнаF Данные тождества суть аналоги тождеств (x/y ) ћ z = (x ћ z )/y и (x/y )/z = x/(y z ) соответственноF Затем выбирается новая переменE ная wD в обобщаемое тождество вместо переменной x подставляется h(x, w)D и применяются указанные выше вспомогательные тождестваF Проверяется неизE быточность нового параметра wF ЗаметимD что промежуточные теоремы цепочки обобщений отбрасываютсяD и в качестве результата выдаются лишь окончательные версииF Кроме перечисленE ных вышеD имеется множество других обобщающих приемовF Приведем теперь несколько приемов программирующего выводаD обеспечивающих варьирование теоремыF RF Попытка опрокинуть тождество общей стандартизации путем сильного упроE щения заменяемого термаF QU


Рассмотрим тождество для сокращения дробейX

cdf (ѓ(c = 0) & ѓ(f = 0) & c - число & d - число & f - число (df )/(cf ) = d/c)
Это тождество имеет характеристику 4нормализация@второйтермA4D тFеF являE ется тождеством общей стандартизацииF Если воспользоваться другим тождеством общей стандартизации

ab (a - число & b - число & ѓ(b = 0) (a/b)b = a)D
представляющим собой определение деленияD то при унификации числителя df заменяемой части первого тождества с заменяемой частью (a/b)b второго можно вывести следствиеX

abc (a/(bc) = (a/b)/c)
Это следствие тоже является тождеством общей стандартизацииD однако наE правление его применения E обратноеF ПриемD реализующий данный выводD усматривает в заменяемой части тождеE ства общей стандартизации вхождение операции f (. . .)D и обращается к спраE вочнику поиска теорем для обнаружения другого тождества общей стандарE тизацииD обеспечивающего сильное упрощение выражений с заголовком f F СоE здано несколько справочников такого типаF НапримерD для поиска тождествD у которых заменяемая часть имеет имеет несколько переменныхD а заменяющая E не более однойF Затем подтерм f (. . .) заменямой части первого тождества унифицируется с заменяемой частью второгоD и после унификации к нему приE меняется второе тождествоF ПроверяетсяD что результатом служит тождество общей стандартизацииD имеющее встречное направлениеF SF Попытка проварьировать заменяемую часть тождества общей стандартизацииF Рассмотрим тождество для вынесения наружу минуса из сомножителяX

ab (a - число & b - число -ab = (-a)b)
Оно имеет характеристику 4нормализация@первыйтермA4F Если воспользоватьE ся вспомогательным тождеством 4перегруппировочного4 типаX

ab (a - число & b - число -(a - b) = b - a)D
то нетрудно вывести следующее следствиеX

abc (a - число & b - число & c - число -a(b - c) = a(c - b))
Последнее тождество уже не рассматривается как тождество общей стандартиE зацииD а имеет характеристику 4свертка@второйтермA4F Оно используется для сокращенной перезаписи выражения при редактировании ответа задачиF ПриE емD реализующий данный выводD аналогичен предыдущемуF Отличие заключаE ется лишь в использовании других справочников поиска теоремF Они отбираE ют тождестваD у которых обе части имеют одни и те же переменныеD причем каждая переменная E бесповторнаяF Не обязательноD чтобы такое тождество обеспечивало общую стандартизациюF TF Извлечение из декомпозирующей эквивалентности импликации для проверочE ного оператораF Рассмотрим определение принадлежности объединению множествX

abc (b - set & c - set a b c a b a c)
QV


Эта эквивалентность имеет характеристику 4или@второйтермA4D тFеF представE ляет собой декомпозицию элементарного утверждения в дизъюнкциюD построE енную с помощью логических связок из элементарных утвержденийF Она позE воляет получить следующие два следствияX

abc (b - set & c - set & a b a b c) abc (b - set & c - set & ѓ(a b) & ѓ(a c) ѓ(a (b c)))
Первое из них может быть использовано в проверочном оператореD усматриE вающем принадлежностьD второе E в оператореD усматривающем непринадлежE ностьF Данный пример приводит к приему программирующего выводаD обрабатываюE щему эквивалентность вида A (B1 . . . Bn )D где A E элементарное утверE ждениеF Действия приема распадаются на две частиF Первая часть приводит дизъюнкцию (B1 . . . Bn ) к виду дизъюнкции конъюнкций элементарноых утвержденийD и для каждой конъюнкции C выводит следствие C AF ПредE варительно проверяетсяD что существует проверочный операторD обрабатываюE щий утверждения вида AF Вторая часть E приводит к виду дизъюнкции конъE юнкций элементарных утверждений отрицание утверждения (B1 . . . Bn )D и для каждой конъюнкции C выводит следствие C ѓ(A)F Как и вышеD предваE рительно устанавливается существование проверочного оператораD обрабатыE вающего утверждения вида ѓ(A)F UF Вывод из определения класса условия принадлежности классуF Рассмотрим определение образа множестваX

af (a - set & f - функция & a hom(f ) образ(f , a) = setx (y (y a & x = f (y ))))
Это тождество имеет характеристику 4описатель@первыйтермA4D так как оно может быть использовано для исключения описателя 4класс4F В обычных сиE туациях тождество применяется в направлении 4справа налево4F ОднакоD для условия принадлежности образу бывают нужны приемыD выполняющие обратE ное преобразованиеF Они основаны на следующем тривиальном следствии исE ходного тождестваX

abf (f - функция & b - set & b hom(f ) a образ(f , b) x (a = f (x) & x b))F
Прием программирующего вывода здесь просто преобразует тождество B = setx A(x) в эквивалентность x B A(x)F VF Разбиение теоремы с условным выражением на две теоремы для подслучаевF Рассмотрим определение модуляX

a (a - число |a| = (a при 0 a, иначе - a))
Для двух различных альтернатив условного выражения выводим следующие два следствияX

a (a - число & 0 a |a| = a) a (a - число & a < 0 |a| = -a)
Из этого примера легко извлекается прием программирующего выводаD примеE няемый к произвольной теореме с условным выражением в консеквентеF QW


WF Использование тождества общей стандартизации для получения тождестваD устраняющего сложное подвыражение с неизвестными при навешивании внешE ней операцииF Для исключения неизвестных радикалов путем возведения обеих частей уравE нения в некоторую степень используется тождествоX

abcd (ѓ(c = 0) & a - число & b - число & c - число & d - число & 0 a & 0 b (bad/c )c = bc ad )
Оно сопровождается в базе теорем характеристикой 4смнеизв@. . .A4D указываE ющейD что было получено именно для этой целиF В ней уточняется контекст применения тождестваX преобразуется подтерм условия задачи на описаниеD выражение a содержит неизвестныеD d E натуральная константаD выражение c не содержит неизвестныхD причем либо b тоже не содержит неизвестныхD либо c E натуральная константаF Рассматриваемое тождество получается обобщением относительно данной характеристики следующего более простого тождестваD котороеD собственноD и будет представлять для нас интерес в этом пунктеX

acd (ѓ(c = 0) & a - число & c - число & d - число & 0 a (a abc (a - число & b - число & c - число & 0 a (ab )c = abc )
с помощью вспомогательного тождества

d/c c

) = ad )F

Оно легко получается из тождества последовательного возведения в степень

ab (a - число & b - число & ѓ(b = 0) (a/b)b = a)F
Прием программирующего выводаD выполняющий этот шагD анализирует подE терм заменяющего терма тождества общей стандартизации @в нашем случае E выражение bcA и обращается к справочнику поиска теорем для нахождения соE кращающего тождестваD применимого к данному подтермуF Под сокращающим понимается тождество вида f (x, g (x, y )) = aD где a E константа либо переменE наяF Далее находится результат последовательного применения двух тождествD и проверяетсяD что он может быть использован для исключения сложного выE ражения с неизвестными при навешивании на обе части уравнения некоторой внешней операцииF Таким образом и появляется изначально характеристика 4смнеизв@. . .A4F ЗаметимD что никаких других характеристик выведенному тожE деству не присваиваетсяD и далее оно будет использоваться только по своему прямому назначениюF База теорем предоставляет обучающий материал не только для программируюE щего выводаD извлекающего источники теорем из базисных теорем разделаD но и для 4исследовательского вывода4D объясняющего получение одних базисных теорем из другихF Граница между программирующим и исследовательским выE водами весьма условнаяF Рассмотрим несколько приемовD которые могут быть отнесены к любой из этих категорийF IHF Вывод упрощающего тождества в стандартной форме путем унификации замеE няемых частей двух ранее найденных тождествF Во многих разделах математики упрощение выражений связано с использоваE нием многочленоподобных 4стандартных форм4F НапримерD таковы дизъюнкE тивные и конъюнктивные нормальные формы в алгебре логики и их аналоги в алгебре множествF ПреимуществаD которые создает переход к стандартной RH


формеD заключаются в уменьшении расстояний между ее подвыражениямиX из любой точки к любой другой можно перейти всего за три шага E два раза через аналог 4умножения4 и один раз через аналог 4сложения4F В результате сущеE ственно повышается эффективность использования упрощающих тождеств и уменьшается их количествоF Чтобы порождать новые такие тождестваD задаE ется список базисных тождествD по которым сразу генерируются приемы вспоE могательного пакетного нормализатора N F Этот нормализатор используется только в цикле вывода новых тождествF Он будет упрощать обе части каждого выводимого тождестваD чтобы исключить избыточные следствияF Основной шаг вывода E унификация заменяемых частей двух упрощающих тождествD позволяE ющая применить их последовательно E сначала первое тождество применяется в направлении усложненияD затем второе E в направлении упрощенияF Данное правило вывода хорошо известно в математической логикеF С его помощью можно быстро создавать аппарат упрощения выражений в различных алгебE раических системахF Преобразование тождеств в приемыD ввиду тривиальной целевой установкиD здесь не вызывает затрудненийF В качестве примера рассмотрим тождества ac bca = ac bc и p pq = q из алгебры логикиD используемые для упрощения дизъюнктивных нормальных формF Если проводить унификацию заменяемых частейD вводя вспомогательE ные переменные для дополнительных дизъюнктивных членовD то в качестве одного из вариантов получим выражение ac bca baD При этом заменяющие части обоих тождеств равныD соответственноD ac bc ba и ac baF Отсюда выводится тождество обобщенного склеиванияX ac bc ba = ac baF IIF Попытка склеить два члена факторизуемого выраженияF Иногда возникает задача преобразовать выражение к такому видуD у которого заголовком служит заданный логический символF НапримерD задача разложеE ния на множителиF Для вывода тождествD обеспечивающих приведение к заE данным заголовкамD используется процедураD аналогичная описанной в предыE дущем пунктеF Сначала порождаются простейшие тождества данного типаF В случае разложения на множители для этого берется произведение двух или боE лее сумм различных переменныхD и предпринимается раскрывание скобокF На период вывода по найденным тождествам создается нормализатор приведения к заданным заголовкамD используемый для отбрасывания тождествD сводящихE ся к ранее полученнымF Основной шаг вывода E применение к нескольким члеE нам заменяемой части текущего тождества вспомогательного тождестваD обесE печивающего взаимное уничтожение этих членовF В результате промежуточные членыD необходимые для непосредственного разложенияD оказываются 4спрятаE ны4D и возникает ценное новое тождествоF В качестве примера рассмотрим тождество (a + b)(c + d) = ac + bc + ad + bdF При использовании вспомогательного тождества p - p = 0 можно унифицировать ad с pD bc E с -p и получить следствие (a + b)(a - b) = a2 - b2 F Таким же обраE зом порождаются остальные тождества сокращенного умноженияF Кроме нихD удается получить множество других полезных для ускоренного разложения на множители формулF Обнаруживаются и такие экзотические соотношенияD как a5 - b5 - ba4 = (a2 + b2 - ab)(a3 - b3 - ab2 )F IPF Попытка проварьировать эквивалентностьD разрешающую относительно неизE вестнойD с помощью тождестваD создающего кратные вхождения переменнойF RI


Прием рассматривает эквивалентностьD разрешающую относительно неизвестE ной x некоторое утверждение A с единственным вхождением этой неизвестнойF Внутри A выбирается содержащее x подвыражение tD имеющее самый сложE ный в эвристическом смысле заголовокF Справочник поиска теорем перечисляE ет тождестваD позволяющие преобразовать t в выражение t с несколькими вхоE ждениями переменной xF В исходной эквивалентности предпринимается замена t на t D и после несложной стандартизации выдается результатF Цель данного вывода E получить эквивалентностьD разрешающуюD хотя бы в частном случаеD утверждение с несколькими вхождениями неизвесетнойF Обычно она подлежит цепочке обобщенийF В качестве примера возьмем эквивалентность для разрешения простейшего стеE пенного уравненияD имеющего рациональный показатель степени с четным чисE лителемX

abc (a - число & b - число & c - число & b - rtionl & числитель(b) - even & ѓ(b = 0) ab = c 0 c & (a = c1/b a = -c1/b ))F
Вспомогательным тождеством будет тождество для квадрата суммы

ab (a - число & b - число (a + b)2 = a2 + 2ab + b2 )D
позволяющее перейти от выражения (a + b)2 с бесповторными переменными к повторным переменнымF После группировки в правой части всех известных слагаемыхD получимX cde (c - число & d - число & e - число d2 + 2de = c - e2 ((d = -e + c d = -(e + c)) & 0 c))F Роль неизвестной здесь играет переменная dF Чтобы получить из этой эквиE валентности известную формулу для решения квадратного уравненияD далее можно использовать прием программирующего выводаD усматривающий подE выражение уравненияD не содержащее неизвестныхD и обозначающий его новым параметромF На первом шагеD вводя вспомогательный параметр a для выражеE ния в правой части уравнения и разрешая относительно c уравнение c - e2 = aD получимX ade (a - число & d - число & e - число d2 + 2de = a ((d = -e + a + e2 d = -(e + a + e2 )) & 0 a + e2 )) Еще раз применяем этот же приемD обозначая посредством b подвыражение 2e и разрешая относительно e уравнение 2e = bF ПолучаемX abd (a - число & b - число & d - число d2 + bd = a ((d = -(b + b2 + 4a)/2 d = (-b + b2 + 4a/2)) & 0 b2 + 4a)) Опускаем описание приемов программирующего выводаD доводящих обобщеE ние данной формулы до случая произвольного коэффициента перед квадратом неизвестнойF ЗаметимD что на всех этапах обобщения теорема сопровождалась характеристикойD указывающей неизвестную dF В заключение приведем прием вывода теоремD позволяющий системе 4открыE вать4 формулу КарданоF IQF Попытка использовать оператор усмотрения повторяющихся подвыражений для получения импликацииD подбирающей корень уравненияF

RP


Прием выводит теоремуD позволяющую подобрать значение неизвестнойD имеE ющей кратные вхождения в реализуемое условиеF Он анализирует исходную теорему вида x (A(x) B (x)) и пытается таким образом преобразовать утверE ждение B (x)D чтобы какоеEлибо неконстантное подвыражение t встречалось в нем более одного разаF Далее выбирается новая переменная y D находится резульE тат C (x, y ) замены всех вхождений t в преобразованное B (x) на переменную y D и выводится следствие x (A(x) & y = t C (x, y ))F Роль неизвестной здесь играет переменная y D причем t E подбираемое значениеF Это отражено в харакE теристикеD сопровождающей теоремуF Далее реализуется цепочка обобщенийF В качестве примера рассмотрим тождество для куба суммыX

ab (a - число & b - число (a + b)3 = a3 + 3a2 b + 3ab2 + b3 )F
Консеквент (a + b)3 = a3 + 3a2 b + 3ab2 + b3 ) нетрудно привести к виду

(a + b)3 = a3 + 3ab(a + b) + b3 D
используя для этого вспомогательный пакетный нормализаторD выделяющий 4скрытые4 повторные вхождения одного и того же выраженияF Подвыражение a + b здесь встречается дваждыD и для вспомогательной переменнй y получаем следствиеX

aby (a - число & b - число & y = a + b y 3 - 3aby = a3 + b3 )F
Здесь все неизвестные члены сгруппированы слеваD а известные E справаF Далее реализуется цепочка обобщенийD основанных на том же принципеD что и для квадратного уравненияX выбирается подвыражение без неизвестныхD которое обозначается вспомогательным параметромF Прежде всегоD для -3ab вводится параметр cF Подставляемое вместо a выражение определяется из уравнения -3ab = cD и получаем первый шаг цепочки обобщенийX

bcy (b-число & ѓ(b = 0) & c-число & y = -c/(3b)+b y 3 +cy = -c3 /(27b3 )+b3 )F
На следующем шаге E вводим для выражения -c3 /(27b3 ) + b3 вспомогательный параметр aF Уравнение -c3 /(27b3 ) + b3 = a легко решаетсяD так как преобраE зуется к квадратному относительно b3 F В результате получаем формулу корня кубического уравненияD не имеющего члена с квадратом неизвестнойX

abcy (c - число & ѓ(c = 0) & a - число & 0 4c3 + 27a2 & y = -c/(3b) + b & 3 b = 3 3a - 4c3 + 27a2 /( 3 2 3) y 3 + cy = a)
Для остальных шагов цепочки обобщенийD связанных с добавлением коэффиE циента при y 3 и члена с y 2 D создание приемов вывода не составляет трудаF При обучении решателя 4вручную4 обычно создаются лишь те приемыD которые необходимы для текущей задачиF Множество аналогичных приемовD которые понаE добились бы в близких задачахD при этом пропускаютсяF Именно их отсутствием @а вовсе не переборными трудностямиA обычно и объясняются отказы решателяF ПроцеE дура программирующего вывода позволяет восполнять такие недостачи и приносит большую пользу даже как дополнительный элемент среды 4ручного4 программироE ванияF С помощью весьма скромного аппарата вывода теоремD созданного на текущий моментD в решатель были занесены многие десятки полезных приемовF

RQ


Схема алгоритмизации предметной области
При развитии решателя была создана целая пирамида языков E ЛОСD ГЕНОЛОГD логический ассемблерF ВидимоD для задания одного отдельного приема уровень лоE гического ассемблера E наивысший возможныйF ОднакоD возникает потребность в языке еще более высокого уровня E для задания неких общих эвристических принциE пов алгоритмизации предметной области как единого целогоD своего рода ее 4схемы алгоритмизации4F Здесь можно было бы фиксировать решения о создании в предметE ной области различных пакетных операторов и их использованииD решения о специE ализированной контекстной стандартизации термов и тFпF В настоящее время такие решения фиксируются с помощью термов технического характераD помещаемых в базу теорем E так называемых 4протоколов базы теорем4F Приведем несколько приE меров протоколовF IF Указание контекстной стандартизацииX числители и знаменатели дробных выE ражений в условии задачи на преобразовании разлагаются на множителиF Имеется несколько таких протоколовD уточняющих различные контекстыF КажE дый из них задает пакетный нормализаторD с помощью которого реализуется попытка разложения на множителиF Эти протоколы являются источниками приемовD выполняющих стандартизациюF Анализ связанных с дробями тожE деств легко объясняет ее происхождениеX подготовка возможности сокращеE ния дробных выраженийD а также упрощение сложения таких выражений при усмотрении общих множителей в знаменателях либо в числителяхF Обобщая данную ситуациюD можно создать прием для процедурыD планирующей схему алгоритмизацииF PF Указание контекстной стандартизацииX раскрывание скобок под тригонометриE ческими операциямиF Для каждой тригонометрической операции создан свой протоколF Он служит источником приемаD обращающегося к специальному нормализатору раскрыE вания скобокD если усматривается возможность преобразовать операнд тригоE нометрической операции к виду суммыF Данный протокол учитывается в друE гих приемахD чтобы заблокировать обратное преобразованиеF Происхождение рассматриваемой стандартизации очевидноX существуют тождества для тригоE нометрических операций от суммы либо разности аргументовD и не существует тождеств для аргументов E произведений либо степенейF QF Указание контекстной стандартизацииX преобразование логарифмов к общему основаниюF Протокол определяет создание приемовD преобразующих в различных ситуациE ях логарифмы к общему основаниюF Источником этих приемов служит тождеE ство для перехода к новому основаниюD а спецификаторD создающий по нему приемыD учитывает существование протоколаF Мотивировка ввода протокола планировщиком схемы алгоритмизации тривиальнаX большинство имеющихся базисных тождеств относятся к логарифмам с одинаковыми основаниямиF RF Решение о создании в алгебре множеств стандартной формы 4объединение пеE ресечений4F Протокол фиксирует факт создания нормализатора стандартной формыD преE образующего выражения алгебры множеств к виду объединения пересечений RR


либо разностейF Этот протокол служит источником приемовD предпринимаюE щих попытку упростить выражение алгебры множеств с помощью приведения к данной стандартной формыD использования ее упрощающих тождеств и поE следующей сверткиF Приемы различаются точкой привязки E той операцией алгебры множествD при усмотрении которой выполняется попыткаF SF Решение о создании нормализатора вычисленияX регистрация всего аппарата формального интегрирования в рамках пакетного нормализатораF Протокол служит источником приемаD обращающегося к данному нормализаE тору для вычисления неопределенного интегралаF

Автоматическая доводка приемов по задачнику
Чтобы обеспечить разумное взаимодействие нового приема с ранее созданными приE емамиD необходим анализ его срабатываний на задачах и определенная коррекция E 4доводка4F В первую очередьD должен быть уточнен уровень срабатывания приемаF Необходимая для доводки информация появляетсяD как только находятся задачиD в которых срабатывание приема является полезнымF Программа доводчика подбираE ет по этим задачам уровень срабатыванияD минимизируя суммарное время их решеE нияF Сохраняется информация о контекстах срабатывания приема в данных задачахY такие контексты называются 4позитивными4F Затем реализуется цикл решения всех задач из тех разделов задачникаD в которых возможно срабатывание приемаF НахоE дятся задачиD у которых после создания приема решение оказалось утраченным либо ощутимо замедлилосьF Уточняется информация о контекстах срабатывания приема в последних задачахY эти контексты называются 4негативными4F После выявления списков позитивных и негативных контекстов срабатывания приемаD доводчик предE принимает попытку перейти к подтипам данного типа приемаD чтобы отсечь его сраE батывания во всех негативных случаяхD сохранив срабатывания во всех позитивныхF Иногда приходится разбивать один прием на несколькоD имеющих различные типы и уровни срабатыванияF Помимо разделения позитивных и негативных контекстовD доводчик также анаE лизирует замедление 4холостого хода4D тFеF замедление решения тех задачD где прием вообще не срабатывалF Если идентификация приема трудоемкаD то замедление холоE стого хода может оказаться значительнымD и тогда доводчик увеличивает уровень срабатывания приемаF Программа доводчика развивалась для доводки приемов решения планиметричеE ских задачD причем оказалась способной воссоздавать приемыD созданные вручнуюD иногда даже несколько улучшая их качествоF

Генератор приемов
Перечисленные выше блоки программирующего выводаD характеризацииD создания спецификации приемаD компиляции спецификацийD планирования алгоритмизации предметной области и доводки приема позволяют проследить весь процесс перехода от базисной теоремы к приемуD и в этом смысле образуют аппарат автоматическоE го синтеза приемовF Возможны следующие способы применения данного аппарата @генератора приемовA в процессе самообучения логической системыX IF Синтез приемов при первом ознакомлении с теоремойF RS


Применяется программирующий выводD позволяющий сопоставить новую теоE рему с ранее известными и получить полезные ее следствияF В некоторых слуE чаях они уже будут сопровождены характеристикамиD в других E понадобится процедура характеризацииF Далее выполняются синтез спецификаций приемов и компиляция их в ГЕНОЛОГовские описания приемовF По такой схеме будут синтезироваться лишь наиболее естественные и хорошо мотивированные приемыF Для их отбора потребуются эвристические ограничиE телиF Обычно в учебниках новые теоремы сопровождаются простыми упражE нениямиD которые можно использовать для калибровки уровней срабатывания введенных указанным образом приемовF PF Синтез приемов при решении нестандартной задачиF Если попытка решить задачу 4в лоб4 либо со стандартными средствами усиE ления оказалась неудачнойD то предпринимается повторная попыткаD в котоE рой разрешается синтезировать дополнительные приемыF Вводятся специальE ные приемы решателяD усматривающие в текущем контексте целесообразность создания дополнительных приемов заданного типаF При помощи соответствуюE щих справочников поиска теорем @либо при непосредственном просмотре оглавE ления теоремA отбираются нужные теоремыD для которых либо сразу создаются приемы искомого типаD либо предварительно предпринимается программируюE щий выводD ориентированный на потребности решаемой задачиF После синтеза приемов попытка решения повторяетсяF Если после нескольких обращений к генератору приемов задачу удается решитьD то отбираются фактически испольE зованные новые приемыD которые оптимизируются доводчиком и сохраняются в базе приемовF Остальные приемы удаляютсяF QF Синтез приемовD подсказанный усилителемF Если после неудачной попытки решения задачи 4в лоб4 было получено ее реE шение с помощью стандартного усилителя @тFеF без синтеза дополнительных приемовAD то анализируется протокол решения задачиF В нем рассматриваютE ся точкиD где последовательное применение нескольких слабо мотивированных шагов @напримерD при локальном перебореA дало сильно мотивированное дейE ствиеF В базе теорем находятся теоремыD определяющие указанные слабо мотиE вированные шагиD и реализуется программирующий выводD воспроизводящий получение сильно мотивированного шагаF Найденная теорема представляет соE бой искусственную 4заготовку4D которая может оказаться полезной в будущемF По ней создается новый приемD который оптимизируется доводчикомF Более подробному описанию логической системы 4Искра4 посвящена монография 4Компьютерное моделирование логических процессов4F В первом томе этой моноE графии I описываются архитектура системыD а также языки ЛОС и ГЕНОЛОГF В следующих трех томах будут приведены приемы решателяD созданные при обучении его в таких разделахD как дискретная математикаD теория множествD элементарная алгебраD математический анализD дифференциальные уравненияD элементарная геоE метрияD аналитическая геометрияD линейная алгебраD комплексный анализD теория вероятностейD элементарная физикаD элементарная химияD вычисленияD понимание естественного языкаD шахматы и анализ рисунковF В настоящее время подготовлены первые два из этих трех томовF НаконецD в пятом томе монографии предполагается описать блоки генератора приемовF RT


Логическая система возникала и развивалась исключительно за счет анализа приE меровF В основе ее лежит база приемов решателяD извлекаемая в процессе обучения из разнообразных задачниковF Эта база приемов послужила исходным материалом для выявления архитектуры генератора приемов и его обученияF Если какие E то технические решения оказывались малоэффективными при работе с примерамиD то они отбрасывалисьY работоспособные версии E сохранялисьF В этом смыслеD компьюE терное моделирование сыграло роль 4микроскопа4 для изучения мира логических процессовF Продолжение обучения логической системы на всех ее уровнях позволит уточнить найденные архитектурные решения и вплотную подойти к созданию искусE ственного интеллектаF Автор выражает искреннюю благодарность ВFБF КудрявцевуD поддержка которого сделала возможным проведение данного исследованияF Л и т е р а т у р аF IF Подколзин АFСF Компьютерное моделирование логических процессовF АрхитекE тура и языки решателя задачF МFD ФизматлитD PHHVF

RU