Please use this identifier to cite or link to this item: doi:10.22028/D291-24991
Title: Unification in monoidal theories is solving linear equations over semirings
Author(s): Nutt, Werner
Language: English
Year of Publication: 1992
OPUS Source: Kaiserslautern ; Saarbrücken : DFKI, 1992
SWD key words: Künstliche Intelligenz
DDC notations: 004 Computer science, internet
Publikation type: Report
Abstract: Although for numerous equational theories unification algorithms have been developed there is still a lack of general methods. In this paper we apply algebraic techniques to the study of a whole class of theories, which we call monoidal. Our approach leads to general results on the structure of unification algorithms and the unification type of such theories. An equational theory is monoidal if it contains a binary operation which is associative and commutative, an identity for the binary operation, and an arbitrary number of unary symbols which are homomorphisms for the binary operation and the identity. Monoidal theories axiomatize varieties of abelian monoids. Examples are the theories of abelian monoids (AC), idempotent abelian monoids (ACI), and abelian groups. To every monoidal theory we associate a semiring. Intuitively, semirings are rings without subtraction. We show that every unification problem in a monoidal theory can be translated into a system of linear equations over the corresponding semiring. More specifically, problems without free constants are translated into homogeneous equations. For problems with free constants inhomogeneous equations have to be solved in addition. Exploiting the correspondence between unification and linear algebra we give algebraic characterizations of the unification type of a theory. In particular, we show that with respect to unification without constants monoidal theories are either unitary or nullary. Applying Hilbert's Basis Theorem we prove that theories of groups with commuting homomorphisms are unitary with respect to unification with and without constants.
Link to this record: urn:nbn:de:bsz:291-scidok-37964
Series name: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Series volume: 92-01
Date of registration: 1-Jul-2011
Faculty: SE - Sonstige Einrichtungen
Department: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
RR_92_01.pdf24,39 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.