The paper presents a computational procedure for quantification theory, aiming to provide a method for determining the validity of logical formulas. The authors, Martin Davis and Hilary Putnam, discuss the historical context of the problem, noting that while the existence of an algorithm for deciding the validity of quantification theory formulas was once believed, Church and Turing demonstrated that such an algorithm does not exist. However, recent developments have led to the creation of proof procedures that can be used with modern computing machinery. The paper outlines a uniform proof procedure for quantification theory that is feasible for complex formulas and does not typically lead to exponential growth in complexity. This procedure is compared with previous methods, such as those by Hao Wang and P. C. Gilmore, which face significant challenges with more complex formulas. The new method involves generating a sequence of quantifier-free lines and testing their conjunction for consistency using specific rules, which are designed to be feasible even for large systems of formulas. The authors provide a detailed explanation of the procedure, including the steps for generating quantifier-free lines, applying rules for eliminating one-literal clauses, and using the affirmative-negative rule. They also present an example to illustrate the application of the procedure, showing that it successfully refutes a formula that Gilmore's method failed to handle effectively. The paper concludes by highlighting the practical advantages of the new method, particularly in terms of computational efficiency and the ability to handle complex formulas.The paper presents a computational procedure for quantification theory, aiming to provide a method for determining the validity of logical formulas. The authors, Martin Davis and Hilary Putnam, discuss the historical context of the problem, noting that while the existence of an algorithm for deciding the validity of quantification theory formulas was once believed, Church and Turing demonstrated that such an algorithm does not exist. However, recent developments have led to the creation of proof procedures that can be used with modern computing machinery. The paper outlines a uniform proof procedure for quantification theory that is feasible for complex formulas and does not typically lead to exponential growth in complexity. This procedure is compared with previous methods, such as those by Hao Wang and P. C. Gilmore, which face significant challenges with more complex formulas. The new method involves generating a sequence of quantifier-free lines and testing their conjunction for consistency using specific rules, which are designed to be feasible even for large systems of formulas. The authors provide a detailed explanation of the procedure, including the steps for generating quantifier-free lines, applying rules for eliminating one-literal clauses, and using the affirmative-negative rule. They also present an example to illustrate the application of the procedure, showing that it successfully refutes a formula that Gilmore's method failed to handle effectively. The paper concludes by highlighting the practical advantages of the new method, particularly in terms of computational efficiency and the ability to handle complex formulas.