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

From Event-B
Jump to navigationJump to search
imported>Nicolas
(Created page with "== Overview == {{TODO}} == Motivations / Decisions == {{TODO}} == Available Documentation == Tactic profiles are described in the Rodin Handbook<ref>http://handbook.event-b....")
 
imported>Nicolas
m
Line 6: Line 6:
  
 
== Available Documentation ==
 
== Available Documentation ==
 +
{{TODO}}
 
Tactic profiles are described in the Rodin Handbook<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref>.
 
Tactic profiles are described in the Rodin Handbook<ref>http://handbook.event-b.org/current/html/preferences.html#ref_01_preferences_auto_post_tactic</ref>.
  
Line 15: Line 16:
  
 
== Conclusion ==
 
== Conclusion ==
 +
{{TODO}}
  
 
== References ==
 
== References ==

Revision as of 14:25, 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].

The introduction of variations in the HYP, HYP_OR, CNTR and GenMP reasoners is described in the Event-B wiki [3].

The design of the Membership Goal reasoner[4] has been updated to reflect the use of a SAT solver.

Conclusion

TODO

References