Equational reasoning in Isabelle
- 31 July 1989
- journal article
- Published by Elsevier in Science of Computer Programming
- Vol. 12 (2) , 123-149
- https://doi.org/10.1016/0167-6423(89)90038-5
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- The foundation of a generic theorem proverJournal of Automated Reasoning, 1989
- Reveur-3: the implementation of a general completion procedure parameterized by built-in theories and strategiesScience of Computer Programming, 1987
- Termination of rewritingJournal of Symbolic Computation, 1987
- Completion of a Set of Rules Modulo a Set of EquationsSIAM Journal on Computing, 1986
- Natural deduction as higher-order resolutionThe Journal of Logic Programming, 1986
- A higher-order implementation of rewritingScience of Computer Programming, 1983
- An Efficient Unification AlgorithmACM Transactions on Programming Languages and Systems, 1982