A.A.

I’ve written a small tutorial for installation of HOLZ with Zeta. Read it here if you have trouble installing HOLZ.

Secondly, I’ve finished the 7th session. From Mr. MM.: You said you’ve been working with Z. I need to know how you actually work with Z. I’m talking about tools used. Do you do it using pen/paper or do you use a tool? I’m asking because here’s how HOLZ works:

The actual Z notation is written using Latex! (I knew my efforts with Latex wouldn’t go in vain.) The latex source is converted to PDF by Zeta. (Or to HOLZ if you install the adapter.) This HOLZ file can then be loaded into Isabelle/HOLZ and theorem proving can be done there. So, if you know how to encode Z notation in latex, you get a head start. If you know latex, that shouldn’t be much trouble. Otherwise, some work will need to be done on that front too.

This is one question I’d like an answer to before the next meeting.