2010/04/11 by Prabhu Manyem, Manyem, Prabhu
Computer Science · Mathematics · #Advanced Algebra and Logic #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #acm:03D15 #acm:68Q15 #acm:68Q17 #acm:68Q19 #cs.CC #cs.LO #math.LO #msc:03D15 #msc:68Q15 #msc:68Q17 #msc:68Q19
paper · pdf · doi:10.48550/arxiv.1004.1814
Manuscript withdrawn, because results are incorrect. If phi = phi_1 AND phi_2, and phi is a Horn formula, it does NOT mean that both phi_1 and phi_2 are Horn formulae. Furthermore, the cardinality constraint CANNOT be expressed as a universal Horn sentence in ESO (NOT even when the structure is ordered). Graedel's theorem is valid at a lower (machine) level, but probably NOT at a higher level
arxiv created 2010/10/02 · arxiv updated 2010/10/05
We show that the maximum clique problem (decision version) can be expressed in existential second order (ESO) logic, where the first order part is a Horn formula in second-order quantified predicates. Without ordering, the first order part is Π2 Horn; if ordering is used, then it is universal Horn (in which case, the second order variables can be determined in polynomial time). UPDATE: Manuscript withdrawn, because results are incorrect. If phi = phi1 AND phi2, and phi is a Horn formula, it does NOT mean that both phi1 and phi2 are Horn formulae. Furthermore, the cardinality constraint CANNOT be expressed as a universal Horn sentence in ESO (NOT even when the structure is ordered). Graedel's theorem is valid at a lower (machine) level, but probably NOT at a higher level.