[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] (grind :theories real_props) enters infinite loop
The problem seems to be related to the following example:
A : theory
test: lemma forall (x:real): 4 = 2 * some(4 ,2) => 4 = x
Here (grind) would try to use the assumption indefinitely
which results in non terminating loop. In my situation
there are rewriting rules in the imported theories which
replaces some(4,2) by 2. The question is why in one
case these rewrites are used before the assumption
and in the other not?
On 6/18/12 4:58 PM, Viorel Preoteasa wrote:
I have the following theories:
((power(1 / (square_root(2)), 4)) = (1 / 4)
((power(1, 4)) / (power(square_root(2), 4))) = (1 / 4))
ctx_exponents defines power and square_root and provides many
rewriting rules for them. The definitions of power and square_root
are based on the Nasa PVS library.
The command (grind :theories real_props) proves the lemma
However if in contextname4__example I import contextname4
instead of ctx__exponents, then the same proof command
enters an infinite loop.
The theories on which this is based are quite large, but I
can provide them if needed to reproduce the problem.
Any help would be much appreciated.