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

АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМ (также известное как автоматическая дедукция) — подраздел автоматизированных рассуждений и математической логики, занимающийся доказательством математических теорем с помощью компьютерных программ. Автоматическое рассуждение над математическим доказательством стало основным стимулом для развития информатики.

• Логические основы 

В то время как корни формализованной логики восходят к Аристотелю, современная логика и формализованная математика появились в конце 19-го и начале 20-го веков. В своей «Begriffsschrift (1879) Готлоб Фреге представил полное исчисление высказываний и то, что, по существу, составляет современную логику предикатов. Его «Die Grundlagen der Arithmetik», опубликованные в 1884 году, [1] выражают (части) математики в формальной логике. Этот подход был продолжен Расселом и Уайтхедом в их влиятельных «Principia Mathematica» («Принципы математики»), впервые изданных в 1910–1913 гг.[2] и с пересмотренным вторым изданием в 1927 году [3]. Рассел и Уайтхед считали, что они могут вывести всю математическую истину, используя аксиомы и правила вывода формальной логики, в принципе открывая дорогу для автоматизации. В 1920 годе норвежский математик Туральф Альберт Скулем упростил предыдущий результат, достигнутый Леопольдом Лёвенгеймом, что привело к появлению теоремы Лёвенгейма — Скулема, а в 1930 г. к понятию Вселенной Эрбрана и интерпретации Эрбрана, что позволило появиться формулам первого порядка и, следовательно, справедливость теоремы, сводится к потенциально бесконечному множеству проблем пропозициональной выполнимости [Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration].
В 1929 году польский математик еврейского происхождения Мойжеш Пресбургер показал, что теория натуральных чисел со сложением и равенством (теперь называемая в его честь арифметикой Пресбургера) разрешима, и дал алгоритм, который мог определить, было ли данное предложение в языке истинным или ложным [Presburger, Mojżesz (1929). «Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt». Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101]. Однако вскоре после этого положительного результата австрийский логик Курт Фридрих Гёдель опубликовал «On Formally Undecidable Propositions of Principia Mathematica and Related Systems» (1931 г.), показывая, что в любой достаточно сильной аксиоматической системе есть истинные утверждения, которые невозможно доказать в системе. Эта тема получила дальнейшее развитие в 1930-х годах Алонзо Чёрчем и Аланом Тьюрингом, которые, с одной стороны, дали два независимых, но эквивалентных определения вычислимости, а с другой — конкретные примеры неразрешимых вопросов.

• Автоматическое доказательство теорем исчисления предикатов 

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

• Практическое использование 

Коммерческое использование автоматического доказательства теорем, в основном, сосредоточено в разработке и проверке интегральных схем. После аппаратной ошибки «Pentium» FDIV, сложные модули с плавающей запятой современных микропроцессоров разрабатывались уже с особой тщательностью. «AMD», «Intel» и другие используют автоматическое доказательство теорем, чтобы убедиться, что деление и другие операции в их процессорах реализуются верно.

© При копировании активная ссылка на сайт обязательна

См. Алфавитный указатель статей Большой энциклопедии знаний