4.1 Universo de Herbrand
Cuando lo simbolos de función son usados para formar términos, el conjunto de posibles interpretacines es extremadamente complejo. En esta sección, se muestra que un conjunto de clausulas tiene interpretaciones canónicas: si un conjunto de cláusulas tiene un modelo, entonces, tiene una interpretación canónica. Sea
un conjunto de cláusulas, el conjunto de símbolos constantes en y el conjunto de símbolos función en se define inductivamente:Como un caso especial, si no hay simbolos constantes en
, inicialize la definición inductiva de con un simbolo constante arbitrario a.El Universo de Herbrand es el conjunto de términos atados que pueden ser formados con los símbolos en
. Obviamente, si contiene un símbolo función, el Universo de Herbrand es infinito dado queEjemplos:
Sea
el Universo de Herbrand para un conjunto de clausulas . La Base Herbrand () son los átomos atados que pueden formarse de los símbolos predicados en y términos en .Una Interpretación Herbrand para un conjunto de cláusulas
es una interpretación cuyo dominio es el Universo de Herbrand para y cuyos simbolos constantes y función son asignados “por si mismos”:No hay restricciones en las asignaciones en relación de el Universo de Herbrand y los predicados. Un Modelo de Herbrand para un conjunto de cláusulas
es una interpretación Herbrand la cual satisface . Puede ser identificada con un subconjunto de la base Herbrand por cadaEjemplo: La Base Herbrand para el conjunto de formulas
del ejemplo anterior es:Un Modelo Herbrand para
puede ser definido:o de manera mas simple, mediante un subconjunto de la Base Herbrand:
Sea
un conjunto de cláusulas. tiene un modelo si y solo si tiene un modelo de Herbrand.| <= | Regresar Tema 3.2 Funciones y Términos? |
| => | Siguiente Tema: 4.2 Forma de Skolem |
| Regresar al TEMARIO: Matematicas Para Maestria |
