Re: [PVS-Help] How can I fix this?

[Lee Pike <leepike@gmail.com>]

Nguyen,

> I wrote a PVS theory as below:
>
> test:  THEORY
> BEGIN
> x: VAR real
> test: LEMMA(FORALL x: x = ((7-sqrt(37))/6) OR x = ((7+sqrt(37))/6)
> IMPLIES x>=0)
> END test
>
> When I run it, PVS displays the error
>
> "Expecting an expression
> No resolution for sqrt with arguments of possible types:
>  37 :  reals.real"
>
> 1) I do not understand the error content. Please explain it for me.

PVS is expecting sqrt to be a defined function taking as an argument  
a real number.  You have not defined sqrt in your theory.

> 2) How can I fix it?

Define it, or better yet, download NASA Langley's PVS libraries in  
which sqrt is defined and many relevant properties are proved:  
<http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html>.   
In particular, you'll want the reals library.

Regards,
Lee