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

Re: really basic question




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