SciDok

Eingang zum Volltext in SciDok

Lizenz

Report (Bericht) zugänglich unter
URN: urn:nbn:de:bsz:291-scidok-37964
URL: http://scidok.sulb.uni-saarland.de/volltexte/2011/3796/


Unification in monoidal theories is solving linear equations over semirings

Nutt, Werner

Quelle: (1992) Kaiserslautern ; Saarbrücken : DFKI, 1992
pdf-Format:
Dokument 1.pdf (24.391 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Künstliche Intelligenz
Institut: DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
DDC-Sachgruppe: Informatik
Dokumentart: Report (Bericht)
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Bandnummer: 92-01
Sprache: Englisch
Erstellungsjahr: 1992
Publikationsdatum: 01.07.2011
Kurzfassung auf Englisch: 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.
Lizenz: Standard-Veröffentlichungsvertrag

Home | Impressum | Über SciDok | Policy | Kontakt | Datenschutzerklärung | English