3

As far as I understand, then Coq have built-in First Order Logic https://coq.inria.fr/tutorial/1-basic-predicate-calculus. But Coq is not theorem prover, Coq is proof assistant and that means that user is required to provide some hints what rules/strategies Coq should select in each step. There exists more ore lest combined heuristic strategies, but, still, Coq is not prover. I have heard about efforts to use machine learning or other heuristics to automate the proof procedure in the proof assistants (they have been named *hammer?), some of these trends are published in http://ai4reason.org/activities.html.

My question is - can Coq be configured to be used as FOL theorem prover in a similar capacity as E-prover or Z3 prover for the first order logic? And - if yes - how can I configure Coq for such use?

TomR
  • 2,696
  • 6
  • 34
  • 87

1 Answers1

2

If you want to find a proof automatically of a first order statement within a Coq proof you can use the standard tactic firstorder, of the reconstruction tactics of Coq hammer (see below).

If you want to use Coq to solve problems presented in the tptp format, there is this tool https://github.com/lukaszcz/tptp2coq which can translate a tptp file into a Coq file, then you can use some automated tactics to solve the goals, but it will not compete with E-prover or Z3.

There is a also the tool, Coq hammer which will translate the Coq goal to FOL and then run FOF provers such as E, Vampire, Z3. If those FOF provers can find a proof, Coq hammer will use the list of lemmas used in the proof to try to find again the proof in Coq using automatic tactics (this is called proof reconstruction).

Julien Narboux
  • 148
  • 7