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 .
definition Let be a closed formula in Skolem form , F * denote the quantifier-free matrix .
F.
=
∀
y
1
∀
y
2
.
.
.
∀
y
n
F.
∗
{\ displaystyle F = \ forall y_ {1} \ forall y_ {2} ... \ forall y_ {n} F ^ {*}}
For F the Herbrand expansion E (F) is defined as:
E.
(
F.
)
=
{
F.
∗
[
y
1
/
t
1
]
[
y
2
/
t
2
]
.
.
.
[
y
n
/
t
n
]
|
t
1
.
.
.
t
n
∈
D.
(
F.
)
}
{\ displaystyle E \ left (F \ right) = \ left \ {F ^ {*} \ left [y_ {1} / t_ {1} \ right] \ left [y_ {2} / t_ {2} \ right ] ... \ left [y_ {n} / t_ {n} \ right] | t_ {1} ... t_ {n} \ in D \ left (F \ right) \ right \}}
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.
example Be
F.
=
∀
x
∀
y
∀
z
P
(
x
,
f
(
y
)
,
G
(
z
,
x
)
)
{\ displaystyle F = \ forall x \ forall y \ forall zP (x, f (y), g (z, x))}
Then see Herbrand Universe .
D.
(
F.
)
=
{
a
,
f
(
a
)
,
G
(
a
,
a
)
,
f
(
G
(
a
,
a
)
)
,
G
(
f
(
a
)
,
f
(
a
)
)
,
.
.
.
}
{\ displaystyle D \ left (F \ right) = \ {a, f (a), g (a, a), f (g (a, a)), g (f (a), f (a)) , ... \}}
The simplest formulas in are:
E.
(
F.
)
{\ displaystyle E \ left (F \ right)}
P
(
a
,
f
(
a
)
,
G
(
a
,
a
)
)
{\ displaystyle P \ left (a, f (a), g (a, a) \ right)}
With
[
x
/
a
]
[
y
/
a
]
[
z
/
a
]
{\ displaystyle \ left [x / a \ right] \ left [y / a \ right] \ left [z / a \ right]}
P
(
f
(
a
)
,
f
(
a
)
,
G
(
a
,
f
(
a
)
)
)
{\ displaystyle P \ left (f (a), f (a), g (a, f (a)) \ right)}
With
[
x
/
f
(
a
)
]
[
y
/
a
]
[
z
/
a
]
{\ displaystyle \ left [x / f (a) \ right] \ left [y / a \ right] \ left [z / a \ right]}
P
(
a
,
f
(
a
)
,
G
(
G
(
a
,
a
)
,
a
)
)
{\ displaystyle P \ left (a, f (a), g (g (a, a), a) \ right)}
With
[
x
/
a
]
[
y
/
a
]
[
z
/
G
(
a
,
a
)
]
{\ displaystyle \ left [x / a \ right] \ left [y / a \ right] \ left [z / g (a, a) \ right]}
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.
E.
(
F.
)
{\ displaystyle E \ left (F \ right)}
See also literature Schöning, Uwe: Logic for computer scientists . 5th edition. Spectrum Akademischer Verlag, Berlin 2000, ISBN 3-8274-1005-3 .
<img src="https://de.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">
![E \ left (F \ right) = \ left \ {F ^ {*} \ left [y_ {1} / t_ {1} \ right] \ left [y_ {2} / t_ {2} \ right] .. . \ left [y_ {n} / t_ {n} \ right] | t_ {1} ... t_ {n} \ in D \ left (F \ right) \ right \}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5c9ef88f5c17d87c418446968285373769fdde4d)
![\ left [x / a \ right] \ left [y / a \ right] \ left [z / a \ right]](https://wikimedia.org/api/rest_v1/media/math/render/svg/20d6947446363c8d41e4c1f6ea8e1d53d9c92b83)
![\ left [x / f (a) \ right] \ left [y / a \ right] \ left [z / a \ right]](https://wikimedia.org/api/rest_v1/media/math/render/svg/a75359be94fa0f1defb18cf5069b8de22de9a7e2)
![\ left [x / a \ right] \ left [y / a \ right] \ left [z / g (a, a) \ right]](https://wikimedia.org/api/rest_v1/media/math/render/svg/97c2a0198f3dbe28f73b809d968e22158dc911ae)