View Related Documents

Abstract

We extend the notion of atom definitions in first-order formulae by guards. These are conditions restricting the atom definition in a form that frequently occurs in many application areas of automated theorem proving. We give a suficient and complete criterion for a formula to contain such a definition and provide an effective algorithm to actually retrieve the definition in an applicable form. An implementation within our prover Spass leads to significant performance improvements in application areas where atom definitions are present.

Fulltext Preview

Image of the first page of the fulltext document