D45 Prover Enhancement: Difference between revisions
imported>Tommy |
imported>Tommy |
||
| Line 1: | Line 1: | ||
= Overview = | = Overview = | ||
Two tasks concerned the prover performance from 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. | 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 ProB Disprover (Daniel Plagge, Jens Bendiposto) | ||
* {{TODO}} An overview of the contribution about the SMT Solver Integration (Laurent Voisin) | * {{TODO}} An overview of the contribution about the SMT Solver Integration (Laurent Voisin) | ||
Revision as of 17:40, 18 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
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
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
