An Entity of Type: Procedure101023820, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm.

Property Value
dbo:abstract
• The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm. (en)
dbo:thumbnail
dbo:wikiPageID
• 2732435 (xsd:integer)
dbo:wikiPageLength
• 7042 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
• 1071405701 (xsd:integer)
dbp:date
• June 2021 (en)
dbp:reason
• In the algorithm below, adding to and removing from a formula should be defined. I guess the formula has to be in clausal normal form , and adding and removing is achieved by set operations? Moreover, the 'consistent set of literals' test, and the concepts 'polarity', 'pure literal' and 'unit propagation' should be briefly explained. (en)
dbp:wikiPageUsesTemplate
dct:subject
rdf:type
rdfs:comment
• The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm. (en)
rdfs:label
• Davis–Putnam algorithm (en)
owl:sameAs
prov:wasDerivedFrom
foaf:depiction
foaf:isPrimaryTopicOf
is dbo:knownFor of
is dbo:notableIdea of
is dbo:wikiPageRedirects of