User:Nicolas/Collections/ADVANCE D3.4 Improvement of automated proof: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Nicolas
mNo edit summary
imported>Nicolas
Line 10: Line 10:


The user manual of the ''SMT Solvers'' plug-in is available on the Event-B wiki<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref>.
The user manual of the ''SMT Solvers'' plug-in is available on the Event-B wiki<ref>http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in</ref>.
The introduction of variations in the HYP, HYP_OR, CNTR and GenMP reasoners is described in the Event-B wiki <ref>http://wiki.event-b.org/index.php/Variations_in_HYP,_CNTR_and_GenMP</ref>.
The design of the ''Membership Goal'' reasoner<ref>http://wiki.event-b.org/index.php/Membership_in_Goal</ref> has been updated to reflect the use of a SAT solver.


== Conclusion ==
== Conclusion ==

Revision as of 14:29, 6 October 2014

Overview

TODO

Motivations / Decisions

TODO

Available Documentation

TODO Tactic profiles are described in the Rodin Handbook[1].

The user manual of the SMT Solvers plug-in is available on the Event-B wiki[2].

Conclusion

TODO

References

  1. ↑ http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic
  2. ↑ http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in
Retrieved from ‘https://wiki.event-b.org/index.php?title=User:Nicolas/Collections/ADVANCE_D3.4_Improvement_of_automated_proof&oldid=10880’