Instantiation Based First-Order Calculi

Abstract

This paper provides a survey over instantiation based calculi for first-order logic. This kind of calculus, which has the generation of instances of formulae at its core, has been neglected for a long period of time due to the success of resolution based methods. It has experienced a revival in interest in the last decade, as more efficient instantiation based calculi have been developed. After shortly introducing the field of automated theorem proving, some of the current instantiation based methods are described in moderate detail. The survey finishes with a comparison of these methods, based on theoretical properties and practical experiences with existing implementations.