Equational inference, canonical proofs, and proof orderings
- 1 March 1994
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 41 (2) , 236-276
- https://doi.org/10.1145/174652.174655
Abstract
We describe the application of proof orderings—a technique for reasoning about inference systems-to various rewrite-based theorem-proving methods, including refinements of the standard Knuth-Bendix completion procedure based on critical pair criteria; Huet's procedure for rewriting modulo a congruence; ordered completion (a refutationally complete extension of standard completion); and a proof by consistency procedure for proving inductive theorems.Keywords
This publication has 23 references indexed in Scilit:
- Automating inductionless induction using test setsJournal of Symbolic Computation, 1991
- A completion procedure for conditional equationstJournal of Symbolic Computation, 1991
- Completion for rewriting modulo a congruenceTheoretical Computer Science, 1989
- Critical pair criteria for completionJournal of Symbolic Computation, 1988
- Only prime superpositions need be considered in the Knuth-Bendix completion procedureJournal of Symbolic Computation, 1988
- Proof by consistencyArtificial Intelligence, 1987
- Termination of rewritingJournal of Symbolic Computation, 1987
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Proving termination with multiset orderingsCommunications of the ACM, 1979