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

Re: [PVS-Help] begginer's question



Jane,

I suspect that the problem you are having is that the tutorial you are using
is based on a much older version of PVS.  The theory "decisions" as
presented in the tutorial declares x, y, and v to be of type number.  At
that time, the built in PVS type 'number' had all the properties that we
expect of real numbers, including the order axioms.  However, in the current
version of PVS, the order axioms are introduced for type 'real'.  They do
not apply for objects of type number.

If you change the declaration to:

  x, y, v: VAR real

Then the proof given in the tutorial should work.

Paul Miner


On 10/2/08 10:29 AM, "Cesar Munoz" <munoz@xxxxxxxxxx> wrote:

> You should try (grind) instead of (ground):
> 
> {-1}  x!1 < 2 * y!1
> {-2}  y!1 < 3 * v!1
>   |-------
> {1}   3 * x!1 < 18 * v!1
> 
> Rule? (grind)
> Trying repeated skolemization, instantiation, and if-lifting,
> Q.E.D.
> 
> Cesar
> 
> jane huffam wrote:
>> Hi,
>> I'm studying pvs through "A Tutorial Introduction to PVS" by  Crow, Owre,
>> Rushby, Shankar and Srivas.  They gave an example I can't prove. It is
>> "decisions", section 4.3. I'm stuck in arith. What do I do after "(then
>> (skolem!)(ground))" ?
>> Thanks for any tip!
>>