# Difference between revisions of "Disprover"

imported>Jrloria |
imported>Jens |
||

Line 2: | Line 2: | ||

The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples | The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples | ||

− | for a given | + | or proofs for a given proof obligation. |

The Disprover is described in [http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Debugging Event-B Models using the ProB Disprover Plug-in], Ligot, Bendisposto, Leuschel. | The Disprover is described in [http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Debugging Event-B Models using the ProB Disprover Plug-in], Ligot, Bendisposto, Leuschel. | ||

Line 8: | Line 8: | ||

== Installation == | == Installation == | ||

− | The ProB Disprover is available through the ProB Update Site. | + | The ProB Disprover is currently only available through the ProB Nightly Build Update Site (http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/). |

− | |||

− | |||

− | |||

== How to use it, how it works == | == How to use it, how it works == | ||

− | The proof obligation editor in Rodin presents the user with a number of Hypotheses and one Goal, to be proved. If the Disprover is installed, it is available in the tool bar alongside the other provers. | + | [[Image:disprover-all.png]]: The proof obligation editor in Rodin presents the user with a number of Hypotheses and one Goal, to be proved. If the Disprover is installed, it is available in the tool bar alongside the other provers. |

− | Upon selecting the Disprover, it builds | + | Upon selecting the Disprover, it builds a formula from the Hypotheses and the negated Goal. The ProB model checker then tries to find a model for that formula. If that is possible, this model is a counter example that will be presented back to the user in the proof tree. The disprover also checks if there cannot be a model for the formula. If this is the case it acts like a decision procedure, i.e., absence of a model is a proof for the goal. Unfortunately, sometimes neither a counter example nor a proof can be found. |

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

[[Category:User documentation]] | [[Category:User documentation]] |

## Revision as of 13:36, 9 April 2013

## ProB Disprover

The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples or proofs for a given proof obligation.

The Disprover is described in Debugging Event-B Models using the ProB Disprover Plug-in, Ligot, Bendisposto, Leuschel.

## Installation

The ProB Disprover is currently only available through the ProB Nightly Build Update Site (http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/).

## How to use it, how it works

: The proof obligation editor in Rodin presents the user with a number of Hypotheses and one Goal, to be proved. If the Disprover is installed, it is available in the tool bar alongside the other provers.

Upon selecting the Disprover, it builds a formula from the Hypotheses and the negated Goal. The ProB model checker then tries to find a model for that formula. If that is possible, this model is a counter example that will be presented back to the user in the proof tree. The disprover also checks if there cannot be a model for the formula. If this is the case it acts like a decision procedure, i.e., absence of a model is a proof for the goal. Unfortunately, sometimes neither a counter example nor a proof can be found.