[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Rewrites under quantifiers



In one of my strategies, I am using rewrite rules to put a formula
into a normalized form.  However, I am running into the problem that
the rewrite rules do not work under a quantifier.  I was able to
partially solve the problem by using (skolem!), applying my rewrites,
and generalizing the skolem constants, however this does not work when
my quantifier is not the outermost operator or when it is an
existential.  

How can I generally do rewrites when the formula to rewrite may be
under a quantifier?  

Thank you,

    Erika