D45 Prover Enhancement
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
