Decision procedures are automated theorem proving algorithms which
automatically recognize the theorems of some decidable theory. The
correctness of these algorithms is important, since a design error
could lead to the misidentification of a false statement as a
theorem. In the past, decision procedures have been shown to be
correct by mechanically verifying that they are sound, i.e. they only
identify valid statements. Soundness does not entail correctness,
however, as a decision procedure could still fail to recognize a true
formula from the theory it decides. To rigorously verify that a
decision procedure for a theory T is correct, it must also be shown to
be complete in that it recognize all true propositions from T . We
have developed a decision procedure called bagahk for the validity of
formulas modulo the theory of ground equations T=, which we have
proven sound and complete in the proof assistant Coq. In this thesis,
we highlight the important lemmas and theorems of these proofs. As
part of the soundness proof, we embed Coq-level proof terms into the
meta-language of our solver using reflection. As a result of this,
bagahk can also be used to assist users in the construction of other
proofs. In addition, we develop a proof system for T= and show that
our decision procedure recognizes all T=-provable propositions,
showing that bagahk is complete.