Proofs and pictures: Proving the diamond lemma with the GROVER theorem proving system
Dave Barker-Plummer · 1992
In this paper we describe a theorem proving system called grover. grover is novel in that it may be guided in its search for a proof by information contained in a diagram. There are two parts to the system: the underlying theorem prover, called &, and the graphical subsystem which examines the diagram and makes calls to the underlying prover on the basis of the information found there. We have used grover to prove the Diamond Lemma, a non-trivial theorem from the theory of well-founded relations. Key words. Automated reasoning, graphical theorem proving, proof strategies. This material is based upon work supported by the National Science Foundation under award number ISI-8701133. 1 INTRODUCTION 2 1 Introduction Open almost any mathematics text book and you will find, along with the familiar symbolism of mathematics and motivational text, many diagrams which are included to help the reader visualize the particular point being made. One might be tempted to conclude that mathema...