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

*To*: Eric Klavins <klavins@cs.caltech.edu>*Subject*: Re: really basic question*From*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Mon, 21 Jan 2002 17:29:01 -0800*cc*: pvs-help@csl.sri.com*In-Reply-To*: Message from Eric Klavins <klavins@cs.caltech.edu> of "Mon, 21 Jan 2002 17:01:38 PST." <Pine.LNX.4.33.0201211657420.21101-100000@sveiks.cs.caltech.edu>*Sender*: pvs-help-owner@csl.sri.com

Eric: Since both quantifiers in the theorem are of existential strength, you need an witness for instantiating them. If you do M-x ppe on the theory simple, you'll see that the UNIVERSE : TYPE+ declaration generates an axiom UNIVERSE_nonempty: AXIOM EXISTS (x: UNIVERSE): TRUE; You can then prove simple by (LEMMA "UNIVERSE_nonempty") followed by (skosimp*). At this point, the formula corresponding to the lemma disappears, but the skolem constant is still around. The extant skolem constants can be viewed by M-x show-skolem-constants. Instantiating one of the remaining quantifiers with x!1 using, say, (inst - "x!1") followed by (grind) finishes the proof. The automation for finding quantifier instantiations fares badly here because the skolem constant does not actually appear in any sequent formula. While it makes sense to explore the skolem constants for potential instantiations in this case, this isn't such a good idea in general. When there are quantifiers over numeric types, as there often are, the resulting instantiations will be mostly useless. -Shankar > From: Eric Klavins <klavins@cs.caltech.edu> > Subject: really basic question > Date: Mon, 21 Jan 2002 17:01:38 -0800 (PST) > To: <pvs-help@csl.sri.com> > > Hi, > > I'm trying to prove the theorem "simple" below, but can't get it to go > through. Am I missing something about what this theorem means in PVS? > > simple: THEORY > > BEGIN > > UNIVERSE : TYPE+ > PRED : TYPE = [ UNIVERSE -> bool ] > > Q : VAR PRED > x: VAR UNIVERSE > > simple: THEOREM > ( ( FORALL x : Q(x) ) => ( EXISTS x : Q(x) ) ) > > END simple > > > Thanks! > > -eric > > > o---- > | Eric Klavins > | Postdoctoral Scholar > Caltech Computer Science > klavins@cs.caltech.edu > (626)395-4858

**References**:**really basic question***From:*Eric Klavins <klavins@cs.caltech.edu>

- Prev by Date:
**really basic question** - Next by Date:
**Generalizations** - Prev by thread:
**really basic question** - Next by thread:
**Latex printing. a problem.** - Index(es):