From: ACKERMANN J G <322...@my...> - 2014-11-17 20:27:26
|
Good evening, Laurent, Thank you very much for this information. Kindest regards Jaco ________________________________________ From: Laurent Voisin <lau...@sy...> Sent: 14 November 2014 12:33 To: ACKERMANN J G Cc: rod...@li... Subject: Re: [Rodin-b-sharp-user] Inference mechanisms Hi Jaco, > Le 13 nov. 2014 à 12:02, ACKERMANN J G <322...@my...> a écrit : > > I am very interested in improving my understanding of the various theorem provers that are available as plug-ins in Rodin. More specifically, I am trying to understand the various inference mechanisms implemented by the provers. > > [My interest stems from MSc level research into identifying heuristics that could facilitate automated proof discovery.] > > Information on any of the following provers would be great: > Mono-Lemma (ML) > The various Predicate Provers (PP or newPP) ML and PP are provers that have been developed by ClearSy for Atelier B. I am not aware of any public documentation on their internals. For newPP, the most accurate documentation is the master thesis of François Terrier at ETH. > CVC3 SMT2 > veriT SMT2 These are external SMT solvers. Their documentation is available from their respective web sites: http://www.cs.nyu.edu/acsys/cvc3/ http://www.verit-solver.org/ > Furthermore, whilst trying to prepare and write-up some results, is there a way to obtain (through plug-ins or otherwise): > 1. output representative of the search effort? > 2. (nicely formatted) final proof listings? Not that I know of. Cheers, Laurent. |