Using SMT-prover to generate proof

[j123123]

It is possible to implement Hilbert-style deduction system in SMT language and then get the proof. Here is an example in attachment. Hilbert_system.txt

I encoded axiom from Metamath http://us.metamath.org/ileuni/ax-1.html http://us.metamath.org/ileuni/ax-2.html http://us.metamath.org/ileuni/ax-mp.html and it works, I was able to prove some theorem using https://verit.loria.fr/ SMT solver and get the proof, but proof is very long and not human-readable.

So, how about using some SMT-prover to generate proof for mm0 theorem and then check it in mm0 (like SMTCoq)?

[digama0]

The main problems I have had in the past with SMT solvers is that they have a poorly defined proof format and elaborating everything into a formal proof is sometimes difficult. That said I haven't looked at veriT specifically so perhaps things have improved. Assuming this hurdle is overcome, it would be possible to turn such a proof into an MM0 proof, either as a standalone file that is imported into an existing development, or as a tactic to be used from MM1. Either way, it would be compiled down to a pure MM0 proof and then an MM0 verifier would not need to know anything about SMT to check the proof.

[j123123]

I am wondering what is the best way to rewrite the axioms. Maybe like that:

; (IMPL a (IMPL b a)) <=> a
; like http://us.metamath.org/mpeuni/ax-1.html
(assert
  (forall ( (a M_wff) (b M_wff) )
    (=
      (M_impl a (M_impl b a))
      a
    )
  )
)

; (IMPL
;   (IMPL a (IMPL b c))
;   (IMPL (IMPL a b) (IMPL a c))
; )
; <=>
; (IMPL
;
;   (IMPL
;     (IMPL a (IMPL b c))
;     (IMPL (IMPL a b) (IMPL a c))
;   )
;
;   (AND3 a b c)
;
; )
; like http://us.metamath.org/mpeuni/ax-2.html

(assert
  (forall ( (a M_wff) (b M_wff) (c M_wff) )
    (=

      (M_impl
        (M_impl a (M_impl b c))
        (M_impl (M_impl a b) (M_impl a c))
      )

      (M_impl
        (M_impl
          (M_impl a (M_impl b c))
          (M_impl (M_impl a b) (M_impl a c))
        )
        (M_a3 a b c)
      )

    )
  )
)

; (AND2 a (IMPL a b)) <=> (AND2 a b)
; like http://us.metamath.org/mpeuni/ax-mp.html

(assert
  (forall ( (a M_wff) (b M_wff) )
    (=
      (M_a2 a (M_impl a b))
      (M_a2 a b)
    )
  )
)

With this, z3 is able to prove theorem like http://us.metamath.org/ileuni/syl.html

And what about Why3? If I understand correctly, WhyML is some intermediate language, which can be converted in Coq language, or SMT-Lib, or Isabelle/HOL etc. so if encode MM0 in WhyML language, all this things can be used to automatically/semi-automatically/manually prove MM0 theorem and then extract proof into MM0 and verify it.

[digama0]

As I understand it, Why3 is itself a frontend, that translates to various backend provers. MM0 is closer to a backend language and so it would be more appropriate to target the provers directly or adapt what Why3 does. Another issue is that Why3 does not receive or translate proofs from the backend provers, it simply trusts the yes/no response from the solver. For MM0 this is insufficient because the goal is to construct an MM0 proof term.

Regarding translating the axioms, I think this is the wrong way around. MM0 is likely to be more powerful than the FOL prover in question, and more to the point the mapping itself is axiom-dependent, you can't do it in for general MM0 databases (or at least you would have to deeply embed everything to the point that automatic provers will likely have a tough job seeing past it all).

Instead, you would fix some MM0 axiomatization (for example peano.mm1 or set.mm1), which sets the ground rules, defines the basic logical connectives and so on, and then construct a map FOL -> MM0 with a partial inverse MM0 -> FOL, where "FOL" means the language accepted by the solver. The partial inverse determines which theorems are amenable to automatic proof, and the FOL -> MM0 map has to also be proof preserving, i.e. FOL-proof -> MM0-proof, which means that for every proof step the FOL prover can take there has to be an analogous MM0 theorem. The MM0 axioms need not fit in the FOL fragment or have any FOL equivalent.

It is the FOL-proof -> MM0-proof map that worries me the most. I've tried to work with Z3 before, which has an ok proof output, but the "modulo theories" part of SMT is a doozy, because it will e.g. produce 1-step proofs of any theorem in presburger arithmetic, which is a bit problematic for peano.mm1 since that's almost everything. The rationale is that these are decidable theories, so you "just" have to write a decision procedure for presburger in order to elaborate the proof.