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

*To*: pvs_help list_serve <pvs-help@csl.sri.com>*Subject*: ? about "complete"/"incomplete" proof status*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Wed, 15 Jul 1998 14:43:36 -0400 (EDT)

I proved a bunch of simple claims about finite sets in a theory of mine that imports the theories for finite sets provided by Jamsek, Butler, Owre & Holloway. The proofs of these claims relied on several lemmas in those theories. Then I tried M_x status-proof-theory to see if my claims showed up as proved. In the proof-summary table that came up, the claims were all listed as "proved - incomplete". Why is this? Also, another claim I'd proved in a different pvs file was listed as "proved - incomplete" and it relied on no additional assumptions; the proof was done simply by calls to skolem!, flatten and propax. My question is: What's the complete/incomplete distinction? "Incomplete" sure doesn't look good when it's displayed. Can you suggest any reference document where I can find a discussion of the proof-summary table? I've seen the discussion of Proof Status in "User Guide for the PVS Spec..." and it touches on this matter but doesn't say enough to answer the above question. Thanks in advance for any help. Mark Aronszajn

- Prev by Date:
**Re: ? about "complete"/"incomplete" proof status** - Next by Date:
**Re: ? about "complete"/"incomplete" proof status** - Prev by thread:
**Re: ? about "complete"/"incomplete" proof status** - Next by thread:
**Re: ? about "complete"/"incomplete" proof status** - Index(es):