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