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

Re: A property I cannot prove in PVS


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

Lemma 4.1.2 of Shaz and Shankar's "procomet" paper is a version of
the pigeonhole principle.  The paper sketches their proof.