Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Journal of Automated...arrow_drop_down
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
Journal of Automated Reasoning
Article . 1987 . Peer-reviewed
License: Springer TDM
Data sources: Crossref
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
zbMATH Open
Article
Data sources: zbMATH Open
versions View all 4 versions
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

Unification in Abelian semigroups

Unification in abelian semigroups
Authors: Herold, Alexander; Siekmann, Jörg H.;

Unification in Abelian semigroups

Abstract

As always when Professor J. Siekmann takes the floor, he has really something to say. His experience and results [Lect. Notes Comput. Sci. 170, 1-42 (1984; Zbl 0547.03011); Automation of reasoning: Classical papers on computational logic. Vol. 1: 1957-1966, Vol. 2: 1967-1970 (1983; Zbl 0567.03001, Zbl 0567.03002)] are strong arguments. The paper is a thorough investigation on associative-commutative (AC- )unification, a theoretical basis, bringing also improvements of the techniques and algorithms at each stage of the general AC-unification problem. We just point out some of the questions raised in the paper. The first section begins with a review of the contributions to the AC- unification problem solving: After first basic results in \textit{M. E. Stickel} [(*)\ J. Assoc. Comput. Mach. 28, 423-434 (1981; Zbl 0462.68075)], and \textit{M. Livesey} and the second author [(**)\ Unification of AC-terms (bags) and ACI-terms (sets), Internal Report, Univ. Essex (1975), and Technical Report 3-76, Univ. Karlsruhe (1976)], further results belong to G. Huet, J. M. Hullot, F. Fages, A. Fortenbacher, C. Kirchner, and others. The key moments in solving the problem were: (1) the (independent) essential observation in (*) and (**) of the relationship between the AC-unification problem and the solving of linear (homgeneous in (*) and inhomogeneous in (**)) diophantine equations, as well as of the fact (deriving from a previously known mathematical result) that the set of the most general unifiers is always finite for the AC-unification procedure; (2) the termination of the extended AC-unification procedure, solved by \textit{F. Fages} [Lect. Notes Comput. Sci. 170, 194-208 (1984; Zbl 0547.03012)] by using an induction argument on a complexity measure on AC-tems. A still open problem remains that of a minimality condition for the extended AC-unification algorithm. Section 2 presents the complete solution of the unification in abelian monoids, following the original ideas in (**). {\S} 2.5 is devoted to a detailed comparison of the authors' solution and that belonging to Stickel (*), emphasizing the advantages of the present approach but also the recent improvements of Stickel's approach. The present algorithm is stated in general terms both for AC-operators with or without unit. Section 3 presents the extension of the AC-unification algorithm to first order terms containing uninterpreted function symbols. The solutions are also different from those of Stickel's algorithm: while this makes a ``variable abstraction'', the authors' reduction is of the ``constant abstraction'' type, the subterms being replaced by ``special'' constants in the reduction process. The classical J. A. Robinson's unification algorithm is combined, after the reduction process, with diophantine equation procedures, ``merging'' the unifiers of the two processes. The correctness and completeness of the extended AC-unification are proved. F. Fages' complexity measure is slightly modified (constants not being alien subterms) to prove, by noetherian induction on this measure, the termination of the algorithm. All the notions and proofs are most clearly exposed and exemplified. The paper is, we think, a serious candidate to the future ``elections'' for an (eventually, but so much desired) forthcoming ``Classical papers on computational logic'' new volume.

Related Organizations
Keywords

ddc:004, associative-communicative theories, abelian monoids, complexity measure, 004, AC- unification, Mechanization of proofs and logical operations, Semigroups in automata theory, linguistics, etc., linear diophantine equations, Linear Diophantine equations, constant abstraction, Theorem proving (deduction, resolution, etc.)

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    29
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Top 10%
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Top 10%
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
29
Average
Top 10%
Top 10%
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!