История автоматизации поиска доказательства для исчисления предикатов
Компьютерная автоматизация поиска доказательства для исчисления предикатов – это направление исследований на стыке логики и теории искусственного интеллекта.
Родоначальником поиска общих разрешающих процедур для проверки общезначимых формул считается Лейбниц, который проводил изыскания еще в XVII веке. Продолжились исследования уже в XX веке. В 1936 году независимо друг от друга Черч и Тьюринг доказали, что общей разрешающей процедуры не существует, невозможно разработать универсальный алгоритм, который бы проверял общезначимость формул в логике предикатов (даже первого порядка). Тем не менее, были созданы алгоритмы для поиска доказательства, подтверждающие общезначимость формул (если они являются таковыми). Для необщезначимых формул такие алгоритмы не завершают работу.
Общезначимой называется формула, истинная при всех интерпретациях.
Важным для автоматического доказательства теорем стал подход, разработанный в 1930 году Эрбраном. Смысл алгоритма состоит в нахождении интерпретации, опровергающей рассматриваемую формулу. Однако для общезначимых формул таких интерпретаций не существует, и алгоритм завершается за конечное число шагов. Разработанный Эрбраном метод лежит в основе большинства современных систем автоматического поиска доказательств.
В 1959 году Гилмором была реализована процедура Элбрана. Программа предназначалась для того, чтобы обнаружить противоречивость отрицания анализируемой формулы. Формула является общезначимой тогда и только тогда, когда противоречиво ее отрицание. Программа Гилмора была неэффективной. В 1960 году Девис и Патнем улучшили ее. Однако эти улучшения оказались недостаточными и не позволяли доказать за разумное время общезначимость многих формул логики предикатов.
Программа Девиса работала на ламповом компьютере Johniac. Она на основе техники разрешимости для арифметики доказывала, что сумма двух четных чисел – четное число. Это было первым доказательством математических утверждений, сгенерированным ЭВМ.
А. Невел, Г. Саймон и Дж. К. Шоу создали программу, которая умела доказывать некоторые предложения из книги Б. Рассела и Н. Уайтхеда «Principia Mathematica». В 1958 Хао Ван написал программу автоматического доказательства, справляющуюся с 350 теоремами из «Principia Mathematica» для чистого исчисления предикатов с равенством.
Велика заслуга Робинсона, который в 1965 году ввел метод резолюций. Этот метод оказался эффективнее описанных ранее процедур. Позднее метод резолюций был дополнен рядом стратегий, увеличивающих его эффективность:
- семантической резолюцией,
- лок-резолюцией,
- линейной резолюцией,
- стратегией предпочтения единичных,
- стратегией поддержки.
Современные системы автоматизации поиска доказательства для исчисления предикатов
Современные системы автоматизации поиска доказательства для исчисления предикатов делятся на две группы:
- системы интерактивного поиска доказательства теорем. Второе название этих систем – редакторы доказательств. Они позволяют пользователям конструировать доказательство под контролем системы;
- автоматические генераторы доказательств. В них пользователь только ставит задачу («необходимо доказать теорему»), после чего генератор работает до обнаружения доказательства или выполнения условия останова.
Одной из наиболее популярных систем интерактивного поиска доказательства теорем является Coq. Coq предоставляет язык программирования и окружение для создания формальных доказательств. Он позволяет пользователям записывать математические утверждения и применять логические правила для доказательства этих утверждений. Coq также поддерживает автоматические тактики, которые могут автоматически выполнять некоторые части доказательства.
Другой известной системой интерактивного поиска доказательства теорем является Isabelle. Isabelle предоставляет окружение для формализации и проверки доказательств. Он использует логику второго порядка и предлагает различные инструменты для автоматического и интерактивного доказательства.
Системы интерактивного поиска доказательства теорем имеют множество применений в различных областях, включая математику, логику, компьютерные науки и теорию языков программирования. Они могут быть использованы для формализации и верификации программ, а также для разработки новых математических теорий.
Основное преимущество систем интерактивного поиска доказательства теорем заключается в том, что они обеспечивают высокую степень уверенности в правильности доказательств. Однако они требуют от пользователя значительных усилий и экспертизы в области формальной логики и математики.
Генерация доказательств является сложной задачей, требующей знания логических правил, математических теорем и способности применять их для решения конкретных проблем. Автоматические генераторы доказательств основаны на алгоритмах, которые пытаются найти формальное доказательство, используя заданные правила вывода и аксиомы.
Одним из самых известных автоматических генераторов доказательств является система Prover9, которая основана на методе резолюций и может генерировать доказательства в логике первого порядка. Еще один популярный инструмент - Z3, который предоставляет возможность генерации доказательств в различных формальных системах и языках программирования.
Однако, несмотря на значительные достижения в области автоматической генерации доказательств, они все же имеют свои ограничения. Некоторые математические проблемы могут быть слишком сложными для автоматического решения или требовать большого количества вычислительных ресурсов. Кроме того, автоматические генераторы доказательств могут быть подвержены ошибкам или генерировать неполные доказательства.
В целом, автоматические генераторы доказательств представляют собой мощный инструмент для автоматизации процесса доказательства теорем и верификации программного обеспечения.
