In computer science, it is important to verify properties of data structures such as arrays and linked lists, and generic properties of procedures such as encoding and decoding. In general, these properties can be described in first-order logic with equality, that is, by using first-order axioms that describe arrays or linked lists. In many important situations, the only part that cannot be described in propositional terms is the background theory (of arrays, linked lists, integers, and so on). In such situations, we need to check the satisfiability (or validity) of a propositional formula in which propositional variables are actually first-order statements from a given background first-order theory. Such checking is called satisfiability modulo theories. (The term satisfiability is often abbreviated as SAT.)

One of the approaches to such checking is to replace the original set of first-order clauses with several grounded instances, by performing an appropriate instantiation. After that, we can apply efficient SAT solvers to the resulting purely propositional problem. In general, we can generate a large (sometimes infinite) number of instantiated formulas, and if we stop after generating some of them, there is no guarantee that the resulting answer is correct. It is therefore important to develop efficient instantiation schemes to provide such a guarantee. The authors describe a guaranteed scheme applicable to many mathematical theories, including those that describe data types and encryption-decryption schemes. When the number of variables in each clause is bounded by a given constant, this instantiation scheme requires feasible (polynomial) time.

The paper is very well written. A basic knowledge of logic is, of course, necessary to fully understand the results. The paper is intended for readers familiar with the basic concepts of automated theorem proving. However, a detailed introduction with basic definitions has been added for those less familiar with these concepts. For the convenience of all readers, the proofs are made as simple as possible, within the single-sorted framework (from which the corresponding results can be easily generalized); the most technical proofs are located in a special appendix.