Skip to main content
PRL Project

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)

  • unofficial copies PDF, PS

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

cite link