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

[PVS-Help] (grind :theories real_props) enters infinite loop



Hello,

I have the following theories:

contextname4: theory
begin
    importing ctx__exponents;
end contextname4

contextname4__example: theory
begin
  %importing contextname4;
  importing ctx__exponents;

  example: LEMMA
    ((power(1 / (square_root(2)), 4)) = (1 / 4)
<=>
    ((power(1, 4)) / (power(square_root(2), 4))) = (1 / 4))

end contextname4__example

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
example above.

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.

Best regards,

Viorel Preoteasa