A Human Oriented Logic for Automatic Theorem-Proving
Arthur J. Nevins · Journal of the ACM · 1974
A deductive system is described which combines aspects of resolution (e.g. unification and the use of Skolem functions) with that of natural deduction and whose performance compares favorably with the best predicate calculus theorem provers.