D45 Prover Enhancement: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Tommy
m New page: = 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 ru...
 
imported>Tommy
mNo edit summary
Line 1: Line 1:
= Overview =
= Overview =
Concerning Rodin's General Platform Maintenance the following contributions have been made:
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 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 advanced Preferences for auto-tactics (Nicolas Beauger)  

Revision as of 17:22, 18 November 2011

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