On handling distinct objects in the superposition calculus

Many domains of reasoning include a set of distinct objects. For general-purpose automated theorem provers, this property has to be specified explicitly, by including distinctness axioms. Since their number grows quadratically with the number of distinct objects, this results in large and clumsy specifications, that may affect performance adversely. We show that object distinctness can be handled directly by a modified superposition-based inference system, including additional inference rules. The new calculus is shown to be sound and complete. A preliminary implementation shows promising results in the theory of arrays.