“A Machine-Oriented Logic Based on the Resolution Principle” was published by John Alan Robinson in the Journal of the ACM, volume 12, number 1, pages 23 to 41, in January 1965. The paper gave automated reasoning a single, powerful inference rule, resolution, and is one of the foundation stones of computational logic.
Before Robinson, programs that tried to prove theorems in first-order logic used many separate rules and tended to drown in possibilities. Robinson combined the work of substitution, finding the right way to match variables, with truth-functional reasoning into one operation. The key technical ingredient is unification, a procedure that finds the most general way to make two logical expressions identical. With unification in hand, resolution can repeatedly combine clauses to derive new ones, and a proof is found by deriving a contradiction from the negation of the goal. The result was an inference engine simple enough for a machine to run systematically yet complete enough to find any valid proof eventually.
Resolution reshaped its field. It became the standard basis for automated theorem provers, and a restricted, efficient form of it, applied to Horn clauses, became the execution model of the programming language Prolog. The idea that a computer could be handed logical facts and rules and made to derive consequences mechanically traces directly to this paper.
Why business readers should care: resolution is the engine inside logic-based reasoning systems, from formal verification of chips and software to the rule engines and knowledge bases used in compliance and configuration. It is the technical reason a machine can answer “does this follow from what we already know?”