Jan 1, 1970
In connection with Rand's Relational Data File (RDF), a class of proper formulas has been proposed comprising those formalizations of questions to be processed by the RDF that are especially suitable for machine processing (discussed in R-511 and RM-5428). That the decision problem for several classes of proper formulas is solvable was shown in R-661. This report goes further and shows that the decision problem for the class lambda of proper formulas on the connectives negation, disjunction, conjunction, implication, and existential quantification is solvable. It follows that the decision problem for any class of proper formulas based on a subset of these connectives is solvable. Thus, for each of these classes, there is a mechanical decision procedure that determines whether an arbitrary formula is a member of the class. Also a representation theorem for the members of lambda is proven that reveals the reason for the existence of an algorithm that solves the decision problem for lambda.