First-order atom definitions extended

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 sufficient 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.