Accession Number:

AD0737319

Title:

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

Descriptive Note:

Corporate Author:

RAND CORP SANTA MONICA CA

Personal Author(s):

Report Date:

1971-08-01

Pagination or Media Count:

45.0

Abstract:

In connection with Rands Relational Data File, 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. That the decision problem for several classes of porper formulas is solvable was shown in another report. The 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.

Subject Categories:

  • Linguistics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE