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.
BibTeX:
<![CDATA[
@article{Nipkow-SCP-89,
author="Tobias Nipkow",
title="Equational Reasoning in {Isabelle}",
journal="Science of Computer Programming",
year=1989,volume=12,pages="123--149"}
]]></plaintext></p></div></div>