Instantiation of Existentially Quantified Variables in Inductive Specification Proofs
by Brigitte Pientka, Christoph Kreitz
Proceedings of Fourth International Conference on Artificial Intelligence and Symbolic Computation (AISC'98)
We present an automatic approach for instantiating existentially quantified variables in inductive specifications proofs. Our approach uses first-order meta-variables in place of existentially quantified variables and combines logical proof search with rippling techniques. We avoid the non-termination problems which usually occur in the presence of existentially quantified variables. Moreover, we are able to synthesize conditional substitutions for the meta-variables. We illustrate our approach by discussing the specification of the integer square root.
bibTex ref: PK98