Developing Sound and Complete Decision Procedures in Coq

Benjamin Delaware


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.