Next: Operational Semantics Up: Finite Domains and Exclusions Previous: Functions with Domain/Exclusion

Domain and Exclusion Anti-Unification

In section 5.1 we have defined the algorithm for `multiplying out' finite domains from clauses into an extensional form, and noted that the general reduction of finite exclusions would involve a strong form of negation.

Conversely, the automatic generation of intensional, domain/exclusion-using clauses from ordinary ones constitutes an interesting generalization task. In particular, a set of `similar' clauses can often be generalized by individually generating a finite domain in each distinguishing argument position, thus `compressing' the clauses' information. Generalizing more than one argument position at a time (giving rise to new combinations when multiplying out) amounts to `inducing' new information from the clauses.

For instance, inverting two transformations, the 24 relational(ized) separates facts

can be generalized (compressed) to the two facts

which are relationalized versions of the separates function in section 6.1.

A simple method for this (least general) generalization is pairwise domain anti-unification of the input facts. For ease of presentation we will assume that clauses are represented as structures, e.g. regarding an atom (fact) as a structure whose constructor stands for the predicate. Domain anti-unification of two structures works like classic anti-unification [11] (in our implementation, [5], (nested) structures having different constructors or arities yield a new variable) with the following modifications. For a (named or anonymous) variable and a domain it yields a variable in the manner classic anti-unification handles variable/constant pairings. For different constants it yields a dom term containing these constants, not a (sometimes overly general) new variable. (For a constant and a structure it has to yield a new variable since currrent dom terms cannot contain structures.) Generally (constants can be treated as singleton domains), domain anti-unification of two dom terms yields their union (unification: intersection). Identical dom (later: exc) terms can directly yield one copy unchanged, short-cutting spurious unions (later: intersections).

The complementary exclusion anti-unification for a (named or anonymous) variable and an exclusion yields a variable in the manner classic anti-unification handles variable/constant pairings. It yields the intersection (unification: union) of two exc terms. For an exclusion and a constant (singleton domain) it yields the exc term minus the constant. Generally, the domain-exclusion anti-unification of a dom and an exc term, in any order, yields the exc term with the elements of the dom term set-theoretically subtracted (unification: domain with exclusion subtracted). An empty-exclusion outcome, as usual, represents the always successful anonymous variable. Altogether, the domain/exclusion complementarity commutes nicely with the unification/anti-unification duality.

Let us start an example for domain anti-unification with, say, the first two input facts:

Anti-unification generalizes them via a domain in the second argument:

This intermediate result domain-anti-unified with the third input fact,

separates(pacific,usa,japan).          %  usa = dom[usa]
leads to the completely generalized pacific fact above. Similarly, the remaining input facts, via three groups of textually ordered domain-anti-unification steps, generalize their third argument to a common domain:

The completely generalized atlantic fact above is then obtained as for the pacific side. (Equivalently, the second argument could be generalized first.)

Suppose we have one additional input fact,

For group formation on the third argument, domain anti-unification would leave this fact as a singleton group since denmark is the only European partner specified for panama. Now, the four resulting groups differ in two arguments, not just in one. Still domain-anti-unifying them would generalize the second argument and `absorb' denmark into the domain of the third argument:

This generalized atlantic fact expresses more information than the input facts, namely an induction from Denmark to the other European countries (which happens to be empirically true); again multiplying out the result makes these induced facts explicit:

. . .
However, since (domain) anti-unification can find a generalization for each pair of structures, its use most be controlled. An example of overgeneralization would result from further domain-anti-unifying the completely generalized pacific and atlantic facts above, generating a single fact expressing much more than the 24 inputs via geographically vacuous Pacific/Atlantic and Japan/Europe domains.

An example for exclusion anti-unification can take two versions of a fact from section 5.1 as input:

likes(X,exc[mary,claire,linda]).  % Everybody likes all except MCL
likes(john,exc[mary,tina]).    % John likes all except Mary & Tina
Anti-unification generalizes them via an intersection of the exclusions in the second argument:

likes(X,exc[mary]).              % Everybody likes all except Mary
This is the least general generalization of the input facts since exactly the subexclusion common to both facts is kept. In cases where we have a closed universe, say of section 5.1, the inputs can be rewritten as complementary domain facts:

likes(X,dom[ann,john,peggy,susan,tina]).   %  (*)
Domain anti-unification via union generalizes them to

which is the complement of the exclusion-anti-unification result above.

Finally, domain-exclusion anti-unification of the input facts

likes(john,dom[mary,tina]).   %  (**)
via subtraction generalizes them to

Here, the exclusion is minimally weakened (its extension being minimally enlarged) to accomodate what is specified by the domain. This can again be illustrated for the case of a closed universe: anti-unify (*) with (**) and re-complement the result. Such least general generalizations by domain-exclusion anti-unification thus remove dom-exc contradictions in a set of clauses, e.g. about John's liking of Mary in the above input facts; similarly, exclusion anti-unification removes the less obvious exc-exc contradictions concerning constants that occur in only one of the exclusions, e.g. about John's liking of, say Claire, in the previous input facts. This may be exploited for `theory revision' [12] of knowledge bases containing exclusion terms.

Next: Operational Semantics Up: Finite Domains and Exclusions Previous: Functions with Domain/Exclusion

Harold Boley & Michael Sintek (