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

? about "complete"/"incomplete" proof status



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