Как настроить Coq в качестве средства доказательства теорем для логики первого порядка

Question

Насколько я понимаю, в Coq встроена логика первого порядка https://coq.inria.fr/tutorial/1-basic-predicate-calculus. Но Coq не доказатель теорем, Coq - помощник по проверке, и это означает, что пользователь должен предоставить некоторые подсказки, какие правила / стратегии следует выбирать Coq на каждом шаге. Существует больше руды, чтобы комбинированные эвристические стратегии, но, тем не менее, Coq не доказывает. Я слышал об усилиях по использованию машинного обучения или другой эвристики для автоматизации процедуры проверки в помощниках по проверке (они были названы * молоток?), Некоторые из этих тенденций опубликованы в http://ai4reason.org/activities.html.

У меня вопрос - можно ли настроить Coq для использования в качестве средства доказательства теорем FOL с той же емкостью, что и средство проверки E или Pro3 для логики первого порядка? И - если да - как я могу настроить Coq для такого использования?

Answer 1

Если вы хотите автоматически найти доказательство утверждения первого порядка в доказательстве Coq, вы можете использовать стандартную тактику первого порядка тактики реконструкции молотка Coq (см. Ниже).

Если вы хотите использовать Coq для решения проблем, представленных в формате tptp, есть этот инструмент https://github.com/lukaszcz/tptp2coq, который может переводить файл tptp в файл Coq, тогда вы можете использовать некоторые автоматизированные тактики для решения целей, но он не будет конкурировать с E-Prover или Z3.

Существует также инструмент Coq hammer, который переводит цель Coq в FOL, а затем запускает программы проверки FOF, такие как E, Vampire, Z3. Если эти доказывающие FOF смогут найти доказательство, Coq hammer будет использовать список лемм, использованных в доказательстве, чтобы попытаться снова найти доказательство в Coq, используя автоматическую тактику (это называется реконструкцией доказательства).