Tema3 programación

que es o para que sirve la Unificación. Sirve para determinar si una formula es consecuencia de un conjunto finito de hipótesis es inutilizable una vez que hemos de manejar una decena de fórmulas. La unificación es la acción y efecto de unificar, relacionada con sinónimos como unión y agrupación.

Etapas del algoritmo de unificación. Comprobar si los símbolos de los predicados son los mismos. En caso negativo los predicados no son unificables. Si los predicados son iguales, han de tener la misma aridad (argumentos). En caso negativo los predicados no son unificables. Comprobaremos los argumentos por pares correspondientes, aplicando el algoritmo recursivamente (es necesario si los argumentos contienen funciones), abortando el proceso desde el momento en que un par de argumentos no sea unificable.

Resolución. La resolución de Robinson evita la generación de conjunto de instancias básicas como exigen los métodos en el teorema de Herbrand. Puede ser aplicada directamente al cualquier conjunto de clausulas para sondear la insatisfactibilidad. Acción y efecto de resolver o resolverse.

que evita La resolución de Robinson. evita la generación de conjunto de instancias básicas como exigen los métodos en el teorema de Herbrand. evita la generación de conjunto de instancias básicas.

Sistema formal. Un conjunto de expresiones básicas y un conjunto de reglas de generación de nuevas expresiones. simion.

Procedimientos efectivos. Desarrollos que involucran un numero finito de operaciones elementales y de posiciones de memoria. posiciones de memoria.

Decidibilidad(ambas son buenas ). Un sistema formal U se dice decible si existen procedimiento efectivos para determinar la validez dentro de U de las expresiones. La decidibilidad se define como la capacidad de un sistema formal para determinar si una fórmula es o no un teorema del sistema, en un número finito de pasos.

Clausulas de HORN. Una clausula de HORN (o definida) es una disyunción de literales, es decir, una secuencia de literales que contiene a lo sumo un literal positivo. Las clausulas de Horn trabajan con secuencias de literales en vez de conjuntos, esto implica dos cosas:. Las clausulas de Horn trabajan con secuencias de literales en vez de conjuntos, esto implica dos cosas:.

Las clausulas de Horn trabajan con secuencias de literales en vez de conjuntos, esto implica dos cosas: Los literales pueden aparecer repetidos en el cuerpo. Un orden en los literales del cuerpo (podemos hablar del primer literal, segundo literal, etc.). Al escribirla en notación de Kowalski tendría una de estas 4 formas.

Los hechos y las reglas se denominan clausulas definidas: Los hechos representan “hechos acerca de los objetos” (de nuestro universo de discurso), relaciones elementales entre estos objetos. Las reglas expresan relaciones condicionales y entre los objetos, dependencias, engloban todos los casos en el siguiente sentido: Un hecho es una regla con cuerpo vacío Un objetivo es una regla con cabeza vacía Y el éxito es una regla con cabeza y cuerpos vacíos.

Las reglas expresan relaciones condicionales y entre los objetos, dependencias, engloban todos los casos en el siguiente sentido: Un hecho es una regla con cuerpo vacío. Un objetivo es una regla con cabeza vacía. Y el éxito es una regla con cabeza y cuerpos vacíos.

a que maquina se iguala la clausula de Horn. Clausulas de Horn. maquina de Turing.

que permiten programar Las clausulas de Horn. Permiten por tanto programar cualquier función computable. gdsgzfbzfbz.

clausulas de Horn. Muchos métodos de resolución de problemas desarrollados en el campo de la inteligencia artificial pueden considerarse como modelos orientados a ser expresados también mediante Clausulas de Horn. Para muchas aplicaciones de la lógica basta con restringirse a las clausulas de Horn.

Resolución SLD. La resolución SLD (Resolución de clausula definida lineal selectiva) es la regla de inferencia básica utilizada en la programación lógica. Es un refinamiento de la resolución, que es a la vez sólida y refutación completa para las clausulas Horn. Es un refinamiento de la resolución, que es a la vez sólida y refutación completa para las clausulas Horn.

Estrategias de resolución SLD. La resolución SLD define implícitamente un árbol de búsqueda de cálculos alternativos, en el que la cláusula de objetivo inicial está asociada con la raíz del árbol. Para cada nodo en el árbol y para cada cláusula definida en el programa cuyo literal positivo se unifica con el literal seleccionado en la cláusula objetivo asociada con el nodo, hay un nodo hijo asociado con la cláusula objetivo obtenida por resolución SLD. Un nodo hoja, que no tiene hijos, es un nodo exitoso si su cláusula de objetivo asociada es la cláusula vacía. Es un nodo de falla si su cláusula de objetivo asociada no está vacía pero su literal seleccionado se unifica sin literal positivo de cláusulas definidas en el programa.

SLDNF. SLDNF es una extensión de la resolución SLD para tratar la negación como falla. En SLDNF, las cláusulas de objetivo pueden contener la negación como literales de falla, por ejemplo, del formulario, que solo se pueden seleccionar si no contienen variables. Cuando se selecciona tal literal libre de variables, se intenta una subprueba (o su computación) para determinar si hay una refutación SLDNF a partir del literal innecesario correspondiente como cláusula superior. La subobjetiva seleccionada tiene éxito si la subprueba falla, y falla si la subprueba tiene éxito.