[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: ? 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?
When you install a library at your local site, you need to issue a
M-x pri to the "top" theory, so that all of the library lemmas are
put into "proved" status..
> 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.
Check to see if there are some unproved TCCs in the theory. i.e.