The class TFNP, of NP search problems where all instances have solutions, appears not to have complete problems. However, TFNP contains various syntactic subclasses and important problems. We introduce a syntactic class of problems that contains these known subclasses, for the purpose of understanding and classifying TFNP problems. This class is defined in terms of the search for an error in a concisely-represented formal proof. Finally, the known complexity subclasses are based on existence theorems that hold for finite structures; from Herbrand's Theorem, we note that such theorems must apply specifically to finite structures, and not infinite ones.
@InProceedings{goldberg_et_al:LIPIcs.ITCS.2018.37, author = {Goldberg, Paul W. and Papadimitriou, Christos H.}, title = {{Towards a Unified Complexity Theory of Total Functions}}, booktitle = {9th Innovations in Theoretical Computer Science Conference (ITCS 2018)}, pages = {37:1--37:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-060-6}, ISSN = {1868-8969}, year = {2018}, volume = {94}, editor = {Karlin, Anna R.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2018.37}, URN = {urn:nbn:de:0030-drops-83403}, doi = {10.4230/LIPIcs.ITCS.2018.37}, annote = {Keywords: Computational complexity, first-order logic, proof system, NP search functions, TFNP} }
Feedback for Dagstuhl Publishing