KnowledgeBase » SEMINAR » ID = 460

Instantiation of Existentially Quantified Variables in Inductive Specification Proofs

by Brigitte Pientka
1997-1998

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.