Utilize FFI to reconstruct cvc5 proofs in Lean.

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.

Apache License 2.0

93 stars 19 forks source link

Utilize FFI to reconstruct cvc5 proofs in Lean. #77

Closed abdoo8080 closed 8 months ago

abdoo8080 commented 8 months ago

This PR utilizes the new Lean FFI interface for cvc5 to reconstruct cvc5 proofs into Lean proofs. The reconstruction supports most rules for boolean and EUF theories.