Instantiation of Existentially Quantified Variables in Inductive Specification Proofs.
Brigitte Pientka, Christoph Kreitz.
In J. Calmet & J. Plaza, eds., Fourth International Conference on Artificial Intelligence and Symbolic Computation (AISC'98), LNAI 1476, pp. 247-258, Springer Verlag, 1998.
Abstract
	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.

		Paper is available in postscript and pdf format
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:PientkaKreitz98a, author = "Brigitte Pientka and Christoph Kreitz", title = "Instantiation of existentially quantified variables in inductive specification proofs", booktitle = "4$^{th}$ International Conference on Artificial Intelligence and Symbolic Computation", year = "1998", editor = "J. Plaza and J. Calmet", volume = "1476", series = "Lecture Notes in Artificial Intelligence", pages = "247--258", publisher = "Springer Verlag" }