"Те длинные цепи" для разных, часто совсем не геометрических вещей кует сегодня вычислительная машина молотом резолюции.
Героиня задачи "Обезьяна и бананы" может отказаться от ненадежных услуг ЛЮБОЗАРа и предпочесть ему обязательную резолюцию. Впрочем, обезьяны давно пользовались методом резолюции, не ручаюсь за всех обезьян, но мартышки точно пользовались.
Об этом свидетельствует басня И. Крылова, в которой мартышка жаждет освоить очки: "то к темю их прижмет, то их на хвост нанижет, то их понюхает, то их полижет". Перебирает варианты, пытается извлечь хотя бы одну резольвенту, а не выходит, "очки не действуют никак". Мартышке, увы, надоедает перебор, она отказывается от резолюции, а могла бы после некоторого числа попыток приладить очки к глазам.
Программа для доказательства теорем в отличие от мартышки имеет железные нервы. Она спокойно перебирает все формально допустимые возможности. В задаче об обезьяне и бананах она даже пробует поставить ящик на голову обезьяне. Все логические атомы сопоставляются друг с другом, ни один камень не остается не перевернутым.
Резолюция вызывает энтузиазм специалистов, проявления которого очевидны, например, в отрывке из совсем свежей научной статьи: "Система доказательства теорем чарует и влечет. В самом деле, она универсальна, упорядочена и ее достоинства имеют подтверждение; опираясь на правильные входные данные, она весело и непринужденно приведет вас к искомому результату".
Итак, "мартышкин труд" предпочтительней эвристик. ЛЮБОЗАР с его колебаниями и отсутствием гарантий успешного решения должен уступить дорогу властной резолюции. Машинная логика сама, без человека одолеет любые препятствия.
Против этой достаточно распространенной постановки вопроса возражает академик В. Глушков: "Такая постановка не соответствует опыту, накопленному в других областях применения ЭВМ".
И предлагает совсем иной подход к машинному доказательству теорем. Центральной фигурой в нем является человек, квалифицированный математик, активно взаимодействующий с машиной. Чтобы взаимодействие было возможным, необходим язык, удобный для математика и понятный для ЭВМ. Чтобы взаимодействие было плодотворным, машину следует вооружить Алгоритмом Очевидности. Язык и Алгоритм - два краеугольных камня, на которых должно быть воздвигнуто новое здание "математического обеспечения для математических доказательств".
В. Глушков изложил свои новаторские идеи в начале 1965 года. Сейчас, в августе 1977 года, мы беседуем о развитии этих идей с ближайшим сотрудником В. Глушкова, профессором Ю. Капитоновой. Задаю ей естественный вопрос:
