Instantiation of Existentially Quantified Variables in Inductive Specification Proofs

unofficial copies [PDF], [PS]

by Brigitte Pientka and Christoph Kreitz

Proceedings of Fourth International Conference on Artificial Intelligence and Symbolic Computation (AISC'98), J. Calmet and J. Plaza (eds.), LNAI 1476, pp. 247-258, Springer-Verlag, 1998.


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.