Autor Tema: Libro o explicación: método de Davis-Putman

0 Usuarios y 1 Visitante están viendo este tema.

01 Junio, 2015, 04:01 pm
Leído 1183 veces

william bautista

  • Nuevo Usuario
  • Mensajes: 3
  • Karma: +0/-0
  • Sexo: Masculino
Hola, estoy necesitando un libro: A. Leitsch. The Resolution Calculus. Springer Verlag. 1997. necesito demostar que el método de Davis-Putman es correcto, pero casi no encuentro información,  si alguien sabe de otro libro donde la pueda estudiar este método. Mucha gracias.

01 Junio, 2015, 06:06 pm
Respuesta #1

luis

  • Aprendiz
  • Mensajes: 304
  • Karma: +1/-0
  • Sexo: Masculino
¿Davis-Putman o Davis-Putnam-Logemann-Loveland?

02 Junio, 2015, 07:11 am
Respuesta #2

william bautista

  • Nuevo Usuario
  • Mensajes: 3
  • Karma: +0/-0
  • Sexo: Masculino
 creo que digite mal es: Davis-Putnam.

02 Junio, 2015, 08:32 pm
Respuesta #3

luis

  • Aprendiz
  • Mensajes: 304
  • Karma: +1/-0
  • Sexo: Masculino
¿Davis-Putnam o Davis-Putnam-Logemann-Loveland?

(no es por la m, es porque son cosas distintas)

02 Junio, 2015, 11:41 pm
Respuesta #4

william bautista

  • Nuevo Usuario
  • Mensajes: 3
  • Karma: +0/-0
  • Sexo: Masculino

03 Junio, 2015, 04:38 am
Respuesta #5

luis

  • Aprendiz
  • Mensajes: 304
  • Karma: +1/-0
  • Sexo: Masculino
Lo primero que tendrías que tener claro es qué significa que ese algoritmo es correcto; que el algoritmo te indica que la fórmula es satisfacible si y solamente efectivamente lo es.

En la Wikipedia http://es.wikipedia.org/wiki/Algoritmo_de_Davis-Putnam se propone el siguiente algoritmo:

1. para cada variable en la fórmula
   1.a. para cada cláusula c que contenga la variable y cada cláusula n que contenga la negación de la variable
      1.a.i. resolver c y n y añadir la resolución a la fórmula
   1.b. eliminar todas las cláusulas originales que contengan la variable o su negación

Este planteo presupone que sabés que la fórmula está expresada como conjunto de cláusulas, y que sabés qué es resolver dos cláusulas.

Lo que este planteo no explicita es cuándo el algoritmo indica que la fórmula es o no es satisfacible. Debes recordar que la cláusula vacía es insatisfacible.

Me parece que el argumento más simple para mostrar la corrección sería una inducción en la cantidad de variables de la fórmula.

saludos