3. Автоматическое доказательство теорем

Автоматическое доказательство теорем ведет свое начало от основополагающих работ Эрбрана, который еще в тридцатых годах прошлого столетия предложил механическую процедуру дедуктивного вывода. В шестидесятые годы усилиями Ньюэлла и Саймона был создан общий решатель проблем, доказывающий теоремы формальной логики, разработанной Расселом и Уайтхедом, которые считали, что для математики достаточно иметь формальный вывод теорем из основных аксиом.

Однако результаты Чёрча и Тьюринга о неразрешимости логики предикатов первого порядка в какой-то степени оттеснили работы Эрбрана на задний план. Интерес к ним возрос лишь в шестидесятые годы, когда Гилмор реализовал эрбрановскую процедуру вывода на компьютере. Действительно, если нет процедуры для проверки противоречивости (общезначимости) формул логики предикатов первого порядка, то самое большее, что можно сделать – это проверить противоречивость (общезначимость) формулы, если она на самом деле таковой и является. Гилмору удалось доказать с помощью процедуры Эрбрана ряд простых теорем из логики высказываний и логики предикатов первого порядка, но его программа столкнулась с неразрешимыми трудностями при доказательстве более сложных теорем логики предикатов.

Ненамного эффективнее был метод Девиса и Патнема, с помощью которого были доказаны некоторые теоремы из логики предикатов первого порядка, не доказанные Гилмором. В 1964-1965 гг. независимо друг от друга появились обратный метод установления выводимости Маслова и принцип резолюции Робинсона. В те же годы Шаниным и его коллегами было разработано несколько версий алгоритма машинного поиска естественного логического вывода в исчислении высказываний (АЛПЕВ). Разработка версий системы АЛПЕВ и машинных алгоритмов вывода на основе обратного метода и принципа резолюции показала принципиальную возможность машинных доказательств теорем.

Сейчас принято считать, что автоматические рассуждения на основе формальной логики относятся к слабым (weak) методам доказательства теорем, и чисто синтаксические методы управления поиском не способны обрабатывать огромное пространство поиска при решении задач практической сложности. Поэтому альтернативой являются неформальные методы поиска, ad hoc стратегии, эвристики и рассуждения здравого смысла, которые человек использует при решении проблем.

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

Конечно, доминирующий в автоматическом доказательстве теорем метод резолюции не является панацеей от всех бед, сопровождающих процедуры доказательства теорем, и мы вправе надеяться на появление более совершенных процедур дедуктивного вывода. Это касается и языка Пролог, неплохо зарекомендовавшего себя при решении логических проблем. Здесь можно согласиться с точкой зрения Н.Н. Непейводы, утверждавшего, что «есть смысл использовать Пролог для кусков программ, обладающих исключительно сложной логикой при явном задании вариантов. Все вычислительные части программ при этом стоит писать на других языках и иметь либо Пролог-программу, вызывающую вычислительные модули, либо (скажем) Паскаль-программу с внешней Пролог-подпрограммой».