= Solution
Fix a signature, adding a fresh constant if it otherwise has no ground terms. Its <Herbrand universe> $U$ is the set of all ground terms, and its <Herbrand base> $B$ is the set of all <ground atoms> over $U$. A <Herbrand interpretation> is identified with a subset $I\subseteq B$: precisely its members are true. Function symbols and constants have their term interpretations.
A <least Herbrand model> of a <knowledge base> $\mathcal K$ is a <Herbrand model> $M$ satisfying
$$
\boxed{M\models\mathcal K\quad\text{and}\quad M\subseteq J\text{ for every Herbrand model }J\models\mathcal K.}
$$
If it exists, it is unique. This is stronger than being minimal: a minimal model merely has no strictly smaller model contained in it.
For a positive definite <Datalog> program with facts, let $T$ add every fact and the head of every ground rule whose body is already true. Starting from the empty set and repeatedly adding consequences yields
$$
\boxed{M=\bigcup_{n\ge0}T^n(\varnothing)=\bigcap\{J:J\text{ is a Herbrand model of }\mathcal K\},}
$$
where $T$ is taken inflationary, so it also retains its input. Every added <ground atom> belongs to every model, and the union is closed under every finite rule body. These two facts establish that it is the <least Herbrand model>. The intersection assertion is guaranteed here by the definite Horn form, not for arbitrary <knowledge bases>.
Back to article page
