Good summary :-) A resolution uniform proof procedure had the problem that once all the propositions had been flattened in to clauses, the proof procedure di

Good summary :-) A resolution uniform proof procedure had the problem that once all the propositions had been flattened in to clauses, the proof procedure did not have a good idea where to focus its efforts.