ABSTRACT
Lower Predicate Calculus-1 decision procedure will be found much easier to apply in practice than the previous one, especially when reader have to deal with a Well-formed formula containing more than two predicate variables. A Well-formed formula is in the standard form for Decision Procedure II if it consists of a disjunction of quantified schemata, or a conjunction of such disjunctions; no quantifier is immediately preceded by ∃ occurs at most once in any disjunction. The only task, therefore, is to give rules for testing the validity of conjuncts in the standard form. If the Well-formed formula consists simply of a disjunction of quantified schemata reader regard it as a conjunct in a degenerate conjunction.
