DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click

HERE to register or log in.

# 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

# 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.

# Distribution Statement:

## APPROVED FOR PUBLIC RELEASE

#