Synthesis of induction orderings for existence proofs

Abstract

In the field of program synthesis inductive existence proofs are used to compute algorithmic definitions for the skolem functions under consideration. While in general the recursion orderings of the given function definitions form the induction ordering this approach often fail for existence proofs. In many cases a completely new induction ordering has to be invented to prove an existence formula. In this paper we describe a top-down approach for computing appropriate induction orderings for existence formulas. We will use constraints from the knowledge of guiding inductive proofs to select proper induction variables and to compute a first outline of the proof. Based on this outline the induction ordering is finally refined and synthesized.