Abstraction-based relevancy testing for model elimination

Abstract

In application areas like formal software verification or in connection with lemma use, the success of automated theorem provers strongly depends on their ability to choose from a huge number of given axioms only some relevant ones. We present a new technique for deleting irrelevant clauses for model elimination proof procedures which is based on the use of abstractions. We analyze general conditions under which abstractions are well-suited for choosing useful clauses and investigate whether certain abstractions are applicable. So-called symbol abstrac­tions are further examined in a case study which, e.g., introduces new techniques for the automatic generation of abstractions. We evaluate our techniques by means of experiments performed with the prover SETHEO.