D45 Prover Enhancement
From Event-B
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 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
