Search results

From Event-B
Jump to navigationJump to search
  • # adding a new [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/reasoners.h # adding a new [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/proof_tacti ...
    3 KB (400 words) - 10:27, 27 October 2011
  • === Adding a reasoner === # Manual rewriters: Reasoners which apply a rewriting rule at a given position. ...
    17 KB (2,378 words) - 09:48, 17 June 2010
  • ...ings and additions to it, such as the addition of integrated reasoners and tactics, but also by the integration of some external reasoning ability such as ext ...proof obligations. The user can furthermore share and backup these defined tactics using the provided import/export mechanism.<br> ...
    4 KB (596 words) - 13:21, 18 July 2012
  • # Providing a reference manual. * The reference manual seems fairly complete, but is hard to navigate (mixture of PDFs, links and ...
    5 KB (720 words) - 11:28, 15 September 2011
  • ...necessary (but still possible) to create a new profile to use SMT solvers tactics (see [[#Selecting_an_SMT_Auto-Tactic_Profile|Selecting an SMT auto-tactic p ...ct it to the Rodin platform by adding it to the list of known solvers, and adding SMT configurations to be used by the SMT tactic.<br/> ...
    17 KB (2,538 words) - 15:41, 2 October 2017
  • ...atform, by adding new features to it, such as new integrated reasoners and tactics, but also by connecting some external reasoning ability such as external pr ...to-tactic configuration. Sometimes, the automatic prover fails because the tactics are applied in an unappropriate order. Since Rodin 3.0, plug-ins can contri ...
    7 KB (1,145 words) - 10:05, 8 October 2013
  • ...e profiles (e.g. ordered lists) of tactics to be used in post or automatic tactics at both workspace and/or project level. Exported projects contain the profi ...ic_tactics | the page on the work done about Preferences for the automatic tactics]] ...
    10 KB (1,277 words) - 13:45, 26 July 2011
  • ...tics. A tactic can be either automatic (auto tactic and/or post tactic) or manual (using providers in the UI that paint their applications in red on formulas ...uent prover provides a set of tactics applying proof rules (and even other tactics!). These rules are either rewriting rules (see [[All_Rewrite_Rules|rewritin ...
    13 KB (2,012 words) - 15:43, 21 September 2021
  • * automatically, when post-tactics are run. * automatically, when auto-tactics are run. ...
    27 KB (4,348 words) - 08:56, 26 September 2011
  • * automatically, when post-tactics are run. * automatically, when auto-tactics are run. ...
    27 KB (4,348 words) - 18:45, 28 September 2011
  • This page contains descriptions of the available proof tactics within the RODIN Platform. * '''[[The Proving Perspective (Rodin User Manual)#The Automatic Post-tactic|Post-tactic]]''': ''No'': the tactic cannot be a ...
    57 KB (6,150 words) - 17:25, 21 February 2012
  • : The user manual, user tutorial and other developer documentation on the wiki<ref>http://wik | WP1-4 partners|| Preferences for the automatic tactics <ref>http://sourceforge.net/tracker/index.php?func=detail&aid=1581775&group ...
    9 KB (1,423 words) - 16:28, 14 November 2011
  • ...a ''parameterization'' of a tactic (timeout, ...), or a ''combination'' of tactics and profiles (see [http://handbook.event-b.org/current/html/preferences.htm ...nction overridden by maplet'' (auto), EQL_LR applied at a single position (manual), ''Generalised Modus Ponens'' (auto) ...
    11 KB (1,401 words) - 09:39, 8 November 2011
  • Bug 3008554: Scroll bar does not refresh when adding hypotheses Bug 3027428: OnePointRule in post tactics makes proof save crash ...
    15 KB (2,008 words) - 15:34, 10 January 2011