It is shown that J. A. Robinson's P1—deduction is a special case of a large class of types of deduction by resolution, an optimum choice from which should be possible for any particular theorem to be proved. Some further results, based on the operation of renaming literals by means of their negations, are obtained and suggest an alternative approach to automatic deduction.
No takes yet. Share an insight, caveat, or question.
Bernard D. Meltzer (1966) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: