The Solvability of the Decision Problem for Classes of Proper Formulas and Related Results

by Robert Di Paola

Download

Download eBook for Free

FormatFile SizeNotes
PDF file 1.2 MB

Use Adobe Acrobat Reader version 10 or higher for the best experience.

Purchase

Purchase Print Copy

 FormatList Price Price
Add to Cart Paperback43 pages $20.00 $16.00 20% Web Discount

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.

This report is part of the RAND Corporation report series. The report was a product of the RAND Corporation from 1948 to 1993 that represented the principal publication documenting and transmitting RAND's major research findings and final research.

The RAND Corporation is a nonprofit institution that helps improve policy and decisionmaking through research and analysis. RAND's publications do not necessarily reflect the opinions of its research clients and sponsors.