Axiom Lists and Conjectures.

   In proving a theorem, Specware assembles a list of the axioms  for the specification in question. These axioms define the theory corresponding to the specification. The list includes the following axioms:

• The axioms explicitly mentioned in the specification.
• Previously proved theorems mentioned in the specification.
• The implicit axioms corresponding to the sorts of the specification (e.g., the axioms that define the relax operator for each of the specification's subsorts). 
• If the specification is a colimit, the axioms for the component specifications. 
• If the specification is a translation, the translation of the axioms of the original specification.  
• If the specification imports another, the axioms of the imported specification. 

The induction  axiom is not included explicitly in the list; however, if the specification includes a constructor set , a special tactic will enable the theorem to be proved by induction.

As we have remarked, Specware will attempt to prove any theorem presented explicitly within a specification . It will also attempt to prove the images under a morphism  of any axioms of the source specification. The Specware theorem prover will regard each formula it attempts to prove as a conjecture  until it has been proved. Once a conjecture is proved, it is regarded as a theorem.

Restriction: At the present time, for technical reasons, the conjecture must be expressed in prenex  normal form--quantifiers must be at the top level. It may also be a conjunction of formulas in prenex normal form.

Let us illustrate this with some examples. Later () we can use some of these to illustrate the guidance of the theorem prover.

• Example: Collection
• Example: Sack
• Bag into Sequence