abstract ;;Quote: resolution combines substitution with truth-functional analysis; includes proof of completeness and discussion of efficient proof-procedures

23 ;;Quote: resolution is an inference principle specifically designed for computer theorem-proving programs; the complexity of the principle does not matter; permits a very compact, not to say elegant, piece of reasoning

23+;;Quote: an inference principle needs to be sound (i.e., allow only logical consequences) and effective (i.e., algorithmically decidable)

24 ;;Quote: resolution may be the first complete system of first-order logic using just one inference principle

35 ;;Quote: the resolution principle -- from any two clauses, one may infer a resolvent; a refutation is a sequence of resolutions leading to the empty clause; unsatisfiable iff refutation

38 ;;Quote: resolution search principles include purity (one may delete pure clauses), subsumption (C subsumes D if there is a substitution), and replacement (a resolvent may replace a subsumed clause)