Just as the flair surrounding automated theorem proving and the union of logic and programming was beginning to die down, a mathematician named John Alan Robinson discovered an inference rule that could be used in place of all the others, providing that the sentences were in clausal form. This inference rule is known as resolution. Although Alan Robinson discovered the rule in 1965, it is a descendant of an earlier concept known as 'Herbrand's proof procedure' from the 1930s.

Resolution was a big step for research on automated theorem proving but still failed to address the issue of large search spaces. This was overcome pragmatically by taking onboard two key concepts:

With these advances, the first logic programming language, Planner was developed in 1969 by Carl Hewitt at MIT. Following Planner, came Prolog in 1972. By now the focus of logic programming had shifted slightly away from automated theorem proving and more towards artificial intelligence. Prolog was designed with Natural Language Processing in mind, which is itself a subset of the A.I. field.