This is a lean library that tries to incorporate the power of SMT solvers. With a single tactic a proposition will be either proved or disproved (with the counter-model given).
Currently only booleans are supported; we only work with CVC4 for now. For examples, refer to src/cvc4/tactic.lean.
- smtlib
- complete the parser according to the smtlib specification.
- CVC4
- add other theories(integers, reals, binary vectors, etc.)
- get rid of
trust_f. As of CVC4 1.6 for booleans thetrust_fsimply asserts an assumption which is superfluous. For other theories, theory-specific auto prover is needed, or we shall ask CVC4 developers to detail these proofs instead oftrust_fassertion.
- add supports of other solvers(Z3, veriT)
- Z3 seems to have quite detailed theory specific proofs, but the documentation of the proof format and rules is lacking.
- veriT doesn’t seem to be better than CVC4, proof-wise.
This project is kindly funded by LSEC Fellowship.