−-match: An inference rule for incrementally elaborating set instantiations

In this paper we describe a new inference rule, called –-match, which is used for finding set instantiations within an automated reasoning program. We have implemented –-match within a theorem prover called & and have used the system to prove some non-trivial theorems in mathematics, including Cantor's theorem and the correctness of transfinite induction. While not complete, we believe that –-match is a generally useful inference rule for finding set instantiations. One of the major contributions of the –-match rule is the ability to instantiate a term as an incompletely specified set abstraction, and then subsequently elaborate the identity of this set by considering other subgoals in the proof. This elaboration happens as a consequence of the deduction rules of the prover, and requires no additional machinery in the prover.