Искусственный интеллект

В качестве формальных систем математические теории не обязательно должны быть наглядными или «интуитивно истинными» - наглядность и интуитивная достоверность не являются их критериями истинности. Достаточно лишь, чтобы эти теории были бы формально правильными, свободными от внутренних противоречий. В рамках формальной аксиоматики система аксиом может быть также исследована на предмет наличия таких свойств, как независимость какой-либо аксиомы от других, полнота, категоричность, и т.д. Традиционным способом проверки истинности, формальной правильности математических доказательств является их перепроверка другими математиками, сообщество которых выступает в роли окончательных «верховных» судей. Однако математики тоже люди, и они могут ошибаться - такие случае широко известны из истории научного познания. Формализация доказательств автоматизировала вычисления и тем самым создала предпосылки для конструирования современной вычислительной техники. Создание такой техники, в свою очередь, открыла новые возможности для проверки правильности математических доказательств и их поиска компьютером. Первые попытки использовать ЭВМ для проверки и получения логико-математических доказательств были предприняты еще в 50-х гг. XX в. (программа «Логический Теоретик»), К настоящему времени эта область применения ЭВМ значительно расширилась, причем перечень проблем, решаемых только компьютером, постоянно пополняется.

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