## Canonical equational proofs |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

STANDARD COMPLETION | 13 |

EXTENDED COMPLETION | 39 |

ORDERED COMPLETION | 73 |

Copyright | |

2 other sections not shown

### Other editions - View all

### Common terms and phrases

A-critical pairs A-unifiers associative-commutative Bachmair binary relation Boolean rings Church-Rosser cliff complete reduction ordering completion procedure congruence relations contains convergent modulo convergent rewrite system convergent system covering set critical overlap critical pair criterion Critical Pair Lemma deletion Dershowitz equational theories exists a ground extended rules fair with respect finite function symbols ground convergent ground instance ground reducible ground terms Horn clauses inductive completion inductive theorem inference rules inference system irreducible Jouannaud Lect left-hand side left-linear lexicographic path ordering multiset non-overlap normal forms Notes in Comput ordered completion pair criteria paramodulation peak Proc proof by consistency proof complexity proof ordering proof Q proof step proper overlap proper subterm provably inconsistent rewrite proof modulo rewrite relation rewrite rules s w t s y t set of equations simplification standard completion subset substitution term rewriting systems terminating theorem proving transformation rules unifier variable overlap well-founded