Theory Unification in Abstract Clause Graphs

Abstract

Clause Graphs, as they were defined in the 1970s, are graphs representing first order formulas in conjunctive normal form together with the resolution possibilities. The nodes are labelled with literals and the edges (links) connect complementary unifiable literals. This report describes a generalization of this concept, called abstract clause graphs. The nodes of abstract clause graphs are still labelled with literals, the links however connect literals that are "unifiable" relative to a given relation between literals. This relation is not explicitely defined; only certain "abstract" properties are required. for instance the existence of a special purpose unification algorithm is assumed which computes substitutions, the application of which makes the relation hold for two literals. When instances of already existing literals are added to the graph (e.g. due to resolution or factoring), the links to the new literals are derived from the links of their ancestors. An inheritance mechanism for such links is presented which operates only on the attached substitutions and does not have to unify the literals. This solves a long standing open problem of connection graph calculi: how to inherit links (with several unifiers attached) such that no unifier has to be computed more than once.