АВТОМАТИЗИРОВАННЫЙ ПОИСК ДОКАЗАТЕЛЬСТВ ТЕОРЕМ

— взаимодействие человека с вычислительной машиной, направленное на поиск доказательств теорем. Система А. п. д. т. включает комплекс средств спец. матем. обеспечения ЭВМ, предназначенных не только для поиска доказательств теорем, но также для проверки на очевидность и новизну тех или иных утверждений в рассматриваемой теории, для корректирования гипотез, построения естественного доказательства, для информационно-справочных целей и т. п. Особенностью большинства работ по доказательству теорем на ЭВМ является стремление к созданию универсальных программ, ориентированных на самостоятельный поиск доказательства теорем машиной. Такой подход не соответствует опыту, накопленному в других областях применения ЭВМ. Естественный путь, которым идет машинная математика, — это развитие систем автоматизации программирования и средств взаимодействия человека с машиной. Этот путь является, по-видимому, одним из реалистических путей решения проблемы А. п. д. т. Он предполагает смещение центра тяжести работы в этой области от универсализации программ для ЭВМ к кооперации между математиком и ЭВМ, к созданию специализированных систем автоматизации программирования и операционных систем, позволяющих в случае необходимости быстро программировать поиск доказательства даже одной единственной теоремы и способных работать, если потребуется, в реальном масштабе времени с математиком, ищущим доказательство этой теоремы. Человек при этом определяет принципиальное направление, план доказательства, промежуточные гипотезы, различные методы и приемы доказательства, а машина реализует намеченный план поиска, применяет рекомендуемые человеком методы, проделывает промежуточные логические выкладки, а также выдает информацию о состоянии поиска, о полученных ею результатах и о неудачах — для принятия человеком решений.

В матем. обеспечении А. п. д. т. выделяют следующие составные части: средства для описания данных в системе (внеш. и внутр. языки системы); систему алгоритмов для решения различных задач, возникающих в процессе поиска; средства (язык) общения с системой в диалога режиме; спец. операционную систему; автоматизацию и методику программирования. Необходимо, чтобы формализованный язык для записи матем. теорий был удобным для практ. использования в процессе работы с системой. Для этого в него вводят достаточно богатый запас исходных предикатов, операций и ф-ций. Часть их свойств (напр., ассоциативность) учитывается уже во внутр. представлении языка, и это может значительно облегчить поиск. С целью повышения степени практичности языка целесообразно включить в объем понятия ф-ции и определенные конструкции, часто применяемые в обычном языке. Под конструкцией в общем случае понимается многозначная -местная ф-ция Напр., выражение «подмножество мн-ва М» можно рассматривать как одноместную неоднозначную ф-цию «подмножество ()», аргумент которой принимает значения из класса мн-в (т. е. имеет тип «множество»). Другие примеры конструкций: группа, подгруппа (G), единица (G). В описаниях конструкций должны быть описания возможного типа их аргументов и типа значений конструкции. Это позволит строить дерево конструкций в виде суперпозиций соответствующих конструкций. Выбор подходящей конструкции является одним из решающих моментов, обеспечивающих успех доказательства. Поиск доказательства с помощью машины удобно организовать как работу эвристических программ различных уровней, которые включены в комплекс средств спец. матем. обеспечения ЭВМ. Иерархическое построение программ позволяет быстро осуществить поиск одного из

вариантов доказательств. Программа нижнего уровня реализует т. н. алгоритм очевидности и содержит набор операторов-подпрограмм, задачей которых являются элементарные преобразования обрабатываемой информации. Эта программа перебирает варианты вывода, использующие простейшие логические и теоретико-множественные приемы, а также проверяет конкретные примеры и проводит аналитические выкладки. Большинство преобразований, выполняемых в процессе работы алгоритма очевидности, имитируют действия специалиста в схожих ситуациях. Программа более высокого уровня в зависимости от ситуации перераспределяет последовательность операторов 1-й программы, задавая тем самым некоторый новый метод доказательств. Программы еще более высоких уровней служат усовершенствованию программ низшего уровня, накапливанию опыта, самообучению и т. п. Если программы самого низшего уровня содержат эвристики, основой которых являются наиболее общие методы доказательства (метод цепного заключения, метод аналогии и т. п.), то программы 2-го уровня используют эвристики, разрабатываемые более сложно (эвристики распознавания образов, относящиеся к выбору наиболее эффективных методов или к выбору наивыгоднейших целей, семантические эвристики, основанные на использовании интерпретации среды, и многошаговые эвристики планирования). Наиболее же сложные эвристики используются программами самых высоких уровней: эвристики обобщения прошлого опыта и эвристики индуктивных предска-зании

Осн. средствами программирования в системе А. п. д. т. являются язык процедурно-ориентированный программирования и язык директив. Язык директив используется для обращения к отдельным рабочим программам в процессе поиска доказательства. Директиву может вводить пользователь, ее могут порождать рабочие программы в процессе работы. Система программ, составляющая специализированную операционную систему, распределяет ресурсы (компоненты оборудования ЭВМ) и определяет порядок выполнения инструкций, поступающих от пользователя.

Проблема А. п. д. т. связана с другой сложной и интересной проблемой — моделированием мышления и отличается от нее использованием в первую очередь не каких-либо творческих способностей машин, а их мощных исполнительских возможностей при постоянном взаимодействии с человеком. С развитием автоматизированных систем поиска доказательств и прежде всего алгоритмов поиска в направлении построения эвристической надстройки, роль математика будет состоять преимущественно в определении новых понятий и в формулировке новых предложений, а искусство доказать новую теорему с использованием машины будет состоять в умении сформулировать ряд промежуточных теорем и лемм.

Лит.: Чернявский А. Л. Моделирование процесса решения сложных логических задач на вычислительных машинах (эвристическое программирование). «Автоматика и телемеханика», 1967, № 1; Глушков В. М. Некоторые проблемы теории автоматов и искусственного интеллекта. «Кибернетика», 1970, М 2; Вычислительные машины и мышление. Пер. с англ. М., 1967 [библиогр. с. 491—546].

Ф. В. Ануфриев, 3. М. Аселъдеров, В. Ф. Костырко.

АВТОМАТИКА (греч. абтоиато? — самодействующий) — 1) Область теоретических и прикладных знаний об автоматически действующих устройствах и системах. Термин А. относится к более раннему периоду развития исследований и практических разработок в области автомат, регулирования и управления. В связи со становлением и быстрым развитием нового науч. направления — кибернетики — в его рамках определился крупный раздел — кибернетика техническая, в который как составная часть вошла А. в виде автоматического управления теории вместе с теор. и прикладными основами создания и организации функционирования соответствующих тех. средств (управляющих вычислительных машин, управляющих устройств, датчиков, исполнительных механизмов, а также устройств, обеспечивающих взаимодействие человека с вычислительной машиной в системах автоматизированных). 2) Совокупность механизмов и устройств, действующих автоматически. См. Агрегатная унифицированная система, Пневмоника, Телемеханика, Универсальная система элементов промышленной пневмоавто-Матики. Б. Б. Тимофеев.