[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] How can I fix this?
> I wrote a PVS theory as below:
> test: THEORY
> 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:
In particular, you'll want the reals library.