Theta-Subsumption for Structural Matching

Abstract

Structural matching, originally introduced by Steven Vere, implements and formalizes the notion of a “most specific generalisation” of two productions, possibly in the presence of a background theory. Despite various studies in the mid-seventies and early eighties, several problems remained. These include the use of background knowledge, the nonuniqueness of most specific generalisations, and handling in-equalities. We show how Gordon Plotkin's notions of “least general generalisation” and “relative least general generalisation” defined on clauses can be adapted for use in structural matching such that the remaining problems disappear. Defining clauses as universally quantified disjunctions of literals and productions as existentially quantified conjunctions of literals, it is shown that the lattice on clauses imposed by θ-subsumption is order-isomorphic to the lattice on productions needed for structural matching.