Content deleted Content added
OK, I've decided after some hesitation to leave the "stub" notice intact, but I'm putting it BELOW everything else the reader sees, since it causes too much blank white space otherwise. |
m link to article on very similar methods |
||
Line 12:
* for every variable in the formula
** for every clause <math>c</math> containing the variable and every clause <math>n</math> containing the negation of the variable
*** [[Resolution (logic)|resolve]] <math>c</math> and <math>n</math> and add the resolvent to the formula
** remove all original clauses containing the variable or its negation
| |||