search

harp-project / AML-Formalization

GNU Lesser General Public License v2.1
9 stars 5 forks source link

Integrate with an SMT Solver #375

Open h0nzZik opened 1 year ago

h0nzZik commented 1 year ago

The SMTCoq plugin (https://smtcoq.github.io/) can be used in Coq to solve some goals automatically. I wonder if we could reuse SmtCoq for solving propositional and first-order goals in matching logic.

Essentially, the plugin converts the goal to a query that is sent to an SMT solver, then takes the proof object generated by the solver, represents it as a term inhabiting some inductive type, and lifts it up to the Coq level. We could reuse the interaction with the SMT, and only write our own conversion from a ML goal to FOL, and then the lifting of the proof object to the type of ML proof.

daniel-horpacsi commented 1 year ago

Section 4.3 in the AML technical report presents a conservative extension theorem for MSFOL, which may be of use when it comes to reasoning about the conversions.