[ProofPower] Some questions about ProofPower/Z

[Thiago Carvalho de Sousa]

Hi friends,

I have some questions related to ProofPower and Z :

1) I´d like to know if there is some .doc explaining
the encoding of Z in ProofPower-HOL. I´l like to
verify how deep is this enconding...

2) In the "ProofPower Description Manual", I can read
about an approximation to the Z language. I´d like to
know if there is a a .doc explaining explicity the
diference between the standard and the approximation.

3) I´ve not seen any explicity proof in the ProofPower
documentation about the initialisation theorem. I
think it could useful for newbies in ProofPower and Z.

4) In the Z style states-operations, can I have two
initial states or can an operation generate two or
more states? I mean I´d like to know if the Z style is
a deterministic automata or not..

Thanks in advance

=====
Thiago Carvalho de Sousa
Msc Student 
University of São Paulo


		
__________________________________
Do you Yahoo!?
New and Improved Yahoo! Mail - Send 10MB messages!
http://promotions.yahoo.com/new_mail