Term Rewriting and Beyond - Theorem Proving in Isabelle
Tobias Nipkow
The subject of this paper is theorem proving based on rewriting and
induction. Both principles are implemented as tactics within the generic
theorem prover Isabelle. Isabelle's higher-order features enable us to go
beyond first-order rewriting and express rewriting with conditionals,
induction schemata, higher-order functions and program transformers.
Applications include the verification and transformation of functional
versions of insertion sort and quicksort.
BibTeX:
<![CDATA[
@article{Nipkow-FAC-89,
author="Tobias Nipkow",
title="Term Rewriting and Beyond --- Theorem Proving in {Isabelle}",
journal="Formal Aspects of Computing",
year=1989,volume=1,pages="320--338"}
]]></plaintext></p></div></div>