This paper presents a computational procedure for quantification theory, which is a method to determine whether a given formula in quantification theory is logically valid. The procedure is based on the idea of replacing existential quantifiers with function symbols, allowing for the generation of a sequence of quantifier-free lines. These lines are then tested for consistency using a set of rules that help eliminate one-literal clauses, apply the affirmative-negative rule, and eliminate atomic formulas. The algorithm terminates if the conjunction of the first n lines is inconsistent, indicating that the original formula is inconsistent. If the conjunction remains consistent for all n, the algorithm does not terminate, indicating that the original formula is consistent. The procedure is feasible for use with complex formulas and avoids the exponential growth associated with other methods. The paper also includes an example demonstrating the effectiveness of the algorithm, showing that it can successfully refute a formula that previously eluded a computer program. The method is compared to other approaches, such as truth-tables and disjunctive normal forms, which are less efficient for large n. The algorithm is described in detail, including the steps for generating quantifier-free lines and testing their consistency. The paper concludes with a note on the importance of finite axiomatizations for applying proof procedures to genuine mathematical problems.This paper presents a computational procedure for quantification theory, which is a method to determine whether a given formula in quantification theory is logically valid. The procedure is based on the idea of replacing existential quantifiers with function symbols, allowing for the generation of a sequence of quantifier-free lines. These lines are then tested for consistency using a set of rules that help eliminate one-literal clauses, apply the affirmative-negative rule, and eliminate atomic formulas. The algorithm terminates if the conjunction of the first n lines is inconsistent, indicating that the original formula is inconsistent. If the conjunction remains consistent for all n, the algorithm does not terminate, indicating that the original formula is consistent. The procedure is feasible for use with complex formulas and avoids the exponential growth associated with other methods. The paper also includes an example demonstrating the effectiveness of the algorithm, showing that it can successfully refute a formula that previously eluded a computer program. The method is compared to other approaches, such as truth-tables and disjunctive normal forms, which are less efficient for large n. The algorithm is described in detail, including the steps for generating quantifier-free lines and testing their consistency. The paper concludes with a note on the importance of finite axiomatizations for applying proof procedures to genuine mathematical problems.