Rodin Handbook





 
Previous: Proof Tactics Up: Proving Next: How to Use the Provers Effectively Rodin User’s Handbook v.2.8

3.4.4 Provers

In the end, provers perform the actual work. Rodin comes with one prover installed (New PP). It is strongly recommended that you install the third-party provers from Atelier B (as described in Section 3.4.4) in order to add the PP and ML provers. More provers may be available as plugins.

We will now give a very brief overview of the existing provers by pointing out their strengths/weaknesses.

3.4.4.1 PP

We recommend trying the PP prover first because it is sound and does a pretty good job.

Names in the proof control:

P0, P1, PP

Names in the proof tree:

PP

Names in the preferences:

Atelier B P0, Atelier B P1, Atelier B PP

Input:

In the configuration “P0", all selected hypotheses and the goal are passed to PP. In the configuration “P1", one lasso operation is applied to the selected hypotheses and the goal and the result is passed to PP. In the configuration “PP", all the available hypotheses are passed to PP.

How the Prover Proceeds:

The input sequent is translated to classical B and fed to the PP prover of Atelier B. PP works in a manner similar to newPP but with support for equational and arithmetic reasoning.

Some Strengths:

 

  • PP has limited support for equational and arithmetic reasoning.

Some Weaknesses:

 

  • PP does not output a set of used hypotheses.

  • PP is unaware of some set theoretical axioms.

  • PP has similar problems to New PP with regard to well-definedness.

  • If unnecessary hypotheses are present, they may prevent PP from finding a proof even when the proof obligation obviously holds.

3.4.4.2 ML

The ML prover can be quite helpful when the proofs involve arithmetic.

Names in the proof control:

M0, M1, M2, M3, ML

Names in the proof tree:

ML

Names in the preferences:

Atelier B ML

Input:

All visible hypotheses are passed to ML. The different configurations refer to the configuration (proof force) of the ML prover.

How the Prover Proceeds:

ML applies a mix of forward, backward and rewriting rules in order to discharge the goal (or detect a contradiction among hypotheses).

Some Strengths:

 

  • ML has limited support for equational and arithmetic reasoning.

  • ML is more resilient to unnecessary hypotheses than newPP and PP.

Some Weaknesses:

 

  • ML does not output a set of used hypotheses.

  • Not all set theoretical axioms are part of ML.

3.4.4.3 New PP

\includegraphics[width=7mm]{img/warning_64.png}

New PP is unsound. There have been several bug reports. Some have been fixed, but at this point we do not recommend New PP for inexperienced users.

Names in the proof control:

nPP R., nPP with a lasso symbol, nPP

Names in the proof tree:

Predicate Prover

Names in the preferences:

PP restricted, PP after lasso, PP unrestricted

Input:

In the configuration “restricted", all selected hypotheses and the goal are passed to New PP. In the configuration “after lasso", a lasso operation is applied to the selected hypotheses and the goal and the result is passed to New PP. The lasso operation selects any unselected hypothesis that have a common symbol with the goal or a hypothesis that is currently selected. In the configuration “unrestricted", all the available hypotheses are passed to New PP.

How the Prover Proceeds:

First, all function and predicate symbols that are different from “$\in $" and not related to arithmetic are translated away. For example A $\subseteq B$ is translated to $\forall x\cdot x \in A \mathbin \Rightarrow x \in B$. Then New PP translates the proof obligation to CNF (conjunctive normal form) and applies a combination of unit resolution and the Davis Putnam algorithm.

Some Strengths:

 

  • New PP outputs a set of “used hypotheses". If an unused hypotheses changes, the old proof can be reused.

  • New PP has limited support for equational reasoning.

Some Weaknesses:

 

  • New PP is unsound. There have been several bug reports.

  • New PP does not support arithmetic; hence, $\vdash _{\mathcal L} 1=1$ is discharged, but $\vdash _{\mathcal L} 1+1=2$ is not. Note that arithmetic reasoning when the formula is not ground (i.e. the formula contains variables) is a long standing challenge.

  • New PP is unaware of set theoretical axioms. In particular, $\vdash _{\mathcal L} \exists A\cdot \forall x\cdot x \in A \mathbin \Leftrightarrow x \in B \lor x \in C$ is not recognized because the union axiom is not available within New PP. This means that New PP can only reuse sets that already appear in the formula, but it is unable to introduce new sets. Note that set theoretical reasoning is perceived as a hard problem.

  • If unnecessary hypotheses are present, they may prevent New PP from finding a proof even when the proof obligation obviously holds. We therefore advise you to unselect unnecessary hypotheses.

  • New PP does not take well-definedness into account: Lemma $\vdash _{\mathcal L} b \in f^{-1} [\{ f(b)\} ]$ is not discharged. In fact, this sequent has exactly the same translation as $\vdash _{\mathcal L} b \in \mathop {\mathrm{dom}}\nolimits (f)$, which cannot be proved.

  • New PP tends to run out of memory if the input is large.

Previous: Proof Tactics Up: Proving Next: How to Use the Provers Effectively  
Rodin User’s Handbook v.2.8 : Reference : Proving : Provers