Skip to main content
PRL Project

Instantiation of Existentially Quantified Variables in Inductive Specification Proofs

by Brigitte Pientka

In this talk 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 can 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 and give a demo of the proof.

This is joint work with Christoph Kreitz; a paper about this topic is going to be published in September at the Fourth International Conference of Artificial Intelligence and Symbolic Computation.