J'ai récemment commencé à lire beaucoup sur la complexité des preuves et j'ai vraiment apprécié ce que j'ai lu. J'aimerais vraiment en savoir plus à ce sujet, mais j'ai du mal à trouver du bon matériel pour les débutants. Quelqu'un pourrait-il recommander des notions de base?
cc.complexity-theory
lo.logic
proof-complexity
Yugioh Mishima
la source
la source
Réponses:
Cela dépend du type de niveau "débutant" que vous souhaitez avoir. Je ne pense pas qu'il existe un très bon texte de premier cycle sur la complexité des preuves (cela est probablement vrai pour la plupart des sous-domaines spécialisés en complexité). Mais pour les sources débutantes (niveau supérieur), je recommanderais quelque chose comme bien comprendre la limite exponentielle de base sur les réfutations de résolution du principe du pigeonhole (via des restrictions aléatoires, un compromis largeur-taille et une interpolation réalisable), et étendre à partir de cela pointer plus loin. Cela pourrait être réalisé (approximativement) comme suit:
Stasys Jukna, Extremal Combinatorics With Applications in Computer Science, 2001, Springer-Verlag, Section 4.8.
Eli Ben-sasson et Avi Wigderson, Short Proofs are Narrow - Resolution made Simple (2000), JACM.
P. Beame et T. Pitassi, Complexité de la preuve propositionnelle: passé, présent et futur, Tendances actuelles en informatique théorique: entrée dans le XXIe siècle (G. Paul, G. Rozenberg et A. Salomaa, éditeurs), World Scientific Publishing , 2001, p. 42--70.
Pavel Pudlák, Limites inférieures pour les épreuves de résolution et de plan de coupe et les calculs monotones, The Journal of Symbolic Logic, vol. 62 (1997), no. 3, pp. 981-998.
Vous pouvez également consulter le texte plus autonome et plus long:
Pour l' aspect plus logique de la complexité de la preuve, comme l'a suggéré Kaveh, vous pouvez commencer à lire les premiers chapitres de:
la source
Pour l'aspect plus algébrique de la complexité de la preuve, je recommande de commencer par le document d'enquête de Pitassi de 1996:
Pour un aperçu rapide, vous pouvez également consulter le chapitre 5 du livre Clote - Kranakis déjà mentionné par Iddo, qui a une section sur les systèmes de preuve algébriques.
Le premier document de recherche que je recommanderais de lire (à la fois parce qu'il est séminal et parce que c'est une lecture agréable) est le document dans lequel le système d'épreuve Groebner ou Polynomial Calculus a été introduit:
la source
Je trouve ces notes de cours introductives faciles à lire: Paul Beame's IAS Lectures
la source
L'enquête sur la complexité des preuves à usage général la plus récente et la plus récente est probablement celle de Nathan Segerlind:
Nathan Segerlind: La complexité des preuves propositionnelles. Bulletin of Symbolic Logic 13 (4): 417-481, 2007 ( http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps ).
Et maintenant, des avertissements pour deux self plugs éhontés…
Une enquête encore plus récente, mais plus étroitement centrée sur les questions concernant la taille des preuves, l'espace des preuves et les compromis taille-espace, est la suivante:
Jakob Nordström. Jeux de galets, complexité de la preuve et compromis temps-espace. Logical Methods in Computer Science, volume 9, numéro 3, article 15, septembre 2013 ( http://www.lmcs-online.org/ojs/viewarticle.php?id=674 ).
Il y a aussi quelques notes de cours d'un cours quelque peu récent que j'ai donné sur le "spectre bas de gamme" de la complexité de la preuve (c'est-à-dire des systèmes de preuve relativement faibles tels que la résolution, le calcul polynomial et les plans de coupe) et les connexions à la résolution SAT. Ces notes peuvent être trouvées sur http://www.csc.kth.se/~jakobn/teaching/proofcplx11/#scribe-notes (certaines sont toujours en cours mais celles qui sont disponibles devraient être en bon état).
la source