Editing Unification (computer science) (section)

===One-sided paramodulation===
If there is a [[convergent term rewriting system]] ''R'' available for ''E'',
the ''one-sided paramodulation'' algorithm<ref>N. Dershowitz and G. Sivakumar, ''Solving Goals in Equational Languages'', Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, Springer LNCS vol.308, pp. 45–55, 1988</ref>
can be used to enumerate all solutions of given equations.

{| style="border: 1px solid darkgray;"
|+ One-sided paramodulation rules
|- border="0"
| align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''f''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>) }
| ; ''S''
| ⇒
| align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ ''t''<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ ''t''<sub>''n''</sub> }
| ''; ''S''
|
| &nbsp; &nbsp; ''decompose''
|-
| align="right" | ''G'' ∪ { ''x'' ≐ ''t'' }
| ; ''S''
| ⇒
| align="right" | ''G'' { ''x'' ↦ ''t'' }
|; ''S''{''x''↦''t''} ∪ {''x''↦''t''}
| align="right" | if the variable ''x'' doesn't occur in ''t''
| &nbsp; &nbsp; ''eliminate''
|-
| align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''t'' }
| ; ''S''
| ⇒
| align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ u<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ u<sub>''n''</sub>, ''r'' ≐ ''t'' }
| ; ''S''
| align="right" | &nbsp; &nbsp; if ''f''(''u''<sub>1</sub>,...,''u''<sub>''n''</sub>) → ''r'' is a rule from ''R''
| &nbsp; &nbsp; ''mutate''
|-
| align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''y'' }
| ; ''S''
|⇒
| align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ ''y''<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ ''y''<sub>''n''</sub>, ''y'' ≐ ''f''(''y''<sub>1</sub>,...,''y''<sub>''n''</sub>) }
| ; ''S''
| align="right" | if ''y''<sub>1</sub>,...,''y''<sub>''n''</sub> are new variables
| &nbsp; &nbsp; ''imitate''
|}

