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

[PVS-Help] statements about skolemization constants



Hi,

In PVS 3.1 I want to prove that NOT (FORALL (n:nat): f(n)) has no
solution, thus steering towards a counterexample.

After using (grind), PVS gives

 {-1} m!1 >= 0
 {-2} m!1 > 1
 |-------
 (false)

Is there a way to give a counterexample, thus to instantiate m!1 with a
number >=2 ?

Regards,
Rene
r.c.ladan@student.tue.nl
Infinite_Many_Primes: THEORY
BEGIN

non_prime_divides(m,n:nat) : bool =
  1<m AND m<n AND (EXISTS (k:nat): k*m = n)

prime(n:nat) : bool =
  (FORALL (m:nat): NOT non_prime_divides(m,n))

bigger_prime(n:nat) : bool = 
  (EXISTS (m:nat) : m>n AND prime(m))

% this has no prove, gives rise to a counter-example
main_statement : CONJECTURE
 NOT (FORALL (n:nat) : bigger_prime(n))

END Infinite_Many_Primes

PGP signature