What Is Essential Unification?

Peter Szabo, Jorg Siekmann and Michael Hoche

Abstract A unifier of two terms s and t is a substitution a such that sa = tо. For flrst-order terms there exists a most general unifier a in the sense that any other unifier т can be composed from a with some substitution X such that т = о о X. For many practical applications it turned out to be useful to generalize this notion to E -unification, where E is an equational theory, =E is equality under E and a is an E-unifier if so =Eta. Depending on the equational theory E, the set of most general unifiers is always a singleton (as above) or it may have more than one unifier, either finitely or infinitely many unifiers and for some theories it may not even exist, in which case we call the theory of type nullary. The set of most general unifiers is denoted as x-U ?E (Г) for a unification problem Г, which is a system of equations and an equational theory E. Unfortunately the set xU ?E (Г) may be very large in general—even if it is finite—and for all practical purposes not really useful. For this and other reasons there is hence (i) a strong interest to compute a much smaller generating set of minimal unifiers and then (ii) to find efficient engineering solutions to handle these sets. Essential unifiers, as introduced by Hoche and Szabo, generalize the notion of a most general unifier and they have a dramatically pleasant effect: the set of essential unifiers is often much smaller than the set of most general unifiers. Essential unification may even reduce an infinitary theory to an essentially finitary theory. For example the one variable string unification problem is essentially finitary whereas it is infinitary in the usual sense. The most drastic reduction known so far is obtained for idempotent semigroups, or bands as they are called in computer science, which are of type nullary: there exist two unifiable terms s and t, but the set of most general unifiers does not exist. This is in stark contrast to essential

P. Szabo (B)

Kurt-Schumacher-Str. 13, 75180 Pforzheim, Germany e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

J. Siekmann

Saarland University/DFKI, Stuhlsatzenhausweg, 66123 Saarbrucken, Germany e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

M. Hoche

Airbus Defense and Space, Claude-Dornier-Str., 88090 Immenstaad, Germany e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

© Springer International Publishing Switzerland 2016 285

E.G. Omodeo and A. Policriti (eds.), Martin Davis on Computability,

Computational Logic, and Mathematical Foundations,

Outstanding Contributions to Logic 10, DOI 10.1007/978-3-319-41842-1_11

unification: the set of essential unifiers for bands always exists and is finite. The key idea for essential unification is to base the notion of generality not on the standard subsumption order for terms with the associated subsumption order for substitutions, but on the encompassment order for terms and substitutions. Hence we propose the encompassment order as a more natural order relation for minimal and complete sets of E-unifiers and call these sets essential unifiers, denoted as eU ?E (Г). This paper introduces essential unification, provides a definitional framework based on order relations and surveys what is presently known. We conclude with a list of some of the more important open problems, including the main open problem, namely how to build essential unification into an automated reasoning system.

Keywords E-Unification • Order relations for unification • Most general unifiers • Essential unifiers • Unification theory

< Prev   CONTENTS   Source   Next >