Proving completeness by logic

被引:2
|
作者
Escoffier, B [1 ]
Paschos, VT [1 ]
机构
[1] Univ Paris 09, LAMSADE, F-75775 Paris 16, France
关键词
completeness; NP-completeness; min-NPO-completeness; reduction; SAT;
D O I
10.1080/00207160412331296625
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
We first give a proof of SAT 's NP-completeness based upon a syntactic characterization of NP given by Fagin in 1974. We illustrate the central part of our proof by giving examples of how two well-known problems, MAX INDEPENDENT SET and 3-COLORING , can be expressed in terms of CNF. This new proof is, in some sense, 'more constructive' than Cook's classical one, as we need only to show how an NP problem can be expressed in terms of a second-order logical formula. Next, inspired by Fagin's characterization, we propose a logical characterization for the class NP-optimization (NPO), i.e ., the class of optimization problems, the decision versions of which are in NP. Based upon this new characterization, we demonstrate the Min-NPO-completeness of MIN WSAT under strict reductions.
引用
收藏
页码:151 / 161
页数:11
相关论文
共 50 条
  • [41] Correctness and Completeness of Logic Programs
    Drabent, Wlodzimierz
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2016, 17 (03)
  • [42] On the completeness of propositional Hoare logic
    Kozen, D
    Tiuryn, J
    [J]. INFORMATION SCIENCES, 2001, 139 (3-4) : 187 - 195
  • [43] Completeness of global evaluation logic
    Goncharov, Sergey
    Schroeder, Lutz
    Mossakowski, Till
    [J]. MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2006, PROCEEDINGS, 2006, 4162 : 447 - 458
  • [44] On arithmetical completeness of the logic of proofs
    Iwata, Sohei
    Kurahashi, Taishi
    [J]. ANNALS OF PURE AND APPLIED LOGIC, 2019, 170 (02) : 163 - 179
  • [45] METHODOLOGY FOR PROVING THE TERMINATION OF LOGIC PROGRAMS
    WANG, B
    SHYAMASUNDAR, RK
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 480 : 214 - 227
  • [46] Proving quantified literals in Defeasible Logic
    Billington, D
    [J]. INFORMATION SCIENCES, 1999, 116 (01) : 55 - 81
  • [47] THEOREM-PROVING FOR INTENSIONAL LOGIC
    RAMSAY, A
    [J]. JOURNAL OF AUTOMATED REASONING, 1995, 14 (02) : 237 - 255
  • [48] Proving differential privacy in Hoare logic
    Barthe, Gilles
    Gaboardi, Marco
    Arias, Emilio Jesus Gallego
    Hsu, Justin
    Kunz, Cesar
    Strub, Pierre-Yves
    [J]. 2014 IEEE 27TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2014, : 411 - 424
  • [49] A METHODOLOGY FOR PROVING TERMINATION OF LOGIC PROGRAMS
    WANG, B
    SHYAMASUNDAR, RK
    [J]. JOURNAL OF LOGIC PROGRAMMING, 1994, 21 (01): : 1 - 30
  • [50] Proving failure in functional logic programs
    López-Fraguas, FJ
    Sánchez-Hernández, J
    [J]. COMPUTATIONAL LOGIC - CL 2000, 2000, 1861 : 179 - 193