The Recursive Unsolvability of the Decision Problem for the Class of Definite Formulas.

Robert Di Paola

ResearchPublished 1968

A class of formulas of the first-order predicate calculus--the definite formulas--have recently been proposed as formal representations of "reasonable" questions to be processed by an actual data retrieval system known as the Relational Data File (see RM-5428-PR). It is shown in this study that the decision problem for the class of definite formulas is recursively unsolvable. Hence there is no algorithm that can be used to decide whether or not a given formula is definite. 12 pp. Ref

Document Details

  • Copyright: RAND Corporation
  • Availability: Web Only
  • Year: 1968
  • Pages: 12
  • Document Number: RM-5639-PR

Citation

Chicago Manual of Style

Di Paola, Robert, The Recursive Unsolvability of the Decision Problem for the Class of Definite Formulas. Santa Monica, CA: RAND Corporation, 1968. https://www.rand.org/pubs/research_memoranda/RM5639.html.
BibTeX RIS

This publication is part of the RAND research memorandum series. The research memorandum series, a product of RAND from 1948 to 1973, included working papers meant to report current results of RAND research to appropriate audiences.

This document and trademark(s) contained herein are protected by law. This representation of RAND intellectual property is provided for noncommercial use only. Unauthorized posting of this publication online is prohibited; linking directly to this product page is encouraged. Permission is required from RAND to reproduce, or reuse in another form, any of its research documents for commercial purposes. For information on reprint and reuse permissions, please visit www.rand.org/pubs/permissions.

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