An Attempt to Automate NP-Hardness Reductions via SO∃ Logic

Computer Science;descriptive complexity;mathematical discovery;second-order existential logic;theorem proving

Nijjar, Paul

University of Waterloo

关键词: Computer Science;    descriptive complexity;    mathematical discovery;    second-order existential logic;    theorem proving;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/1162/1/pnijjar2004.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

We explore the possibility of automating NP-hardness reductions. We motivate the problem from an artificial intelligence perspective, then propose the use of second-order existential (SO∃) logic as representation language for decision problems. Building upon the theoretical framework of J. Antonio Medina, we explore the possibility of implementing seven syntactic operators. Each operator transforms SO∃sentences in a way that preserves NP-completeness. We subsequently propose a program which implements these operators.We discuss a number of theoretical and practical barriers to this task. We prove that determining whether two SO∃ sentences are equivalent is as hard as GRAPH ISOMORPHISM, and prove that determining whether an arbitrary SO∃ sentence represents an NP-complete problem is undecidable.