Equational Reasoning in Isabelle

Tobias Nipkow

This paper reports on a case study carried out with the generic theorem prover Isabelle. The purpose of this study was to investigate the process of instantiating a generic system like Isabelle for a particular logic (equational logic in this case). Isabelle is like a compiler-compiler, except that it compiles a logic definition into an LCF-style theorem prover for that logic. To make that theorem prover usable, a number of logic-specific ``tactics'', embodying useful theorem proving techniques in that logic, must be built on top. Equational logic was chosen as a test case because it comes with a large body of well tried algorithms. It will be shown how a variety of different algorithms in the area of equational reasoning can be implemented in a unified way using a powerful tactic language. The problems tackled are term rewriting, unification and inductive theorem proving and the tactic language is ML.


@article{Nipkow-SCP-89, author="Tobias Nipkow", title="Equational Reasoning in {Isabelle}", journal="Science of Computer Programming", year=1989,volume=12,pages="123--149"}