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

Re: quantifier library

Dear Kong Woei Susanto,

I will let some of the other more knowledgable people on pvs-help to
give you information about whether there exists any library or
built-in help for quantifier manipulation in the current version of
PVS.  Since, you say you are working in hardware verification I wanted
to bring to your attention a couple of rewrite rules that I use to
"move quantifiers around" to automate RT-level proofs of hardware
designs specified in the "HOL-style" popularized by Mike Gordon.  Even
if these rules are not adequate for your purpose, they may give you
some idea about how higher-order matching can be used in PVS to
maniuplate formulas with quantifiers.  If you want details about the
rules I use, please let me know and I will send you the details.

- Srivas