[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.
  M-x show-tccs

Rick Butler