Relevance Filter Plug-in

The purpose of the Relevance Filter Plugin is to try to automatically select relevant hypotheses for a proof as opposed to the user doing this manually.

Instructions

The relevance filter can be invoked either by clicking the RF button in the proof control, or automatically as part of the auto tactic.

It also comes with a preference dialog (under Event-B > Sequent Prover > Meta Prover) that allows you to configure the filter(s). The plugin implements several filtering methods that will be tried sequentially. The default setting is a selection of filters that have been found to work well.

If you want to add the relevance filter to the auto tactic you should add the Meta Prover item. It replaces NewPP after lasoo, NewPP unrestricted, Atelier B P1 and Atelier B PP since this functionality is already included in the Meta prover. You still have to add ML at the appropriate place in the tactic as well as NewPP restricted and Atelier B P0.

You can install the feature composition plug-in from the Rodin Update Site.

Filters

The relevance filter plugin includes the following filtering methods:

• Meng & Paulson's relevance filter

This filter uses a set of relevant symbols which is initialized with the symbols contained in the goal. Hypotheses are then selected if they contain the symbols contained in this set of relevant symbols. When selected their symbols are also added to the set of relevance filters. The passmark parameter determines how many symbols a hypothesis may contain that are not in the relevant set, in order to be selected. When the pass mark parameter is 0.8 a hypothesis is still considered relevant if 20% of its symbols are not in the relevant set. I.e. higher numbers select less hypotheses. When running the algorithm the pass mark is increased incrementaly to avoid selecting too many hypotheses. The c paramter determines how fast this happens. The parameter must be greater or equal to 1, where 1 is the fastest increase.

• SInE

SInE is based on the idea that each symbol has a defining hypothesis. It selects all hypotheses that define a symbol contained in the goal and recursively all hypotheses that define a symbol contained in the previously selected hypotheses.

• DCR

This filter builds a weighted graph between all hypotheses and the goal. The edges are weighted based on the symbol overlap between the connected formulas. The threshold parameter defines the maximal distance a hypothesis may have from the goal in order to be considered relevant. If "use contextual relevance" is selected the overall frequency of a symbol is taken into account when computing the distance between two formulas.

• Sub-Expression filter

Selects hypotheses that have a common expression with the goal. The initial selection size parameter determines how many hypotheses similar to the goal are selected in the initialization step at most. The threshold parameter defines how similar the formulas selected in the initialization step must be to the goal. Higher means more similar. The value must be between 0 and 1.

• Lasso

Selects all hypotheses that have a symbol in common with the goal or any of the selected hypotheses

• Unrestricted

Selects all hypotheses.

More information can be found in "Relevance Filters for Event-B"

Releases

Version 1.0.0

27th Sep 2010

Version compatible with Rodin 2.0

References

• Röder, Jann "Relevance Filters for Event-B", ETH Zürich, April 5, 2010