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

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. © 1969, ACM. All rights reserved.