Fluted formulas and the limits of decidability
Fluted formulas and the limits of decidability
复制标题
凹槽公式和可判定性的限制
DOI：
10.2307/2275678
复制
发表时间：
1996
影响因子：
0.6
通讯作者：
W. C. Purdy
中科院分区：
文献类型：
--
作者：
W. C. Purdy
在谓词演算中，变量提供了一种灵活的索引服务，它从谓词字母之前的可能参数中选择谓词字母的实际参数（在公式的解析中）。在选择过程中，可能的参数可以被置换、重复（使用多次）和跳过。如果这个服务被扣留，所以参数必须是紧接在前面的，按照它们出现的顺序，这个公式被称为凹槽。奎因证明了如果一个槽式公式只包含齐次合取（只包含等价的子公式），那么这个公式的可满足性是可判定的。它仍然是一个悬而未决的问题是否满足一个槽公式没有这个限制是可判定的。本文回答了这个问题。
Abstract In the predicate calculus, variables provide a flexible indexing service which selects the actual arguments to a predicate letter from among possible arguments that precede the predicate letter (in the parse of the formula). In the process of selection, the possible arguments can be permuted, repeated (used more than once), and skipped. If this service is withheld, so that arguments must be the immediately preceding ones, taken in the order in which they occur, the formula is said to be fluted. Quine showed that if a fluted formula contains only homogeneous conjunction (conjoins only subformulas of equal arity), then the satisfiability of the formula is decidable. It remained an open question whether the satisfiability of a fluted formula without this restriction is decidable. This paper answers that question.