RECURSIVE UNSOLVABILITY OF DECISION PROBLEM FOR CLASS OF DEFINITE FORMULAS

被引：24

作者：

DIPAOLA, RA

机构：

[1] The Rand Corporation, Santa Monica, California

来源：

JOURNAL OF THE ACM | 1969年 / 16卷 / 02期

关键词：

D O I：

10.1145/321510.321524

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：324 / &