Editing Unification (computer science) (section)

===Particular background knowledge sets E===
{|
|+ '''Used naming conventions'''
| {{math|∀ ''u'',''v'',''w'':}}
| align="right" | {{tmath|u*(v*w)}}
| {{=}}
| {{tmath|(u*v)*w}}
| align="center" | '''{{mvar|A}}'''
| Associativity of {{tmath|*}}
|-
| {{math|∀ ''u'',''v'':}}
| align="right" | {{tmath|u*v}}
| =
| {{tmath|v*u}}
| align="center" | '''{{mvar|C}}'''
| Commutativity of {{tmath|*}}
|-
| {{math|∀ ''u'',''v'',''w'':}}
| align="right" | {{tmath|u*(v+w)}}
| {{=}}
| {{tmath|u*v+u*w}}
| align="center" | '''{{mvar|D<sub>l</sub>}}'''
| Left distributivity of {{tmath|*}} over {{tmath|+}}
|-
| {{math|∀ ''u'',''v'',''w'':}}
| align="right" | {{tmath|(v+w)*u}}
| {{=}}
| {{tmath|v*u+w*u}}
| align="center" | '''{{mvar|D<sub>r</sub>}}'''
| Right distributivity of {{tmath|*}} over {{tmath|+}}
|-
| {{math|∀ ''u'':}}
| align="right" | {{tmath|u*u}}
| {{=}}
| {{mvar|u}}
| align="center" | '''{{mvar|I}}'''
| Idempotence of {{tmath|*}}
|-
| {{math|∀ ''u'':}}
| align="right" | {{tmath|n*u}}
| {{=}}
| {{mvar|u}}
| align="center" | '''{{mvar|N<sub>l</sub>}}'''
| Left neutral element {{mvar|n}} with respect to {{tmath|*}}
|-
| {{math|∀ ''u'':}}
| align="right" | {{tmath|u*n}}
| {{=}}
| {{mvar|u}}
| align="center" | &nbsp; &nbsp; '''{{mvar|N<sub>r</sub>}}''' &nbsp; &nbsp;
| Right neutral element {{mvar|n}} with respect to {{tmath|*}}
|}

It is said that ''unification is decidable'' for a theory, if a unification algorithm has been devised for it that terminates for ''any'' input problem.
It is said that ''unification is [[semi-decidable]]'' for a theory, if a unification algorithm has been devised for it that terminates for any ''solvable'' input problem, but may keep searching forever for solutions of an unsolvable input problem.

''Unification is decidable'' for the following theories:
* '''{{mvar|A}}'''<ref>[[Gordon D. Plotkin]], ''Lattice Theoretic Properties of Subsumption'', Memorandum MIP-R-77, Univ. Edinburgh, Jun 1970</ref>
* '''{{mvar|A}}''','''{{mvar|C}}'''<ref>[[Mark E. Stickel]], ''A Unification Algorithm for Associative-Commutative Functions'', Journal of the Association for Computing Machinery, vol.28, no.3, pp. 423–434, 1981</ref>
* '''{{mvar|A}}''','''{{mvar|C}}''','''{{mvar|I}}'''<ref name="Fages.1987">F. Fages, ''Associative-Commutative Unification'', J. Symbolic Comput., vol.3, no.3, pp. 257–275, 1987</ref>
* '''{{mvar|A}}''','''{{mvar|C}}''','''{{mvar|N<sub>l</sub>}}'''<ref group=note name="LRequivC">in the presence of equality '''{{mvar|C}}''', equalities '''{{mvar|N<sub>l</sub>}}''' and '''{{mvar|N<sub>r</sub>}}''' are equivalent, similar for '''{{mvar|D<sub>l</sub>}}''' and '''{{mvar|D<sub>r</sub>}}'''</ref><ref name="Fages.1987"/>
* '''{{mvar|A}}''','''{{mvar|I}}'''<ref>Franz Baader, ''Unification in Idempotent Semigroups is of Type Zero'', J. Automat. Reasoning, vol.2, no.3, 1986</ref>
* '''{{mvar|A}}''','''{{mvar|N<sub>l</sub>}}'''{{mvar|,}}'''{{mvar|N<sub>r</sub>}}''' (monoid)<ref>J. Makanin, ''The Problem of Solvability of Equations in a Free Semi-Group'', Akad. Nauk SSSR, vol.233, no.2, 1977</ref>
* '''{{mvar|C}}'''<ref>{{cite journal| author=F. Fages| title=Associative-Commutative Unification| journal=J. Symbolic Comput.| year=1987| volume=3| number=3| pages=257–275| doi=10.1016/s0747-7171(87)80004-4| s2cid=40499266| url=https://hal.inria.fr/inria-00076271/file/RR-0287.pdf}}</ref>
* [[Boolean ring]]s<ref>{{cite book| author=Martin, U., Nipkow, T.| chapter=Unification in Boolean Rings| title=Proc. 8th CADE| year=1986| volume=230| pages=506–513| publisher=Springer| editor=Jörg H. Siekmann| series=LNCS}}</ref><ref>{{cite journal|author1=A. Boudet |author2=J.P. Jouannaud |author3=M. Schmidt-Schauß | title=Unification of Boolean Rings and Abelian Groups| journal=Journal of Symbolic Computation| year=1989| volume=8|issue=5 | pages=449–477 | doi=10.1016/s0747-7171(89)80054-9| doi-access=free}}</ref>
* [[Abelian group]]s, even if the signature is expanded by arbitrary additional symbols (but not axioms)<ref name="Baader and Snyder 2001, p. 486">Baader and Snyder (2001), p. 486.</ref>
* [[Kripke semantics#Correspondence and completeness|K4]] [[modal algebra]]s<ref>F. Baader and S. Ghilardi, ''[https://web.archive.org/web/20171223215706/https://pdfs.semanticscholar.org/492e/9f03ab7abd043ed0167dc7309552d21a88ef.pdf Unification in modal and description logics]'', Logic Journal of the IGPL 19 (2011), no.&nbsp;6, pp.&nbsp;705–730.</ref>

''Unification is semi-decidable'' for the following theories:
* '''{{mvar|A}}''','''{{mvar|D<sub>l</sub>}}'''{{mvar|,}}'''{{mvar|D<sub>r</sub>}}'''<ref>P. Szabo, ''Unifikationstheorie erster Ordnung'' (''First Order Unification Theory''), Thesis, Univ. Karlsruhe, West Germany, 1982</ref>
* '''{{mvar|A}}''','''{{mvar|C}}''','''{{mvar|D<sub>l</sub>}}'''<ref group=note name="LRequivC"/><ref>Jörg H. Siekmann, ''Universal Unification'', Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS vol.170, pp. 1–42, 1984</ref>
* [[Commutative ring]]s<ref name="Baader and Snyder 2001, p. 486"/>