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