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

A property I cannot prove in PVS

Tamarah Arons writes:
 > I have a question on how to prove a certain property in PVS:
 > There is a set B of 2*N elements labeled 1 ... 2*N.
 > 1. Array A of N elements contains N distinct elements from B.
 > 2. List L can contain up to N elements. The elements in L are
 >    distinct and are different to those in A.
 > I.e. every element in B can either be in A, in L, or in neither but never
 > in both.
 > I have proved properties 1. and 2. in PVS. Now I need to prove
 > the obvious property that if there is an element b in B
 > such that b is not in A and not in L, then L contains less than N
 > elements. 
 > A and L are modified in time-steps in which a number of elements can 
 > change their statuses but always ensuring that 1. and 2. hold.
 > I have worked on this a long time and am reaching the desperate conclusion
 > that it is not provable in PVS, requiring reasoning which cannot be
 > expressed, such as the pigeon-hole principle. 

The pigeonhole principle can certainly be expressed (and proven) in
PVS.  One form of the pigeonhole principle is in the finite_sets
library distributed with PVS2.3.  You should be able to use it (with a 
little effort) to prove the property stated above.

-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/