Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-40148
Titel: Unification in a Combination of Arbitrary Disjoint Equational Theories
VerfasserIn: Schmidt-Schauß, Manfred
Sprache: Englisch
Erscheinungsjahr: 1987
Erscheinungsort: Kaiserslautern
Freie Schlagwörter: Unification
Equational theories
Decidability of Unification
Combination of equational theories
Boolean rings
Abelian groups
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: The unification problem of terms in a disjoint combination E1 + ... + En of arbitrary theories is reduced to a combination of pure unification problems in Ej, where free constants may occur in terms, and to constant elimination problems like: find all substitutions σ such that ci is not a constant in the term σti, i = 1,...,n, where ti are terms in the theory Ej. The algorithm consists of the following basic steps: First of all the terms to be unified are transformed via variable abstraction into terms belonging to one particular theory. Terms belonging to the same theory can now be unified with the algorithm for this theory. For terms in some multi-equation belonging to different theories it is sufficient to select some theory and collapse all terms not belonging to this particular theory into a common constant. Finally constant elimination must be applied in order to solve cyclic unification problems like 〈x=f(x)〉. The algorithm shows that a combination of finitary unifying regular theories, of Boolean rings, of Abelian groups or of theories of Hullot-type is of unification-type finitary, since these theories have finitary constant-elimination problems. As a special case, unification in a combination of a free Boolean ring with free function symbols is decidable and finitary; the same holds for Abelian groups. Remarkably, it can be shown that unification problems can be solved in the general case E1+... +En if for every i there is a method to solve unification problems in a combination of Ei with free function symbols. Thus, unification in a combination with free function symbols is the really hard case. This paper presents solutions to the important open questions of combining unification algorithms in a disjoint combination of theories. As a special case it provides a solution to the unification of general terms (i.e. terms, where free function symbols are permitted) in Abelian groups and Boolean rings. It extends the known results on unification in a combination of regular and collapse-free theories in two aspects: Arbitrary theories are admissable and we can use complete unification procedures (including universal unification procedures such as narrowing) that may produce an infinite complete set of unifiers for a special theory.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-401484
hdl:20.500.11880/36225
http://dx.doi.org/10.22028/D291-40148
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 87,16
Datum des Eintrags: 11-Aug-2023
Fakultät: SE - Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professur: SE - Sonstige
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.