Resolution K-Transformations

Clause-K-transformations are faithful transformations between clause sets. When inferences are drawn on a clause set using resolution as inference rule, some clauses may be involved in particularly many resolution steps. Typically such a clause would express a very general property like the symmetry or transitivity of a relation. Most of these resolution steps do not contribute to inferring the empty clause. Clause-K-transformations can be used to eliminate unnecessary resolution steps. A clause set is transformed by replacing a clause that is involved in particularly many resolution steps by em instances of this clause. The more specific these instances are, the more this transformation will reduce the number of possible resolution steps. The criteria for the faithfulness of such a transformation can be tested automatically. For clauses not containing function symbols, I have described a way to enumerate candidates for clause-K-transformations. With this I have found transformations for many clauses automatically. I have also investigated eliminations for clauses containing function symbols (e.g.~condensed detachment) and eliminations of several clauses at the same time.