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

*To*: pvs-help@csl.sri.com*Subject*: Moving existential quantifiers out over universal quantifiers*From*: Paul Loewenstein <pnl@heavengate.eng.sun.com>*Date*: Thu, 30 Sep 1999 15:07:08 -0700 (PDT)

I have proofs that have antecedent formulas of the form: FORALL (x: a): EXISTS (y: b): Formula (x, y) which I need to convert to the form: EXISTS (z: [a -> b]): FORALL (x: a): Formula (x, z (x)) so I can skolemize z without instantiating x. I currently do this rather tediously by hand specialization of the lemma: FORALL (P: [a -> [b -> boolean]]): (FORALL (x:a): EXISTS (y:b): P (x) (y)) IMPLIES (EXISTS (z:[a -> b]): FORALL (x:a): P (x) (z (x))) which, somewhat to my surprise, turned out to be provable without restricting a or b to be non-empty. This approach leads to tedious, unmaintainable, proofs. I can see the way forward in writing my first PVS strategy, but before I embark on this endeavor, I was wondering whether anyone else has met and solved the same problem, or whether I'm missing something obvious. I also need to apply eagerly the much simpler operation corresponding to the theorem: FORALL (P, Q: [a -> boolean]): (FORALL (x:a): P (a) AND Q (a)) IMPLIES (FORALL (x:a): P (a)) AND (FORALL (x:a): Q (a)) which would be my zeroth strategy to write. I can't help feeling that I may be missing something obvious. -- Paul Loewenstein Sun Microsystems Inc., Mailstop UMPK12-302 Staff Engineer 901 San Antonio Road, Palo Alto, California 94303 Tel: 650-786-6015 FAX: 650-568-9603 paul.loewenstein@eng.sun.com

- Prev by Date:
**Re: union variable binding operator** - Next by Date:
**Re: Moving existential quantifiers out over universal quantifiers** - Prev by thread:
**another TCC question** - Next by thread:
**Re: Moving existential quantifiers out over universal quantifiers** - Index(es):