Herbrand expansion

from Wikipedia, the free encyclopedia

The Herbrand expansion represents a set of predicate logic formulas that can be derived from a given formula F through a special type of substitution . With the help of this set of formulas, the unsatisfiability of a predicate logic formula can be mapped in a propositional form. The Herbrand expansion was named after the French logician Jacques Herbrand .


Let be a closed formula in Skolem form , F * denote the quantifier-free matrix .

For F the Herbrand expansion E (F) is defined as:

D (F) is the Herbrand universe by F.

Colloquially: All variables in the matrix F * are replaced by terms from D (F), all possibilities are played through. One also speaks of the set of instances of the formula F.



Then see Herbrand Universe .

The simplest formulas in are:


Note that in this case is infinite. The formulas can now be treated like propositional formulas ( propositional logic ) because they do not contain any variables.

See also


  • Schöning, Uwe: Logic for computer scientists . 5th edition. Spectrum Akademischer Verlag, Berlin 2000, ISBN 3-8274-1005-3 .