A Semi-Decision Procedure for the Functional Calculus
Joyce Friedman · Journal of the ACM · 1963
AbstracLThis paper develops algorithms by which decision procedures for the functional calculus can be applied mechanically.Given any expression in Skolem normal form with prefix (3y~)(3y2) ... (3y,~,)(z~)(z~) ... (z,~) and matrix M, the algorithms lead to the construction of a nu~trix M* such that M D M* is valid and such that the expressions (3yl)(3y~) ... (3y,~)(zl)(z~) ... (z,~).Mand (3yl)(3y2) "" (3y,,,)(zl)(z~) -.. (z,~).M*areinterprovable.This procedure is thus a semi-decision procedure for the general Skolem case.For two special cases of this prefix, it is further proved that the method provides a solution to the decision problem in the sense that the given expression is a theorem if and only if M* is tautologous.These cases are ~1) a matrix M in which every elementary part contains at least one of the individual variables z~ , z~, .. • , z,~ or contains only one individual variable or contains both Yl and y2 and no other individual variables; and (2) a matrix M in which every elementary part contains at least one of the individual variables z~ , z2, .--,z,, or contains only one individual variable or contains all of y~, y2, '" , ym •