The Stanford Formal Reasoning Group, under the High Performance
Knowledge Base project, is developing a new method of integrating
large knowledges bases.  Knowledge bases, developed independently, can
be correctly combined by writing lifting axioms that describe the
relationship between the two repositories.  Knoweldge bases, orders of
magnitude larger than previously created can be managed by combining
smaller knowledge sources.  This allows queries that depend on
information from more than one source to be answered by a single
interface, removing the previous need for human intervention.