Theorem proving is an essential part of any assurance Specware gives its users of the correctness of its final product. The system has been designed so that the theorems that need to be proved are within the capabilities of contemporary theorem-proving technology, and an effort has been made to have Specware's theorem proving be invisible to the user. Nevertheless, some proofs will require user guidance and some users will be knowledgeable enough to provide this guidance. This note does not constitute a basic introduction to theorem proving, but it will give enough details about the theorem-proving interface to enable the educated user to help the system find a proof. The note does assume familiarity with the Specware language.
Specware will attempt to prove theorems when parsing a specification or a specification morphism (or an interpretation ). In parsing a specification, it will attempt to prove that its alleged theorems do follow from the other axioms in the specification. In parsing a morphism, it will attempt to prove that the morphism maps the axioms of the source specification into theorems of the target specification. The user can postpone the proofs for subsequent verification, and exercise a good deal of control over the way in which proofs are done.