Herbrandization

from Wiktionary, Creative Commons Attribution/Share-Alike License.

• noun logic The conversion of a formula of first-order logic which involves the following steps: (1) replace free variables with constants, (2) replace any variable bound by a universal quantifier which lies in the scope of an even number of logical negations (with a function of the remaining bound variables whose scope contain the given variable), and (3) replace any variable bound by an existential quantifier which lies in the scope of an odd number of negations (with a function of the remaining bound variables whose scope contain the given variable).