Logica Computacional

Investigación:
1. Que es el algoritmo o método de resolución explique cada una de sus etapas con ejemplo:

Algoritmo o método de resolución:
El algoritmo o método de resolución es casi idénticoal de lógica proposicional.

El algoritmo o método de resolución es una regla de inferencia que toma dos clausulas y produce una tercera que es consecuencia lógica de estas.

El método deresolución requiere que una fórmula se encuentre en forma clausular. Afortunadamente, es posible convertir cualquier conjunto de fórmulas en su "equivalente" 1conjunto de fórmulas en formaclausular.

Suponga que quiere demostrar que es consecuencia lógica de . El método es
el siguiente:

• Transforme las oraciones en Σ ∪ {¬ } a forma normal prenex sin cuantificadores
Existenciales.• Usando la equivalencia ∀x (φ(x) ∧ ψ(x)) ↔ ∀x φ(x) ∧ ∀x ψ(x) transforme las
Formulas a un conjunto de cláusulas C = {C1, . . . , Cn} sin cuantificadores.

• Mientras ∈ C y existen Ci, Cj ∈ C,tales que la regla de resolución es aplicable:
– Aplique la regla de resolución a Ci y Cj generando C´ y haga
C := C ∪ {C´}

• Nuevamente, usamos


Para decir que la oración se puede demostrarpor resolución a partir de Σ.

Ejemplo de Resolución:

• Demuestre que |= ∃x (P(x) → ∀y P(y))

• Primero transformamos la negación de la fórmula en un conjunto de cláusulas.

1. ¬∃x (P(x) → ∀yP(y))
2. ∀x¬(P(x) → ∀y P(y))
3. ∀x (P(x) ∧ ¬∀y P(y))
4. ∀x (P(x) ∧ ∃y ¬P(y))
5. ∀x ∃y (P(x) ∧ ¬P(y))
6. ∀x (P(x) ∧ ¬P(f(x)))


• De la última fórmula, generamos el conjunto de cláusulas{P(x),¬P(f(x))}

• Antes de iniciar la resolución, es siempre conveniente renombrar las variables en las distintas cláusulas. Esto aumenta las posibilidades de encontrar unificadores para estas.

•Este renombramiento también se puede hacer antes de aplicar la regla de
Resolución.

• Partimos con el conjunto de cláusulas

{P(x),¬P(f(y))}

• Basta una aplicación de la regla de resolución...