Можно сказать, что автоматическое доказательство теорем – одна из старейших частей искусственного интеллекта. Благодаря исследованиям в области автоматического доказательства теорем были формализованы алгоритмы поиска и разработаны языки формальных представлений, такие как исчисление предикатов и логический язык программирования PROLOG.

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

К сожалению, в ранних пробах написать программу для автоматического доказательства теорем не удалось разработать систему, которая бы единообразно решала сложные задачи. Это было обусловлено способностью любой относительно сложной логической системой сгенерировать бесконечное количество доказуемых теорем: без мощных методик и эвристик, которые бы направляли поиск, программы доказывали большие количества не относящихся к делу теорем, пока не натыкались на нужную. Из-за этой неэффективности многие утверждают, что чисто формальные синтаксические методы управления поиском в принципе не способны справиться с такими большими пространствами, и единственная альтернатива этому – положиться на неформальные, специально подобранные к случаю стратегии, как это, похоже, делают люди. Это один из подходов, лежащих в основе экспертных систем, и он оказался достаточно плодотворным.

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

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