Definición: Sea un lenguaje de primer orden. El universo de Herbrand de se define como el conjunto de los términos cerrados de .
é
Si en no hubiera constantes, se agrega una para poder formar el universo de Herbrand.
Sea el programa lógico
suma(X, 0, X). suma(X, s(Y), s(Z)) :- suma(X, Y, Z).
El universo de Herbrand es
Definición: Sea un lenguaje de primer orden y su universo de Herbrand. La base de Herbrand de se define como el conjunto de fórmulas atómicas cerradas.
La base de Herbrand es
Decimos que un modelo de un lenguaje sobre el universo es un modelo de Herbrand syss cumple lo siguiente:
En los modelos de Herbrand los términos cerrados se interpretan como ellos mismos.
Un modelo de Herbrand para la fórmula define los siguientes elementos:
La elección de para el libre. Digamos:
El modelo de Herbrand no satisface a porque al tomar los términos como , y tenemos que , así , pero sí debería ser cierta.
Ejercicio: Defina un modelo de Herbrand para el cual la satisfaga.
Un modelo de Herbrand define:
Podemos representar a los modelos de Herbrand como subconjuntos de la base de Herbrand. Así es el subconjunto de las fórmulas atómicas que son verdaderas en el modelo de Herbrand , al cual lo identificamos de manera única como .
Para verificar si una fórmula atómica es verdadera en basta ver que .
El modelo anterior queda determinado por
satisface a las cláusulas de .
El modelo de Herbrand no satisface a las cláusulas de .
El modelo de Herbrand tampoco satisface a las cláusulas de .
Definición: Sea un lenguaje, un conjunto de fórmulas en cerradas y universales, y un modelo de . El conjunto de instancias cerradas de , , es , donde y es cualquier sustitución que convierte a cada en instancias particulares del dominio de .
En hay únicamente fórmulas cerradas sin cuantificadores.
Algunos elementos en para la segunda cláusula son:
Sean un lenguaje con al menos una constante y un conjunto de enunciados universales en . Las siguientes afirmaciones son equivalentes:
tiene un modelo
tiene un modelo de Herbrand
Demostración: Las implicaciones y son triviales.
La validez universal de hace ciertas a y .
Demostración: Sea un modelo de . Definimos una estructura de Herbrand sobre mediante la interpretación de los símbolos de predicado. Sea un símbolo de predicado en que recibe argumentos, y .
Por construcción
Lo anterior se puede extender a enunciados sin cuantificadores :
Sea . Que es equivalente a para cualesquiera . Por el syss anterior, esto es equivalente a , es decir, , lo cual es cierto porque es modelo de . De manera que
Así, es un modelo de Herbrand de .
Toda fórmula satisfacible en lógica de predicados tiene un modelo con un universo numerable. Demostración:
Un enunciado universal es insatisfacible syss hay un subconjunto finito de que sea insatisfacbible (en el sentido de la lógica proposicional).
El siguiente es un procedimiento de semi-decisión para el problema de insatisfacibilidad. Tomemos una numeración de como:
Entrada: Un enunciado universal (toda fórmula en lógica de predicados se transforma a esta forma mediante LINREDS) n = 0 repeat n = n + 1 until es insatisfacible output "Insatisfacible" y se detiene
El programa anterior se detiene después de un número finito de pasos para cada entrada que sea una fórmula insatisfacible. Para fórmulas satisfacibles, no se detiene. Si la entrada es , se tiene un procedimiento de semi-decisión para la validez de las fórmulas.
Así obtenemos un procedimiento que se detiene en las fórmulas insatisfacibles y en las válidas.
Otro mecanismo puede buscar sistemáticamente modelos de cardinalidad finita para una dada. Con todo lo anterior llegamos a un procedimiento que se detiene en un número finito de pasos cuando se aplica a las fórmulas en las áreas marcadas.
Los elementos en son en esencia variables proposicionales.
El teorema de Herbrand dice que basta para interpretar a la lógica de predicados.
Si es un programa lógico, entonces tiene un modelo de Herbrand.
Demostración: La base de Herbrand hace verdaderas a todas las cláusulas atómicas del lenguaje, por lo que hace verdaderas a las cláusulas de : hechos o reglas.
Sea un programa lógico. tiene un modelo mínimo de Herbrand, , definido por:
Demostración:
Sea un programa lógico. El modelo mínimo de Herbrand, , se representa por el conjunto de átomos cerrados que son consecuencia lógica de , es decir,
Como contiene exactamente a todos los átomos cerrados que son consecuencia lógica de , este modelo corresponde al significado declarativo de .
La semántica declarativa de está dada por .
Dado un programa lógico , el operador de consecuencia inmediata se define como sigue, donde :
Sea un programa lógico. Definimos las iteraciones del operador de consecuencia inmediata para recursivamente como:
Si es un programa lógico y su modelo mínimo de Herbrand, entonces
Encuentre el modelo mínimo de Herbrand de :
parent(pam, bob). parent(tom, bob). parent(tom, liz). parent(bob, ann). parent(bob, pat). parent(pat, jim). anc(X,Y):-parent(X,Y). anc(X,Y):-parent(X,Z),anc(Z,Y).
Sea el siguiente programa lógico:
p(X,a). q(f(X),X). p(X, f(Y)):-q(X,Y),p(Y,X).
Encuentre el universo, la base y el modelo mínimo de Herbrand.
odd(s(0)). odd(s(s(X))):-odd(X).