Expresión del suelo

AUn término fundamental es untérminoque no contiene variables. Los términos fundamentales pueden definirse mediante recursión lógica (recursión de fórmula):

1. Elementos de${\displaystyle C}$son términos básicos;
2. Si${\displaystyle f\in F}$es un${\displaystyle n}$-ario símbolo de función y${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$son términos básicos, entonces${\displaystyle f\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$es un término básico.
3. Cada término fundamental puede obtenerse mediante una aplicación finita de las dos reglas anteriores (no existen otros términos fundamentales; en particular, los predicados no pueden ser términos fundamentales).

En términos generales, el universo de Herbrand es el conjunto de todos los términos básicos.

Apredicado fundamental ,átomo fundamental oUn literal fundamental es unafórmula atómicacuyos términos de argumento son todos términos fundamentales.

Si${\displaystyle p\in P}$es un${\displaystyle n}$Símbolo de predicado -ario y${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$son términos básicos, entonces${\displaystyle p\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$es un predicado fundamental o átomo fundamental.

En términos generales, la base de Herbrand es el conjunto de todos los átomos fundamentales, ^{[ 1 ]} mientras que una interpretación de Herbrand asigna un valor de verdad a cada átomo fundamental en la base.

Afórmula molida oLa cláusula fundamental es una fórmula sin variables.

Las fórmulas básicas pueden definirse mediante recursión sintáctica de la siguiente manera:

1. Un átomo fundamental es una fórmula fundamental.
2. Si${\displaystyle \varphi }$y${\displaystyle \psi }$son fórmulas básicas, entonces${\displaystyle \lnot \varphi }$,${\displaystyle \varphi \lor \psi }$, y${\displaystyle \varphi \land \psi }$son fórmulas básicas.

Las fórmulas básicas son un tipo particular de fórmulas cerradas .