Relevance filters for event-B
Jann Röder · Repository for Publications and Research Data (ETH Zurich) · 2010
Unnecessary hypotheses, that are not required to find a proof of the goal, often prevent an automated theorem prover (ATP) from finding a proof within reasonable time.In this thesis we examine and compare a number of syntactic relevance filtering techniques from the literature as well as our own relevance filtering idea based on structural similarities between formulas.The evaluation of the filtering techniques in the context of Event-B shows that relevance filtering provides a significant advantage in both proving times and success rate over not using filtering.Additionally we show that using several different relevance filtering techniques with short prover timeouts improves the success rate significantly more than increasing the prover timeout for a single filtering strategy.We present a filtering strategy for the Rodin platform that reduces the number of proofs that need help by the user by about 40 % compared to pre-existing strategies.Finally we will show that our filtering strategy achieves a success rate that lies within one percentage point of what is possible using a perfect relevance filter that selects exactly the required hypotheses.