User:Nicolas/Collections/ADVANCE D3.4 Improvement of automated proof
Overview
TODO
Motivations / Decisions
TODO
ProB as a Disprover / Prover
Usage of ProB as a disprover has been facilitated. Counter-examples are now displayed in an easier to understand fashion. Error messages have been cleared up.
A more in-depth empirical evaluation of using ProB as a prover has been performed [1], using a novel plug-in to compare the performance of different provers [2]. As observed in the initial case studies, ProB is able to find proofs that are not found by the integrated provers or the SMT solvers. For certain classes of proof obligations, i.e. those that heavily rely on enumerated or otherwise finite sets, ProB performs very favourably.
The disprover plug-in now offers the possibility to export proof obligations from inside Rodin into a custom (Prolog-based) format. These files can then be used as test cases for the disprover. We created several initial test cases that cover both provable as well as unprovable obligations.
Several other changes to the disprover plug-in have been made:
- As ProB itself, the disprover and prover are completely aware of theories. See the general information on ProB's theory support for details.
- Based on the empirical evaluation, several improvements have been made to ProB's kernel. While some of them also improve constraint solving in general, other are especially tailored for proof.
- A new setting has been introduced to allow ProB to react differently in animation / constraint solving and (dis-)proving. Mostly, this changes the treatment of well-definedness conditions during constraint solving.
Available Documentation
TODO Tactic profiles are described in the Rodin Handbook[3].
The user manual of the SMT Solvers plug-in is available on the Event-B wiki[4].
Conclusion
TODO
