When searching for proofs of theorems which contain definitions, it is a significant problem to decide which instances of the definitions to instantiate. We describe a method called dual instantiation, which is a partial solutionto the problem in the context of the connection methd; the same solution may also be adaptable to other search procedures. Dual instantiation has been implemented in TPS, a theorem prover for classical type theory, and we provide some examples of theorems that have been proven using this method. Dual instantiation has the desirable properties that the search for a proof cannot possibly fail due to insufficient instantiation of definitions, and that the natural deduction proof which results from a successful search will contain no unnecessary instantiations of definitions. Furthermore, the time taken by a proof search using dual instantiation is in general comparable to the time taken by a search in which exactly the required instances of each definition have been instantiated. We also describe how this technique can be applied to the problem of instantiating set variables.
展开▼
