D45 Prover Enhancement: Difference between revisions
imported>Tommy mNo edit summary |
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. | |||
* {{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:25, 18 November 2011
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.
- 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
