A Semi-Decision Procedure for the Functional Calculus

Abstract

AbstracL This 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