My name is Luiz Lemos Junior, I am a Master's student in Computer Science
at Federal University of Pelotas, working with Rodin platform for Event-B.
I have been looking for some material about the implemented tatics and
rules in Rodin's external provers (PP, newPP, ML, Atelier-B). I have found
the (Atelier B) interactive prover reference/user manuals and the paper
Click’n Prove Interactive Proofs Within Set Theory (among others), but I
would like to find anything about the proof procedure that was implemented
(tatics and rules that are applied). Please, could you indicate me some
references or material about that?
Thanks for information.
Luiz Lemos Jr.