Satisfiability Modulo Theories (SMT) solvers decide satisfiability of
formulas of first-order logic over various background theories, e.g.,
bit vectors. For instance, if x denotes a bit vector,
then x = (x bitand (bitnot x)) is satisfiable (a
satisfying assignment is given by x := 0). The
formula x = bitnot x, on the other hand, is
unsatisfiable.
Some SMT solvers can generate proofs of unsatisfiability. These proofs typically contain thousands of inference steps, and the proof rules used by SMT solvers are often complex. Consequently, checking these proofs poses a challenge.
The HOL4 interactive theorem prover, on the other hand, is based on a very simple inference kernel that provides about a dozen primitive rules. Its correctness is therefore relatively easy to verify.
The goal of this project is to translate proofs about bit vectors (e.g., those generated by the SMT solver Z3) into HOL4 proofs. A similar translation has already been implemented for proofs that do not involve bit vectors, and can be taken as a foundation for this project. The translation should eventually become part of the HOL4 system. Therefore, it must be implemented in Standard ML.