ДОКАЗАТЕЛЬСТВО ТЕОРЕМ НА ЭВМ, машинный поиск логического вывода
— направление в теоретической кибернетике, изучающее возможности моделирования на электронной вычислительной машине мыслительной деятельности математика. Важность этого направления обусловлена тем, что в математике легче, чем в других видах творчества, формализовать и условие решаемой задачи, и элементарные шаги, допустимые при ее решении, и проверку результата (как и во всех областях творчества, сам процесс мышления поддается формализации с огромным трудом и потерями).
Теоретической предпосылкой для Д. т. на ЭВМ явилось создание логики математической, формализовавшей понятие логического вывода теоремы из аксиом. Еще до появления ЭВМ в работах классиков матем. логики были разработаны методы, составившие реальную базу практ. алгоритмов поиска вывода. Первые попытки практически построить машинные программы установления выводимости были сделаны в США в начале 50-х гг. Программа «логик-теоретик» работала с распространенной, но крайне неудобной для поиска вывода формулировкой одной простой теории (см. Исчисление высказываний). Поэтому практические результаты этой программы были очень незначительны. Однако использованная в ней методика оказалась полезной и имела принципиальное значение для формирования направления, получившего название программирование эвристическое. Существенно более интересные логич. теоремы были доказаны с помощью программы Хао Вана, легшей в основу другого направления в автоматизации доказательств. В дальнейшем первое направление было продолжено (напр., Гелернтер использовал анализ чертежей для организации процесса доказательства геом. теорем). Однако подавляющее большинство работ по Д. т. на ЭВМ вслед за Хао Ваном базируется, в первую очередь, на разработке методов матем. логики. Объединение достижений теории логич. вывода и эвристического программирования пока не осуществлено.
Круг теорем, реально доказанных на ЭВМ, ограничен, и теоремы эти не очень сложны. Соответствующие доказательства часто опирались на существенную помощь со стороны человека либо в виде «подсказывающей» формулировки исходной задачи, либо даже в виде
указаний по ходу ее решения (напр., «использовать такую-то лемму», «провести индукцию по такой-то ф-ле» и т. п.). Помимо ряда логич. теорем были доказаны некоторые теоремы элементарной алгебры, элементарной и проективной геометрии, а также элементарной теории чисел. Напр., такие: «если квадрат каждого элемента равен единице, то группа коммутативна», «квадратный корень из простого числа иррационален», «простых чисел бесконечно много». Сложность доказательства двух последних теорем, по-видимому, приближается к границам современных возможностей маш. поиска вывода. Т. о., пока мало надежд на машинное доказательство по-настоящему сложных теорем, тем более теорем, которые не удается доказать человеку. Поэтому больший интерес представляют не достигнутые практические результаты, а постановки задач и методы. Имеется несколько способов Д. т. на ЭВМ. При доказательстве теоремы значительную часть тех. работы математик может поручить ЭВМ, если по ходу доказательства возникает большой объем вычислений или множество вариантов, каждый из которых легко рассматривается. Этим способом получены, напр., некоторые результаты по теории чисел. Хотя проведение таких доказательств часто требует от математика специальной ориентировки хода своих рассуждений на использование ЭВМ, но этот способ выпадает, строго говоря, из проблематики маш. поиска вывода. Способ перспективен, но пока его возможности использованы мало. Другой способ — это кооперирование математика и ЭВМ, при котором человек определяет принципиальное направление доказательства и высказывает гипотезы, а машина проделывает все промежуточные логич. переходы и выкладки, проверяет гипотезы и выдает материал для формирования дальнейших гипотез. Это направление только начинает развиваться и требует, помимо теор. разработок, дальнейшего совершенствования систем связи человека с ЭВМ. К этому направлению примыкают задачи корректирования гипотез и естественного поиска вывода.
Наиболее распространена следующая постановка проблемы автоматизации доказательств: матем. теория формализуется (базой для формализации служит исчисление предикатов), теоремы теории превращаются в ф-лы, выводимые из тех или иных аксиом, требуется построить алгоритм установления выводимости, т. е. алгоритм, который дает правильный ответ на вопрос о выводимости ф-лы и должен кончать работу для всех выводимых ф-л, но для некоторых (или для всех) невыводимых ф-л может работать бесконечно долго. Такая постановка снязана с неразрешимостью подавляющего большинства интересных теорий (т. е. принципиально невозможно построить алгоритм, распознающий выводимость для всех ф-л в языке теории). Существуют и др. постановки проблемы. 1) Поиск высококачественного вывода. Качественность вывода не уточняется, но имеются в виду выводы возможно более компактные (недопустимы излишние применения правил), как можно более «склеенные» (одно и то же вспомогательное утверждение не следует выводить дважды на разных этапах доказательства), записанные в естественном, привычном для математика виде. В Ленинградском отделении Матем. института им. В. А. Стеклова был разработан и запрограммирован алгоритм, который находил в рамках исчисления высказываний естественный вывод утверждения из списка гипотез и записывал этот вывод в виде логико-матем. текста на русском языке. 2) Корректирование гипотез и усиление теорем. Разрабатываются методы, позволяющие вводить в заданную ф-лу небольшие исправления так, чтобы она стала теоремой или (если исходная ф-ла выводима) превратилась в более сильную теорему. Исследуются критерии качества исправлений. 3) Полуразрешающие алгоритмы. Опираясь на наличие у неразрешимых теорий значительных разрешимых фрагментов, разрабатывают разрешающие процедуры для этих фрагментов, а также алгоритмы установления выводимости, кончающие работу для возможно более широких классов ф-л. В качестве основы почти всех предлагавшихся алгоритмов установления выводимости можно рассматривать аппарат секвенциальных исчислений (см. Генцена формальные системы). Эти исчисления часто позволяют организовать процесс поиска вывода «снизу вверх» — путем определения по каждой ф-ле F сравнительно небольшого числа ее возможных «непосредственных предшественников», т. е. ф-л, из которых F может быть выведена. В простейших случаях уже одно это дает реальную возможность установления выводимости. Однако для исчисления предикатов такой поиск часто приводит к огромному к-ву «лишних» ф-л, что делает невозможным непосредственное применение этого метода. Был предложен способ, в соответствии с которым ищется «снизу вверх» не сам вывод, а некоторая его «заготовка» с неуточненными значениями используемых переменных. На определенных этапах построения заготовки проверяется, нельзя ли так уточнить значения переменных, чтобы получить уже настоящий вывод. Этот метод позволяет избавиться от излишеств в выводе и приблизиться к практическим алгоритмам, но проверка сложной заготовки представляет собой непомерно трудную задачу. Поэтому более перспективны методы, сочетающие иеуточненность значений переменных со сравнительной простотой каждого шага работы: метод резолюций, применимый к классическому исчислению предикатов, и обратный метод, применимый почти ко всем секвенциальным исчислениям. Для повышения практической эффективности этих методов решающее значение имеет изучение т. н. «стратегий», накладывающих те или иные ограничения на процесс установления выводимостп. Рассматриваются способы включения в схему этих методов специфических механизмов аксиоматических теорий, правил для равенства и индукции, более сложных формальных языков и др.
Проблемой автоматизации доказательств занимаются в СССР, США, Великобритании, Швеции, ФРГ, Польше и др. странах. Спец. международные симпозиумы «Машинный разум» происходят ежегодно в Эдинбурге (Великобритания). Два всесоюзных симпозиума по машинному поиску вывода состоялись в Тракае (Лит. ССР). См. также Автоматизированный поиск доказательств теорем.
Лит.: Шанин Н. А. [и др.]. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний. М.-Л., 1965; Математическая теория логического вывода. М., 1967; Маслов С. Ю. Обратный метод установления выводимости для логических исчислений. «Труды Математического института им. В. А. Стеклова АН СССР», 1968, т. 98; Вычислительные машины и мышление. Пер. с англ. М., 1967 [библиогр. с. 491—546]; Кибернетический сборник. Новая серия, в. 7. М., 1970; Machine intelligence. Edinburg, 1971.
С. Ю. Маслов.
