Автоматизированное доказательство теорем (также известное как ATP или автоматизированный вывод ) — это область автоматизированных рассуждений и математической логики , связанная с доказательством математических теорем с помощью компьютерных программ . Автоматизация рассуждений над математическими доказательствами явилась важным стимулом для развития компьютерных наук .
Хотя корни формализованной логики восходят к Аристотелю , в конце 19-го и начале 20-го веков развивалась современная логика и формализованная математика. Begriffsschrift Фреге ( 1879) представил как полное исчисление высказываний , так и то, что по существу является современной логикой предикатов . [1] Его «Основы арифметики» , опубликованные в 1884 году, [2] выражали (частично) математику в формальной логике. Этот подход был продолжен Расселом и Уайтхедом в их влиятельных Principia Mathematica , впервые опубликованных в 1910–1913 гг .[3] и с исправленным вторым изданием в 1927 году. [4] Рассел и Уайтхед думали, что они могут вывести всю математическую истину, используя аксиомы и правила вывода формальной логики, в принципе открывая процесс для автоматизации. В 1920 году Торальф Скулем упростил предыдущий результат Леопольда Левенгейма , что привело к теореме Левенгейма-Скулема , а в 1930 году — к понятию вселенной Гербранда и интерпретации Гербранда , которая допускала (не)выполнимость формул первого порядка (и, следовательно, справедливость теоремы ) сводится к (потенциально бесконечному количеству) пропозициональных проблем выполнимости. [5]
В 1929 году Мойжеш Пресбургер показал, что теория натуральных чисел со сложением и равенством (теперь называемая арифметикой Пресбургера в его честь) разрешима , и дал алгоритм, который мог определить, является ли данное предложение в языке истинным или ложным. [6] [7] Однако вскоре после этого положительного результата Курт Гёдель опубликовал книгу «О формально неразрешимых утверждениях принципов математики и родственных систем» (1931 г.), показав, что в любой достаточно сильной аксиоматической системе есть истинные утверждения, которые не могут быть доказаны в системе . Эта тема получила дальнейшее развитие в 1930-х годах Алонсо Черчем иАлан Тьюринг , который с одной стороны дал два независимых, но эквивалентных определения вычислимости , а с другой привел конкретные примеры для неразрешимых вопросов.
Вскоре после Второй мировой войны появились первые компьютеры общего назначения. В 1954 году Мартин Дэвис запрограммировал алгоритм Пресбургера для компьютера с электронными лампами JOHNNIAC в Институте перспективных исследований в Принстоне, штат Нью-Джерси. По словам Дэвиса, «его великим триумфом было доказать, что сумма двух четных чисел четна». [7] [8] Более амбициозной была Logic Theory Machine в 1956 году, система дедукции для пропозициональной логики Principia Mathematica , разработанная Алленом Ньюэллом , Гербертом А. Саймоном и Дж. К. Шоу .. Также работающий на JOHNNIAC, Logic Theory Machine построил доказательства из небольшого набора пропозициональных аксиом и трех правил вывода: modus ponens , (пропозициональная) подстановка переменных и замена формул их определением. Система использовала эвристическое руководство и сумела доказать 38 из первых 52 теорем Principia . [7]
«Эвристический» подход Логической Теоретико-Машины пытался подражать человеческим математикам и не мог гарантировать, что доказательство может быть найдено для каждой действительной теоремы даже в принципе. Напротив, другие, более систематические алгоритмы достигли, по крайней мере теоретически, полноты для логики первого порядка. Первоначальные подходы основывались на результатах Хербранда и Скулема для преобразования формулы первого порядка в последовательно большие наборы пропозициональных формул путем создания экземпляров переменных с терминами из вселенной Хербранда . Затем пропозициональные формулы можно было бы проверить на невыполнимость, используя ряд методов. Программа Гилмора использовала преобразование в дизъюнктивную нормальную форму , форму, в которой выполнимость формулы очевидна.[7] [9]