Editing Knuth–Bendix completion algorithm (section)

==Rules==

Given a set ''E'' of equations between [[term (logic)|terms]], the following inference rules can be used to transform it into an equivalent [[convergent term rewrite system]] (if possible):<ref>{{cite book |author=Bachmair, L. |author2=Dershowitz, N. |author3=Hsiang, J. | chapter=Orderings for Equational Proofs| title=Proc. IEEE Symposium on Logic in Computer Science|date=Jun 1986| pages=346–357}}</ref><ref>{{cite book |author=N. Dershowitz |author2=J.-P. Jouannaud |author2-link=J.-P. Jouannaud | title=Rewrite Systems| year=1990| volume=B| pages=243–320| publisher=Elsevier| editor=Jan van Leeuwen| series=Handbook of Theoretical Computer Science}} Here: sect.8.1, p.293</ref>
They are based on a user-given [[reduction ordering]] (>) on the set of all terms; it is lifted to a well-founded ordering (▻) on the set of rewrite rules by defining {{math|(''s'' → ''t'') ▻ (''l'' → ''r'')}} if 
* {{math|''s'' [[encompassment ordering|{{underset|e|>}}]] ''l''}} in the [[encompassment ordering]], or
* {{mvar|s}} and {{mvar|l}} are [[variant (logic)|literally similar]] and {{math|''t'' > ''r''}}.

{|
|-
| '''Delete'''
| ‹ ''E''∪{''s'' = ''s''} 
| , ''R'' › 
| ⊢ 
| ‹ ''E'' 
| , ''R'' ›
|-
| '''Compose''' &nbsp; &nbsp; &nbsp; &nbsp;
| ‹ ''E''
| , ''R''∪{''s'' → ''t''} › &nbsp; &nbsp; &nbsp; &nbsp;
| ⊢  &nbsp; &nbsp; &nbsp; &nbsp;
| ‹ ''E'' 
| , ''R''∪{''s'' → ''u''} › &nbsp; &nbsp; &nbsp; &nbsp;
| if {{math|''t'' {{underset|''R''|⟶}} ''u''}}
|-
| '''Simplify'''
| ‹ ''E''∪{''s'' = ''t''} 
| , ''R'' › 
| ⊢
| ‹ ''E''∪{''s'' = ''u''}  
| , ''R'' ›
| if {{math|''t'' {{underset|''R''|⟶}} ''u''}}
|-
| '''Orient'''
| ‹ ''E''∪{''s'' = ''t''} 
| , ''R'' ›
| ⊢
| ‹ ''E''
| , ''R''∪{''s'' → ''t''}   ›
| if {{math|''s'' > ''t''}}
|-
| '''Collapse'''
| ‹ ''E''
| , ''R''∪{''s'' → ''t''} › 
| ⊢
| ‹ ''E''∪{''u'' = ''t''}
| , ''R'' ›
| if {{math|''s'' {{underset|''R''|⟶}} ''u''}} by {{math|''l'' → ''r''}} with {{math|(''s'' → ''t'') ▻ (''l'' → ''r'')}}
|-
| '''Deduce'''
| ‹ ''E''
| , ''R'' ›
| ⊢
| ‹ ''E''∪{''s'' = ''t''}
| , ''R'' ›
| if {{math|(''s'',''t'')}} is a [[critical pair (logic)|critical pair]] of ''R''
|}