Editing Boolean ring (section)

== Unification ==
[[Unification (logic)|Unification]] in Boolean rings is [[Decidability (logic)|decidable]],{{sfn|Martin|Nipkow|1986|ps=none}} that is, algorithms exist to solve arbitrary equations over Boolean rings. Both unification and matching in [[finitely generated algebra|finitely generated]] free Boolean rings are [[NP-complete]], and both are [[NP-hard]] in [[finitely presented algebra|finitely presented]] Boolean rings.{{sfn|Kandri-Rody|Kapur|Narendran|1985|ps=none}} (In fact, as any unification problem {{math|1=''f''(''X'') = ''g''(''X'')}} in a Boolean ring can be rewritten as the matching problem {{math|1=''f''(''X'') + ''g''(''X'') = 0}}, the problems are equivalent.)

Unification in Boolean rings is unitary if all the uninterpreted function symbols are nullary and finitary otherwise (i.e. if the function symbols not occurring in the signature of Boolean rings are all constants then there exists a [[most general unifier]], and otherwise the [[Unification (computer science)#Unification problem, solution set|minimal complete set of unifiers]] is finite).{{sfn|Boudet|Jouannaud|Schmidt-Schauß|1989|ps=none}}