Mechanical Generation of Sorts in Clause Sets

Abstract

The algorithm SOGEN is described, which transforms a SIG-sorted clause set CS into a SIG'-sorted clause set CS', where the output clause set is smaller, but the sort structure is more sophisticated. This produced clause set is the input for our Theorem Prover. which has ΣRP* , an extension of ΣRP as its basic deductive calculus. Both calculi have resolution and paramodulation as their basic Operations. We prove that the transformation induced by SOGEN does not affect unsatisfiability, respectively satisfiability, of the clause set.