Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-24991
Titel: Unification in monoidal theories is solving linear equations over semirings
Verfasser: Nutt, Werner
Sprache: Englisch
Erscheinungsjahr: 1992
Quelle: Kaiserslautern ; Saarbrücken : DFKI, 1992
SWD-Schlagwörter: Künstliche Intelligenz
DDC-Sachgruppe: 004 Informatik
Dokumentart : Report (Bericht)
Kurzfassung: 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 zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-37964
hdl:20.500.11880/25047
http://dx.doi.org/10.22028/D291-24991
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Band: 92-01
SciDok-Publikation: 1-Jul-2011
Fakultät: Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Fakultät / Institution:SE - Sonstige Einrichtungen

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
RR_92_01.pdf24,39 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.