On Monday 13 Aug 2012 03:24, Jon Lockhart wrote: > I have already written the specifications in Word using Z > Word Tools, and they are already saved in a variety of > formats. I have them transferred over to my linux image. > What format do they need to be in for me to get to > import them into XPP so I can begin the proof > development.

ProofPower and Word don't really go together. ProofPower works with LaTeX documents using a special encoding for non-ascii characters. There are no automatic conversions available from Word to this format, though there is an alternative fully ascii source format using keywords instead of special characters. The place to look for full details of ProofPower documents and the facilities associated with them is usr001 "ProofPower - Document Preparation" which is part of the PPTex option when building ProofPower. The ProofPower documentation is in directory doc of the installation, see index.html in that directory. > My second question is once you get those specifications > into XPP and the ProofPower tools, then how do you start > writing the proofs on the Zed specs? Is it supposed to > be in Zed terminology or in HOL? Look at the ProofPower documentation page and you will find tutorials on proof in HOL and in Z. Proofs of Z theorems will ideally stick to Z and not stray into HOL, but it doesn't always work out that way. It is generally recommended to learn how to do proofs in HOL first and then move on to Z, and the tutorial materials for Z assume that the student already knows about proof in HOL, If you don't know LaTeX or HOL then there is a pretty steep learning curve ahead to get into a position to do Z proofs in ProofPower. It is possible to cut out the LaTeX, but without the LaTeX your ProofPower-Z source files would not be printable documents and you would be maintaining two parallel sets of documents, a printable set in Word and sources for ProofPower in a different set of documents. Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com