**Summary:** J. A. Robinson's paper introduces a machine-oriented logic based on the resolution principle, which is a key method for theorem proving in first-order logic. The resolution principle combines substitution and truth-functional analysis into a single process, making it more efficient than traditional methods. The paper presents a system of first-order logic with only one inference principle—the resolution principle—which is both sound and complete. This principle allows for the derivation of logical consequences and is central to efficient theorem-proving procedures. The paper discusses the theoretical foundations of the resolution principle, including the concepts of substitution, unification, and resolution. It also introduces the idea of saturation procedures, which are used to determine the satisfiability of a set of clauses by iteratively applying resolution. The resolution principle is shown to be semicommutative with saturation, allowing for efficient computation. The paper then presents the resolution theorem, which states that a finite set of clauses is unsatisfiable if and only if some finite subset of its ground clauses is unsatisfiable. This theorem is crucial for determining the satisfiability of logical statements using resolution. The paper also discusses the development of efficient refutation procedures, which are essential for practical applications of the resolution principle. It introduces the concept of search principles, which guide the design of efficient proof procedures. These principles help in identifying and eliminating redundant steps in the resolution process, thereby improving efficiency. The paper concludes with examples of refutations using the resolution principle, demonstrating its effectiveness in proving theorems. It also highlights the importance of the resolution principle in automating logical reasoning and its potential for practical applications in computer science and artificial intelligence.**Summary:** J. A. Robinson's paper introduces a machine-oriented logic based on the resolution principle, which is a key method for theorem proving in first-order logic. The resolution principle combines substitution and truth-functional analysis into a single process, making it more efficient than traditional methods. The paper presents a system of first-order logic with only one inference principle—the resolution principle—which is both sound and complete. This principle allows for the derivation of logical consequences and is central to efficient theorem-proving procedures. The paper discusses the theoretical foundations of the resolution principle, including the concepts of substitution, unification, and resolution. It also introduces the idea of saturation procedures, which are used to determine the satisfiability of a set of clauses by iteratively applying resolution. The resolution principle is shown to be semicommutative with saturation, allowing for efficient computation. The paper then presents the resolution theorem, which states that a finite set of clauses is unsatisfiable if and only if some finite subset of its ground clauses is unsatisfiable. This theorem is crucial for determining the satisfiability of logical statements using resolution. The paper also discusses the development of efficient refutation procedures, which are essential for practical applications of the resolution principle. It introduces the concept of search principles, which guide the design of efficient proof procedures. These principles help in identifying and eliminating redundant steps in the resolution process, thereby improving efficiency. The paper concludes with examples of refutations using the resolution principle, demonstrating its effectiveness in proving theorems. It also highlights the importance of the resolution principle in automating logical reasoning and its potential for practical applications in computer science and artificial intelligence.