Cover
article
Butiran eJurnal
Testing for Renamability to Classes of Clause Sets
HARVEST (oa) oa2085976
category EJURNAL event 2025-07-07 open_in_new Buka Pautan
Tarikh
2025-07-07
Pencipta
Brandl, Albert
Subjek
Logic in Computer Science; Computational Complexity
Jenis
text
Pengenal (Identifier)
http://arxiv.org/abs/2507.05044 In Proc. Int. Workshop on First-Order Theorem Proving (FTP'97), Maria Paola Bonacina and Ulrich Fuhrbach, editors. RISC-Linz Report Series No. 97-50, pages 34--39. Johannes Kepler Universität, Linz, Austria, 1997
Sumber Harvest
ARXIV
Deskripsi
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.