Replacement rules with definition detection

The way in which a theorem prover handles definitions can have a significan t effect on its performance. Many first-order clause form theorem provers p erform badly on theorems such as those from set theory that are proven larg ely by expanding definitions. The technique of using replacement rules perm its automatic proofs of such theorems to be found quickly in many cases. We present a refinement of the replacement rule method which increases its ef fectiveness. This refinement consists in recognizing which clauses are obta ined from first-order definitions.