Существуют ли высокоуровневые API/среды/библиотеки для проверки эффективности конкретного подхода (например, эвристического алгоритма) для создания конструктивных доказательств на основе логики первого порядка/теории типов?
Я пытаюсь найти удобный API, который может проверять правильность доказательств для таких формул, как: .
Если возможно, я бы предпочел автономные библиотеки вместо прямого интерфейса для таких языков, как Coq/HOL.
Заранее спасибо!
Не в общем, нет.
Логика первого порядка полуразрешима. Короче говоря, это означает, что если есть доказательство, его всегда можно найти. Если его нет, вы можете найти опровержение или бесконечно пытаться его найти. Ни одна система не даст вам готовых доказательств/опровержений для всех формул логики первого порядка.
Конечно, даже если есть доказательства, нет никакой гарантии, что вы сможете их быстро найти. Таким образом, на практике поиск доказательств за разумное количество времени/ресурсов является сложной задачей, даже если они существуют. Теоретически вы всегда можете это сделать, если готовы ждать достаточно долго.
Это теоретическая сторона дела. На практике современные SMT-решатели могут многое, особенно если вас интересуют леммы, возникающие на практике при верификации программно-аппаратных средств; вместо чистой математики. Например, пример, который вы использовали, можно закодировать на языке SMTLib следующим образом:
(assert (not (forall ((a Int)) (=> (>= a 0) (exists ((b Int)) (> b a))))))
(check-sat)
и может быть легко доказано, например, с помощью z3 (при условии, что вы поместили приведенный выше текст в файле с именем a.smt2):
$ z3 a.smt2
unsat
Здесь мы утверждали отрицание того, что хотели доказать, и z3 сказал, что unsatдостоверно, что означает, что исходное утверждение на самом деле является теоремой. Нужно немного прищуриться, чтобы увидеть переписку, но она хорошо установлена. Кроме того, если ваша формула не является теоремой, решатель SMT может дать вам конкретный контрпример; что хорошо для отладки или установления ложности.
Это не означает, что z3 (или любой другой SMT-решатель) решит все формулы, которые вы ему подбрасываете, из коробки. Особенно с чередованием квантификаторов, они могут найти ответ или отказаться от попыток, сказав unknown, или они могут зацикливаться навсегда.
Несомненно, вы уже знаете, что подходящим инструментом для решения таких проблем являются средства доказательства теорем, такие как Coq/Hol/Isabelle/ACL2 и т. д.; но вы явно ищете что-то кнопочное. Я думаю, что решатели SMT близки к тому, что вы хотите, с той оговоркой, что они имеют как врожденные ограничения, как я упоминал выше, так и то, что делает их текущий набор эвристик и механизмов проверки. Они, безусловно, улучшатся со временем, но полной автоматизации у вас никогда не будет.
Подводя итог, все зависит от того, какова ваша цель на самом деле. Для проблем, возникающих при практических задачах проверки программного/аппаратного обеспечения, решатели SMT помогут вам далеко; с дополнительным преимуществом, что они понимают много теорий. (Арифметика, массивы, структуры данных, и это лишь некоторые из них.) Кроме того, их легко программировать, так как большинство решателей предоставляют высокоуровневые API на многих высокоуровневых языках, а большинство языков программирования имеют привязки, облегчающие их программирование. использовать.
Однако если вас интересует чистая математика, я не думаю, что вы сможете избежать полуавтоматического мира доказательства теорем. Попробуйте заглянуть в Lean, который представляет собой, например, современное средство для доказательства теорем с широкими возможностями программирования. Обратите внимание, что большинство средств доказательства теорем уже имеют тактику, использующую преимущества SMT-решателей, поэтому, хотя вам приходится писать доказательство вручную, вам может помочь множество средств автоматизации.
