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

*To*: pvs-help@csl.sri.com*Subject*: A property I cannot prove in PVS*From*: "Paul S. Miner" <p.s.miner@larc.nasa.gov>*Date*: Mon, 15 Nov 1999 10:05:36 -0500 (EST)*Cc*: pvs-help@csl.sri.com*Delivery-Date*: Mon Nov 15 07:05:20 1999*In-Reply-To*: <199911151032.MAA15225@summer.wisdom.weizmann.ac.il>*References*: <199911151032.MAA15225@summer.wisdom.weizmann.ac.il>

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/

**References**:**A property I cannot prove in PVS***From:*Tamarah Arons <tamarah@wisdom.weizmann.ac.il>

- Prev by Date:
**Re: A property I cannot prove in PVS** - Next by Date:
**Re: Question on new decision procedures** - Prev by thread:
**Re: A property I cannot prove in PVS** - Next by thread:
**re: a question about a missing TCC** - Index(es):