Starting with ''G'' being the unification problem to be solved and ''S'' being the identity substitution, rules are applied nondeterministically until the empty set appears as the actual ''G'', in which case the actual ''S'' is a unifying substitution. Depending on the order the paramodulation rules are applied, on the choice of the actual equation from ''G'', and on the choice of ''R''{{'}}s rules in ''mutate'', different computations paths are possible. Only some lead to a solution, while others end at a ''G'' ≠ {} where no further rule is applicable (e.g. ''G'' = { ''f''(...) ≐ ''g''(...) }).

{| style="border: 1px solid darkgray;"
|+ Example term rewrite system ''R''
|- border="0"
| '''1'''
| ''app''(''nil'',''z'')
| → ''z''
|-
|'''2''' &nbsp; &nbsp;
| ''app''(''x''.''y'',''z'')
| → ''x''.''app''(''y'',''z'')
|}

For an example, a term rewrite system ''R'' is used defining the ''append'' operator of lists built from ''cons'' and ''nil''; where ''cons''(''x'',''y'') is written in infix notation as ''x''.''y'' for brevity; e.g. ''app''(''a''.''b''.''nil'',''c''.''d''.''nil'') → ''a''.''app''(''b''.''nil'',''c''.''d''.''nil'') → ''a''.''b''.''app''(''nil'',''c''.''d''.''nil'') → ''a''.''b''.''c''.''d''.''nil'' demonstrates the concatenation of the lists ''a''.''b''.''nil'' and ''c''.''d''.''nil'', employing the rewrite rule 2,2, and 1. The equational theory ''E'' corresponding to ''R'' is the [[congruence closure]] of ''R'', both viewed as binary relations on terms.
For example, ''app''(''a''.''b''.''nil'',''c''.''d''.''nil'') ≡ ''a''.''b''.''c''.''d''.''nil'' ≡ ''app''(''a''.''b''.''c''.''d''.''nil'',''nil''). The paramodulation algorithm enumerates solutions to equations with respect to that ''E'' when fed with the example ''R''.

A successful example computation path for the unification problem { ''app''(''x'',''app''(''y'',''x'')) ≐ ''a''.''a''.''nil'' } is shown below. To avoid variable name clashes, rewrite rules are consistently renamed each time before their use by rule ''mutate''; ''v''<sub>2</sub>, ''v''<sub>3</sub>, ... are computer-generated variable names for this purpose. In each line, the chosen equation from ''G'' is highlighted in red. Each time the ''mutate'' rule is applied, the chosen rewrite rule (''1'' or ''2'') is indicated in parentheses. From the last line, the unifying substitution ''S'' = { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' } can be obtained. In fact,
''app''(''x'',''app''(''y'',''x'')) {''y''↦''nil'', ''x''↦ ''a''.''nil'' } = ''app''(''a''.''nil'',''app''(''nil'',''a''.''nil'')) ≡ ''app''(''a''.''nil'',''a''.''nil'') ≡ ''a''.''app''(''nil'',''a''.''nil'') ≡ ''a''.''a''.''nil'' solves the given problem.
A second successful computation path, obtainable by choosing "mutate(1), mutate(2), mutate(2), mutate(1)" leads to the substitution ''S'' = { ''y'' ↦ ''a''.''a''.''nil'', ''x'' ↦ ''nil'' }; it is not shown here. No other path leads to a success.

{| class="wikitable"
|+ Example unifier computation
|-
! Used rule !!  !! ''G'' !! ''S''
|-
| ||
| { {{color|red|''app''(''x'',''app''(''y'',''x'')) ≐ ''a''.''a''.''nil''}} }
| {}
|-
| mutate(2) || ⇒
| { ''x'' ≐ ''v''<sub>2</sub>.''v''<sub>3</sub>, ''app''(''y'',''x'') ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>2</sub>.''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''a''.''nil''}} }
| {}
|-
| decompose || ⇒
| { {{color|red|''x'' ≐ ''v''<sub>2</sub>.''v''<sub>3</sub>}}, ''app''(''y'',''x'') ≐ ''v''<sub>4</sub>, ''v''<sub>2</sub> ≐ ''a'', ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| {}
|-
| eliminate || ⇒
| { ''app''(''y'',''v''<sub>2</sub>.''v''<sub>3</sub>) ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>2</sub> ≐ ''a''}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| { ''x'' ↦  ''v''<sub>2</sub>.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { {{color|red|''app''(''y'',''a''.''v''<sub>3</sub>) ≐ ''v''<sub>4</sub>}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| { ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| mutate(1) || ⇒
| { ''y'' ≐ ''nil'', ''a''.''v''<sub>3</sub> ≐ ''v''<sub>5</sub>, {{color|red|''v''<sub>5</sub> ≐ ''v''<sub>4</sub>}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| { ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { {{color|red|''y'' ≐ ''nil''}}, ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
| { ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, {{color|red|''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil''}} }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| mutate(1) || ⇒
| { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, ''v''<sub>3</sub> ≐ ''nil'', {{color|red|''v''<sub>4</sub> ≐ ''v''<sub>6</sub>}}, ''v''<sub>6</sub> ≐ ''a''.''nil'' }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>3</sub> ≐ ''nil''}}, ''v''<sub>4</sub> ≐ ''a''.''nil'' }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''v''<sub>3</sub> }
|-
| eliminate || ⇒
| { ''a''.''nil'' ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>4</sub> ≐ ''a''.''nil''}} }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|-
| eliminate || ⇒
| { {{color|red|''a''.''nil'' ≐ ''a''.''nil''}} }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|-
| decompose || ⇒
| { {{color|red|''a'' ≐ ''a''}}, ''nil'' ≐ ''nil'' }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|-
| decompose || ⇒
| { {{color|red|''nil'' ≐ ''nil''}} }
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|-
| decompose &nbsp; &nbsp; || ⇒ &nbsp; &nbsp;
| {}
| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
|}