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