Combination Problems for Commutative/Monoidal Theories: How Algebra Can Help in Equational Reasoning

Franz BaaderFranz Baader, W. NuttW. Nutt

Franz Baader, W. Nutt
Combination Problems for Commutative/Monoidal Theories: How Algebra Can Help in Equational Reasoning
J. Applicable Algebra in Engineering, Communication and Computing, 7(4):309-337, 1996

Details
Bibtex

KurzfassungAbstract
We study the class of theories for which solving unification problems is equivalent to solving systems of linear equations over a semiring. It encompasses important examples like the theories of Abelian monoids, idempotent Abelian monoids, and Abelian groups. This class has been introduced by the authors independently of each other as ``commutative theories (Baader) and ``monoidal theories (Nutt).
We show that commutative theories and monoidal theories indeed define the same class (modulo a translation of the signature), and we prove that it is undecidable whether a given theory belongs to it. In the remainder of the paper we investigate combinations of commutative/monoidal theories with other theories. We show that finitary commutative/monoidal theories always satisfy the requirements for applying general methods developed for the combination of unification algorithms for disjoint equational theories.
Then we study the adjunction of monoids of homomorphismss to commutative/monoidal theories. This is a special case of a non-disjoint combination, which has an algebraic counterpart in the corresponding semiring. By studying equations over this semiring, we identify a large subclass of commutative/monoidal theories that are of unification type zero by. We also show with methods from linear algebra that unitary and finitary commutative/monoidal theories do not change their unification type when they are augmented by a finite monoid of hom s, and how algorithms for the extended theory can be obtained from algorithms for the basic theory.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ BaaderNutt-AAECC-96,
  author = {F. {Baader} and W. {Nutt}},
  journal = {J. Applicable Algebra in Engineering, Communication and Computing},
  number = {4},
  pages = {309--337},
  title = {Combination Problems for Commutative/Monoidal Theories: {H}ow Algebra Can Help in Equational Reasoning},
  volume = {7},
  year = {1996},
}