La colección de todas las fórmulas atómicas ground (átomos sin variables) que se pueden formar aplicando símbolos de predicado a tuplas de términos del universo de Herbrand de un lenguaje.

Principio

Combinar cada predicado n-ario con todas las n-tuplas de términos ground del universo de Herbrand para generar todos los átomos ground posibles; la base es puramente sintáctica y viene determinada por la firma y el universo de Herbrand.

Demostración

Con el predicado p/1 y universo de Herbrand {a, f(a)}, la base contiene p(a) y p(f(a)); con q/2 y universo {a,b} contiene q(a,a), q(a,b), q(b,a), q(b,b).

Aplicación incorrecta

Suponer que la base de Herbrand lista exactamente los átomos verdaderos de una teoría sin fijar una interpretación o modelo; confundir la base con el conjunto de consecuencias de la teoría o con los átomos verdaderos en un modelo concreto.

Consecuencia

Sirve como dominio para definir interpretaciones de Herbrand (asignaciones de verdad a átomos ground) y para groundear cláusulas a forma proposicional empleada en demostración automática y programación lógica.

Inversión

En lugar del conjunto sintáctico completo de átomos ground, considerar un modelo de Herbrand particular que seleccione un subconjunto como verdaderos; la inversión destaca el paso de átomos potenciales a asignaciones efectivas de verdad.

Límite

Incluye solo fórmulas atómicas formadas con los símbolos de predicado aplicados a términos del universo de Herbrand; excluye fórmulas no atómicas, variables, metatérminos y asignaciones de verdad sin una interpretación fijada.

Tensión semántica

Tensión entre la base de Herbrand como reserva sintáctica de todos los átomos ground posibles y la noción semántica de cuáles de esos átomos son verdaderos en un modelo; la base por sí sola no determina la verdad.

Síntesis

La base de Herbrand es el catálogo sintáctico completo de átomos ground generables por los predicados y el universo de Herbrand de un lenguaje; es la base para interpretaciones de Herbrand, grounding y búsqueda de modelos.