The paper introduces a machine-oriented logic system based on the resolution principle, designed for computer theorem-proving. The resolution principle combines the processes of substitution and truth-functional analysis into a single, more efficient process. The theory of the resolution process is presented as a system of first-order logic with a single inference principle (the resolution principle), which is proven to be complete. The paper discusses the efficiency of proof procedures and proposes search principles to improve them. The resolution theorem states that a finite set of clauses is unsatisfiable if and only if the resolution of its ground clauses contains a contradiction. The paper also covers the formal preliminaries, including syntax and semantics, and provides examples of refutations using the resolution principle. Finally, it discusses the design of efficient refutation procedures and introduces the purity principle to handle indefinite continuation behavior.The paper introduces a machine-oriented logic system based on the resolution principle, designed for computer theorem-proving. The resolution principle combines the processes of substitution and truth-functional analysis into a single, more efficient process. The theory of the resolution process is presented as a system of first-order logic with a single inference principle (the resolution principle), which is proven to be complete. The paper discusses the efficiency of proof procedures and proposes search principles to improve them. The resolution theorem states that a finite set of clauses is unsatisfiable if and only if the resolution of its ground clauses contains a contradiction. The paper also covers the formal preliminaries, including syntax and semantics, and provides examples of refutations using the resolution principle. Finally, it discusses the design of efficient refutation procedures and introduces the purity principle to handle indefinite continuation behavior.