What people are saying - Write a review
We haven't found any reviews in the usual places.
REFINEMENTS OF RESOLUTION
4 other sections not shown
0-subsumes 0-subsumption 5-literal assertion automated theorem provers auxiliary chain clause set Completeness Theorem conjunctive set consider contrapositive defined Definition deleted derived clause elimination equation example exists extension factor false finite first-order logic formula in Skolem given clause given set goal clause goal tree ground clauses group theory Horn formula Horn set inference rule input refutation instantiation lemma clause linear deduction linear resolution logically equivalent mesh substitution MESON minimally unsatisfiable subset modulant literal multiliteral node notation O-deduction O-factor O-instance obtained occurrence Option ordering rule paramodulation parent chain parent clause predicate letter prefix problem reduction format proof quantifiers reader refined replacement removed resolvent restriction rightmost literal rules of inference s-linear s-resolvent search plan Section semantic tree set of clauses set-of-support shadow literals Skolem conjunctive form Soundness Theorem subgoals subsumption rule symbol tautology tion top clause top O-clause unifier unit clause unit refutation universal quantifiers unsatisfiable set valid