Rob, Ok so looks like I am looking to rewrite all my specifications again in ProofPower. A minor inconvenience but should not be a problem. I will just pop up my specs on one screen and bring up ProofPower's XPP up on the other screen in my Linux VM, and I should be able to rewrite them with no problems. The only thing I can't seem to find is the symbol library in XPP. I have found where I can insert the various Zed structures, no problem, but there is supposed to be an XPP keyboard that has these symbols, based on the pictures in the documentation. Is this available in the editor version of XPP or do I need to run the full version of XPP to have access to that?
Once I get these in the system though, I definitely need to get some proofs written for them. That is where I am having a fair bit of trouble with the examples and documentation at the moment. I have a solid grasp of Z, and from Rogers email and the documentation, I can just write the proofs mostly in Z, which would save me some time in having to learn HOL right now, though I think I will learn it anyways for the future, just at a slower pace. In any case, the proof writing is not the issue, it is the writing in the ProofPower environment I guess I am hung up on, along with a few other minor things. I will look over all the documentation again on the site Rob, and continuing to see if I can get the examples operational so I can apply what is shown there to my open specifications. Thanks, Jon On Mon, Aug 13, 2012 at 1:12 PM, Rob Arthan <r...@lemma-one.com> wrote: > > On 13 Aug 2012, at 12:05, Jon Lockhart wrote: > > > Gentlemen, > > > > I apologize I should of been more specific at the tasks that I was > trying to accomplish and in describing where I am at so far. > > > > It seems the first point of business though from what Rob is saying is > actually getting the specifications into the ProofPower environment, which > at this point sounds like it needs to be done by hand, but I will explain > it more closely Rob. That way you can tell me if I got a shot of importing > them or if I am going to have to do a hand rewrite. > > > > So as you mentioned Rob, I am using Anthony's Z Word Tools for Word and > I have written all my specifications in there so far. It is a fabulous > writing tool, interfacing so well with Word, and providing all the > structure I need to write the specifications I am working on. Now, I am not > sure if you are aware of this, but the latest version of the Z Word Tools > no longer requires an export of the specification to be used with FUZZ or > CZT, those checkers are built right into the tool now and allow for > typechecking of the specification as you are writing it, using either > checker > > I think you will find that Z Word Tools is actually extracting the Z into > a file and running Fuzz or CZT for you, so it feels like the typechecker is > built in. You will find that the menu you use to do the typechecking has an > item on it to export the Z as a file. > > > Now of course, neither of these checkers run on .doc / .docx format > files, and there are a whole host of other files generated when you save or > run a check, including a LaTeX file of the specification. I was wondering > if you thought this LaTeX file would be possible to import into the > ProofPower system, or does it have to be in a special format of .tex to be > of any use? > > I actually thought that the CZT unicode format might be a bit closer to > what my prototype tools for dealing with UTF-8 can cope with. If you only > have a few pages of Z to start with, then it will probably be quicker just > to reenter it manually. If you have more it may be worth trying to cobble > together something semi-automated. We should be able to do something much > slicker in the slightly longer term. > > > > > I have attached one of the specifications I was originally using to > learn Z Word Tools, and it has passed all the typecheckers. This is the > LaTeX file that is generated for the specification. > > > > Thanks. This reminds me that one of the bigger problems is that > ProofPower has different rules for newlines than Spivey and the Standard Z. > Specifically, ProofPower requires semicolons at the end of declarations and > to separate "stacked" predicates in the predicate parts of schemas. > > Regards, > > Rob. > >
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
