Proof movie — A proof with the Boyer-Moore prover
Debora Weber-Wulff · Formal Aspects of Computing · 1993
Abstract This paper uses the Boyer-Moore prover for developing a proof of correctness for the implementation of a very small compiler. The polished version of the proof is included as an appendix. The major intent of the paper is to describe the process of proving using an automatic theorem prover.