Difference between revisions of "D45 Prover Enhancement"

From Event-B
Jump to navigationJump to search
imported>Tommy
imported>Tommy
Line 6: Line 6:
 
= Motivations =
 
= Motivations =
 
== New rewriting and inference rules ==
 
== New rewriting and inference rules ==
In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs), thus improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does increase directly the number of automatically discharged POs aims to help the user to interactively discharge them. Indeed, some proof steps are made easier from the use of specific rules thus making the user spare his time.
+
In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs), thus improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them. Indeed, some proof steps are made easier from the use of specific rules thus making the user spare his time.
  
 
== Advanced Preferences for Auto-tactics ==
 
== Advanced Preferences for Auto-tactics ==

Revision as of 14:29, 23 November 2011

Overview

Two tasks concerned the prover performance from the core platform: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parameterization or combination of tactics. While the addition of rewriting and inference rules has always been a regular task to enhance the Rodin integrated prover during DEPLOY lifetime, a new way to manage tactics has been implemented. In fact, since Rodin 2.1, the user is able to define various types of tactic strategies called 'profiles' which could allow him to adapt the order of the basic tactics an discharge some particular proof obligations accordingly. Moreover, since Rodin 2.3, the user is able to combine and parameterize these profiles increasing even more the potential of such proving feature.

  • TODO An overview of the contribution about the ProB Disprover (Daniel Plagge, Jens Bendiposto)
  • TODO An overview of the contribution about the SMT Solver Integration (Laurent Voisin)

Motivations

New rewriting and inference rules

In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs), thus improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them. Indeed, some proof steps are made easier from the use of specific rules thus making the user spare his time.

Advanced Preferences for Auto-tactics

TODO To be completed by Nicolas Beauger

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

TODO Laurent Voisin

Choices / Decisions

New rewriting and inference rules

TODO To be completed by Laurent Voisin

Advanced Preferences for Auto-tactics

TODO To be completed by Nicolas Beauger

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

TODO Laurent Voisin

Available Documentation

  • TODO Links for New rewriting and inference rules
  • TODO Links for Advanced Preferences for Auto-tactics
  • TODO Links for Isabelle Plug-in
  • TODO Links for ProB Disprover
  • TODO Links for SMT Solver Integration

Status

New rewriting and inference rules

TODO To be completed by Laurent Voisin

Advanced Preferences for Auto-tactics

TODO To be completed by Nicolas Beauger

Isabelle Plug-in

TODO To be completed by Matthias Schmaltz

ProB Disprover

TODO Daniel Plagge, Jens Bendiposto

SMT Solver Integration

TODO Laurent Voisin