PRL Seminars

In this talk we discuss a uniform approach for instantiating universally and existentially quantified variables within an inductive proof. In order to compute valid instantiations we use rippling techniques.

Our method contributes three main extensions to the existing rippling technique:

1. an efficient way to deal with existential quantifier s
2. a more powerful approach for universal quantifiers
3. the synthesis of case splits during a proof.