Unification in commutative idempotent monoids (Q1111775)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Unification in commutative idempotent monoids |
scientific article |
Statements
Unification in commutative idempotent monoids (English)
0 references
1988
0 references
The paper is related to the algebraic theory of abstract data types and deals with the unification of the algorithms as to associativity, commutativity, and idempotence of the function unions from which the discussed algorithms are constructed. The investigation goes back to the unification in commutative semigroups (AC-unification) and in commutative idempotent semigroups (ACI-unification) [\textit{M. Liversey} and \textit{J. Siekmann}, Unification of sets and multisets, Tech. Rep., University of Karlsruhe, 1976]. ACI-unification is associated with the congruence relation on the totality of free terms. The problems of ACI-unification for free idempotent commutative monoids have been discussed by the second author [Lect. Notes Comput. Sci. 230, 470-488 (1986; Zbl 0643.68136)]. The main result of this paper is the construction of a minimal complete set of unifiers for idempotent commutative monoids. The ACI-unification correctness is established. In spite of finiteness of the complete set of unifiers, the power of the set is rather high and this determines mainly the theoretical value of the obtained results. The investigation is of interest for applications to automatic theorem proving, term-rewrite systems, logic and functional programming.
0 references
logic programming
0 references
algebraic theory of abstract data types
0 references
unification
0 references
commutative semigroups
0 references
ACI-unification
0 references
automatic theorem proving
0 references
term- rewrite systems
0 references
functional programming
0 references