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

Reply via email to