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

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



Hello,

The problem seems to be related to the following example:

A : theory
begin
  some(x,y:real):real
  test: lemma forall (x:real): 4 = 2 * some(4 ,2) => 4 = x
end A

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?

Best regards,

Viorel Preoteasa

On 6/18/12 4:58 PM, Viorel Preoteasa wrote:
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