D45 Prover Enhancement

From Event-B
Revision as of 13:14, 7 November 2011 by imported>Tommy (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...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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