Ensayo lógica de predicados
1) Forma normal de Skolem
Una fórmula puede ser Skolemizada, lo que implica que sus cuantificadores existenciales son suprimidos, produciendo una nueva fórmula equisatisfactible con respecto a la original.
2)Sustitución
Es una regla de transformación que puede ser aplicada únicamente a un segmento particular de una expresión.
3)Conjunto de diferencias
4)Unificación algoritmo
La unificación es un proceso que consiste en encontrar una asignación de variables que haga idénticas a las fórmulas que se desea unificar. Su resultado, el unificador, se expresa como un conjunto de pares substitución/variable para cada una de las variables asignadas.
5)Resolución
Es una regla de inferencia utilizada sobre cierto tipo de proposiciones lógicas y es especialmente utilizada para los demostradores automatizados de teoremas. Utilizando resolución se puede construir un demostrador que sea completo (por contradicción) y correcto para la lógica proposicional y de primer orden supuesto que un conjunto de proposiciones son insatisfacción.
Una fórmula puede ser Skolemizada, lo que implica que sus cuantificadores existenciales son suprimidos, produciendo una nueva fórmula equisatisfactible con respecto a la original.
2)Sustitución
Es una regla de transformación que puede ser aplicada únicamente a un segmento particular de una expresión.
3)Conjunto de diferencias
4)Unificación algoritmo
La unificación es un proceso que consiste en encontrar una asignación de variables que haga idénticas a las fórmulas que se desea unificar. Su resultado, el unificador, se expresa como un conjunto de pares substitución/variable para cada una de las variables asignadas.
5)Resolución
Es una regla de inferencia utilizada sobre cierto tipo de proposiciones lógicas y es especialmente utilizada para los demostradores automatizados de teoremas. Utilizando resolución se puede construir un demostrador que sea completo (por contradicción) y correcto para la lógica proposicional y de primer orden supuesto que un conjunto de proposiciones son insatisfacción.

Comentarios
Publicar un comentario