Matches in DBpedia 2014 for { <http://dbpedia.org/resource/Davis–Putnam_algorithm> ?p ?o. }
Showing items 1 to 26 of
26
with 100 items per page.
- Davis–Putnam_algorithm 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 that is actually only one of the steps of the original algorithm.The procedure is based on Herbrand's theorem, which implies that an unsatisfiable formula has an unsatisfiable ground instance, and on the fact that a formula is valid if and only if its negation is unsatisfiable. Taken together, these facts imply that to prove the validity of φ it is enough to prove that a ground instance of ¬φ is unsatisfiable. If φ is not valid, then the search for an unsatisfiable ground instance will not terminate. The procedure roughly consists of these three parts: put the formula in prenex form and eliminate quantifiers generate all propositional ground instances, one by one check if each instance is satisfiableThe last part is probably the most innovative one, and works as follows: for every variable in the formula for every clause containing the variable and every clause containing the negation of the variable resolve c and n and add the resolvent to the formula remove all original clauses containing the variable or its negationAt each step, the intermediate formula generated is equisatisfiable to the original formula, but it does not retain equivalence. The resolution step leads to a worst-case exponential blow-up in the size of the formula. The DPLL algorithm is a refinement of the propositional satisfiability step of the Davis–Putnam procedure, that requires only a linear amount of memory in the worst case.".
- Davis–Putnam_algorithm wikiPageID "2732435".
- Davis–Putnam_algorithm wikiPageRevisionID "601737564".
- Davis–Putnam_algorithm subject Category:Automated_theorem_proving.
- Davis–Putnam_algorithm subject Category:Boolean_algebra.
- Davis–Putnam_algorithm subject Category:Constraint_programming.
- Davis–Putnam_algorithm 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.".
- Davis–Putnam_algorithm label "Algorithme de Davis-Putnam".
- Davis–Putnam_algorithm label "Algoritmo de Davis-Putnam".
- Davis–Putnam_algorithm label "Algoritmo de Davis-Putnam".
- Davis–Putnam_algorithm label "Algoritmo di Davis-Putnam".
- Davis–Putnam_algorithm label "Davis-Putnam-Verfahren".
- Davis–Putnam_algorithm label "Davis–Putnam algorithm".
- Davis–Putnam_algorithm label "Procedura Davisa-Putnama".
- Davis–Putnam_algorithm label "デービス・パトナムのアルゴリズム".
- Davis–Putnam_algorithm sameAs Davis%E2%80%93Putnam_algorithm.
- Davis–Putnam_algorithm sameAs Davis-Putnam-Verfahren.
- Davis–Putnam_algorithm sameAs Algoritmo_de_Davis-Putnam.
- Davis–Putnam_algorithm sameAs Algorithme_de_Davis-Putnam.
- Davis–Putnam_algorithm sameAs Algoritmo_di_Davis-Putnam.
- Davis–Putnam_algorithm sameAs デービス・パトナムのアルゴリズム.
- Davis–Putnam_algorithm sameAs Procedura_Davisa-Putnama.
- Davis–Putnam_algorithm sameAs Algoritmo_de_Davis-Putnam.
- Davis–Putnam_algorithm sameAs Q1177898.
- Davis–Putnam_algorithm sameAs Q1177898.
- Davis–Putnam_algorithm wasDerivedFrom Davis–Putnam_algorithm?oldid=601737564.