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
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:
Este 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.
Ejercicio: Defina un modelo de Herbrand el cual satisfaga .
Un modelo de Herbrand define:
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
Los modelos de Herbrand se pueden representar 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 , y 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 afirmaciones son equivalentes:
Un modelo satisface a .
Un modelo de Herbrand satisface a .
Demostración: Las implicaciones y son triviales.
La validez universal de hace ciertas a y .
Demostración: Sea un modelo de que lo satisface. 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 .
Del lado derecho, cada término es interpretado por de acuerdo a su universo, y asignación de funciones. Por construcción
Lo anterior se extiende a enunciados sin cuantificadores :
Sea .
corresponde a para cualesquiera . Por el syss anterior, esto equivale a , es decir, , lo cual es cierto porque satisface a . De manera que
Así, es un modelo de Herbrand que satisface a .
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 que lo satisface.
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 cláusulas de programa.
Sea un programa lógico. tiene un modelo mínimo de Herbrand que lo satisface, , definido por:
Demostración:
Sea un programa lógico. El modelo mínimo de Herbrand que lo satisface, , 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 :
La intuición es agregar a aquellos atómos que con la cabeza de cláusulas cerradas en cuyo cuerpo se conforma por elementos de .
Sea un programa lógico. Definimos las iteraciones del operador de consecuencia inmediata para recursivamente como:
Si es un programa lógico y el modelo mínimo de Herbrand que lo satisface, entonces
Encuentre el modelo mínimo de Herbrand de que lo satisface:
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 que lo satisface.
odd(s(0)). odd(s(s(X))):-odd(X).