Content deleted Content added
Robot-assisted spelling. See User:Mathbot/Logged misspellings for changes. |
m propositional logic, +de |
||
Line 1:
The '''[[Martin Davis|Davis]]-[[Hilary Putnam|Putnam]] algorithm''' is an algorithm for checking the [[Boolean satisfiability problem|satisfiability]] of [[propositional logic]] formulae in [[conjunctive normal form]], i.e., sets of [[clause]]s. It is a form of [[resolution (logic)|resolution]] in which variables are iteratively chosen and removed by resolving every clause in which the variable is contained positively with any clause in which the variable is negated.
The algorithm works as follows:
Line 25:
{{Mathlogic-stub}}
[[de:Davis-Putnam-Verfahren]]
| |||