imported>Tommy |
|
Line 1: |
Line 1: |
− | = 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''
| |
− |
| |
− | [[Category:D45 Deliverable]]
| |