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

1 April 1969

journal article
Published by Association for Computing Machinery (ACM) in Journal of the ACM

Vol. 16 (2) , 324-327
https://doi.org/10.1145/321510.321524

Abstract

A class of formulas of the first-order predicate calculus, the definite formulas has recently been proposed as the formal representation of the “reasonable” questions to put to a computer in the context of an actual data retrieval system, the Relational Data File of Levien and Maron. It is shown here that the decision problem for the class of definite formulas is recursively unsolvable. Hence there is no algorithm to decide whether a given formula is definite.

Keywords

RELATIONAL DATA FILE
DECISION PROBLEM
ACTUAL DATA RETRIEVAL SYSTEM
RECURSIVE UNSOLVABILITY
FORMAL REPRESENTATION
DEFINITE FORMULAS
RECURSIVELY UNSOLVABLE
FIRST-ORDER PREDICATE CALCULUS
DEFINITE FORMULA

This publication has 1 reference indexed in Scilit:

A computer system for inference execution and data retrieval
Communications of the ACM, 1967