Difference between revisions of "D45 Prover Enhancement"
imported>Tommy m (New page: = Overview = Concerning Rodin's General Platform Maintenance the following contributions have been made: * {{TODO}} An overview of the contribution about the new rewriting and inference ru...) |
imported>Tommy m |
||
| Line 1: | Line 1: | ||
= Overview = | = Overview = | ||
| − | Concerning | + | Concerning the prover performance, two tasks were performed: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parameterization or combination of tactics. |
* {{TODO}} An overview of the contribution about the new rewriting and inference rules (Laurent Voisin) | * {{TODO}} An overview of the contribution about the new rewriting and inference rules (Laurent Voisin) | ||
* {{TODO}} An overview of the contribution about advanced Preferences for auto-tactics (Nicolas Beauger) | * {{TODO}} An overview of the contribution about advanced Preferences for auto-tactics (Nicolas Beauger) | ||
Revision as of 17:22, 18 November 2011
Overview
Concerning the prover performance, two tasks were performed: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parameterization or combination of tactics.
- TODO An overview of the contribution about the new rewriting and inference rules (Laurent Voisin)
- TODO An overview of the contribution about advanced Preferences for auto-tactics (Nicolas Beauger)
- 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
