Difference between pages "D45 Prover Enhancement" and "File:RodinWorkshop2021 OntoEventB.pdf"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
 
Line 1: Line 1:
= 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 tactics, even if it sometimes does increase the number of automatically discharged POs helps the user to interactively discharge them and make him spare time by making proofs easier.
 
 
== 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''
 
 
[[Category:D45 Deliverable]]
 

Latest revision as of 12:35, 14 June 2021