Term rewriting and beyond — theorem proving in Isabelle
- 1 March 1989
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 1 (1) , 320-338
- https://doi.org/10.1007/bf01887212
Abstract
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.Keywords
This publication has 14 references indexed in Scilit:
- Equational reasoning in IsabelleScience of Computer Programming, 1989
- Inductive proofs by resolution and paramodulationPublished by Springer Nature ,1989
- Higher-order abstract syntaxACM SIGPLAN Notices, 1988
- Complexity of matching problemsJournal of Symbolic Computation, 1987
- Natural deduction as higher-order resolutionThe Journal of Logic Programming, 1986
- REVE a rewrite rule laboratoryPublished by Springer Nature ,1986
- A higher-order implementation of rewritingScience of Computer Programming, 1983
- An Efficient Unification AlgorithmACM Transactions on Programming Languages and Systems, 1982
- Proving and applying program transformations expressed with second-order patternsActa Informatica, 1978
- A Transformation System for Developing Recursive ProgramsJournal of the ACM, 1977