标题： 可重命名性测试到子句集类 显示英文标题

标题： Testing for Renamability to Classes of Clause Sets

摘要： 本文研究了测试子句集是否属于文献中已知类别的问题。 特别是，我们感兴趣的是通过重命名定义的类别：是否可以以某种方式重命名谓词，使得正文字和负文字满足某些条件？ 我们证明，对于如Horn或OCC1N这样的类别，此类重命名的存在性可以在多项式时间内判定，而对于类别PVD，同样的问题则是NP完全的。 决策过程基于超分辨率；如果存在重命名，可以从最终饱和的子句集中提取出来。 显示英文摘要

摘要： This paper investigates the problem of testing clause sets for membership in classes known from literature. In particular, we are interested in classes defined via renaming: Is it possible to rename the predicates in a way such that positive and negative literals satisfy certain conditions? We show that for classes like Horn or OCC1N, the existence of such renamings can be decided in polynomial time, whereas the same problem is NP-complete for class PVD. The decision procedures are based on hyper-resolution; if a renaming exists, it can be extracted from the final saturated clause set.