El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue:

Property Value
dbo:abstract
  • El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue: * para cada variable en la fórmula * para cada cláusula que contenga la variable y cada cláusula que contenga la negación de la variable * resolver y y añadir la resolución a la fórmula * eliminar todas las cláusulas originales que contengan la variable o su negación El nombre algoritmo Davis-Putnam o algoritmo DP a veces es empleado incorrectamente para referirse al algoritmo DPLL, el cual está relacionado pero es diferente. (es)
  • El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue: * para cada variable en la fórmula * para cada cláusula que contenga la variable y cada cláusula que contenga la negación de la variable * resolver y y añadir la resolución a la fórmula * eliminar todas las cláusulas originales que contengan la variable o su negación El nombre algoritmo Davis-Putnam o algoritmo DP a veces es empleado incorrectamente para referirse al algoritmo DPLL, el cual está relacionado pero es diferente. (es)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 739990 (xsd:integer)
dbo:wikiPageLength
  • 2142 (xsd:integer)
dbo:wikiPageRevisionID
  • 119497325 (xsd:integer)
prop-es:apellido
  • Loveland (es)
  • Davis (es)
  • Putnam (es)
  • Logemann (es)
  • Loveland (es)
  • Davis (es)
  • Putnam (es)
  • Logemann (es)
prop-es:año
  • 1960 (xsd:integer)
  • 1962 (xsd:integer)
prop-es:enlaceautor
  • Martin Davis (es)
  • Martin Davis (es)
prop-es:nombre
  • Martin (es)
  • Hillary (es)
  • Donald (es)
  • George (es)
  • Martin (es)
  • Hillary (es)
  • Donald (es)
  • George (es)
prop-es:número
  • 1 (xsd:integer)
  • 7 (xsd:integer)
prop-es:páginas
  • 201 (xsd:integer)
  • 394 (xsd:integer)
prop-es:revista
  • Journal of the ACM (es)
  • Communications of the ACM (es)
  • Journal of the ACM (es)
  • Communications of the ACM (es)
prop-es:título
  • A Computing Procedure for Quantification Theory (es)
  • A Machine Program for Theorem Proving (es)
  • A Computing Procedure for Quantification Theory (es)
  • A Machine Program for Theorem Proving (es)
prop-es:url
prop-es:volumen
  • 5 (xsd:integer)
  • 7 (xsd:integer)
dct:subject
rdfs:comment
  • El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue: (es)
  • El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue: (es)
rdfs:label
  • Algoritmo de Davis-Putnam (es)
  • Algoritmo de Davis-Putnam (es)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is owl:sameAs of
is foaf:primaryTopic of