학술논문

Computer-Aided Verification of P/NP Proofs: A Survey and Discussion
Document Type
Periodical
Source
IEEE Access Access, IEEE. 12:13513-13524 2024
Subject
Aerospace
Bioengineering
Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Computing and Processing
Engineered Materials, Dielectrics and Plasmas
Engineering Profession
Fields, Waves and Electromagnetics
General Topics for Engineers
Geoscience
Nuclear Engineering
Photonics and Electrooptics
Power, Energy and Industry Applications
Robotics and Control Systems
Signal Processing and Analysis
Transportation
Surveys
Queueing analysis
Search problems
Fault diagnosis
Writing
Task analysis
Set theory
Design automation
Formal verification
P/NP question
proofs
barriers
relativization
proof assistants
Language
ISSN
2169-3536
Abstract
We survey a collection of proofs towards equality, inequality, or independence of the relation of P to NP. Since the problem has attracted much attention from experts, amateurs, and in-betweens, this work is intended as a pointer into directions to enable a “self-assessment” of ideas laid out by people interested in the problem. To this end, we identify the most popular approaches to proving equality, inequality, or independence. Since the latter category appears to be without any attempts to follow the necessary proof strategies, we devote a Section to an intuitive outline of how independence proofs would work. In the other cases of proving equality or inequality, known barriers like (affine) relativization, algebrization, and others are to be avoided. The most important and powerful technique available in this regard is a formalization of arguments in automated proof assistants. This allows an objective self-check of a proof before presenting it to the scientific community.