Gödel Prize
https://sigact.org/prizes/gödel.html
20年以上前、Gödel の論文を読もうという身内の企画があった。計算機の仕事で時間が取れずに参加できなかった。
企画そのものが空中分解したのかもしれない。
読んでないという負い目をおいながら仕事をしてきた。
Gödel Prizeがあることを知った。
何一つ読んでいない。これらをすべて読みながら、Gödel の論文も読もうと思った。
Gödel, Kurt (1931), “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.”, Monatshefte für Mathematik und Physik 38: 173–198, doi:10.1007/BF01700692.
英語じゃない。
Gödel, Kurt (1986), Feferman, Solomon, ed., Kurt Gödel: Collected Works: Volume I: Publications 1929-1936, Oxford University Press, pp. 144-195, ISBN 978-0-19-503964-1
Gödel, Kurt Meltzer, B.訳 (1992), On Formally
Undecidable Propositions of Principia Mathematica and Related Systems, Dover Books on Mathematics, Dover Publications, ISBN 978-0-486-66980-9
Gödel, Kurt; Hirzel, Martin (2000-11-27), “On formally undecidable propositions of Principia Mathematica and related systems I” (PDF), Boulder: 173-196
http://hirzels.com/martin/papers/canon00-goedel.pdf
Gödel, Kurt (2002), “Some metamathematical results on completeness and consistency, On formally undecidable propositions of Principia mathematica and related systems I, and On completeness and consistency”, in van Heijenoort, Jean, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Source Books in the History of the Sciences (Fourth Printing ed.), Harvard University Press, pp. 592-617, ISBN 978-0-674-32449-7
Gödel, Kurt (2004), “On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I.”, in Davis, Martin, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Dover Books on Mathematics, Courier Corporation, pp. 4-38, ISBN 978-0-486-43228-1
https://books.google.co.jp/books?id=qW8x7sQ4JXgC&pg=PA4&redir_esc=y#v=onepage&q&f=false
英訳をまず確認中。
ゲーデル賞の方は、2013, 2014, 2015年の詳細記事がリンク切れになっていた。人名等を元に、論文を探して記録する。
http://citeseerx.ist.psu.edu/
https://arxiv.org
http://researchgate.net
で検索。
- Requested としたのはhttp://researchgate.net で関係者に著作物送達依頼した文献。
論文が揃ったら単語帳を作る予定。Wikipediaの記述も直接PDF等のURLを記載していないものもある。
該当する論文がWEBで無償では見当たらず、原型がArxivに掲載のあるものもある。論文URLの後ろに年号を記載した。
https://en.wikipedia.org/wiki/Gödel_Prize#cite_note-36
原文と同一のものはWikipediaに加筆する予定。
#人名一覧
2020: Robin A. Moser and Gábor Tardos
2019: Irit Dinur
2018: Oded Regev
2017: Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith
2016: Stephen Brookes and Peter W. O’Hearn
2015: Daniel A. Spielman and Shang-Hua Teng
2014: Ronald Fagin, Amnon Lotem, and Moni Naor
2013: Antoine Joux, Dan Boneh, and Matthew K. Franklin
2012: Elias Koutsoupias, Christos H. Papadimitriou, Tim Roughgarden, Éva Tardos, Noam Nisan, and Amir Ronen
2011: Johan T. Håstad
2010: Sanjeev Arora and Joseph S. B. Mitchell
2009: Omer Reingold, Salil Vadhan, and Avi Wigderson
2008: Dan Spielman and Shang-Hua Teng
2007: Alexander A. Razborov and Steven Rudich
2006: Manindra Agrawal, Neeraj Kayal, and Nitin Saxena
2005: Noga Alon, Yossi Matias and Mario Szegedy
2004: Maurice Herlihy and Nir Shavit / Michael Saks and Fotios Zaharoglou
2003: Yoav Freund and Robert Schapire
2002: Géraud Sénizergues
2001: Sanjeev Arora, Uriel Feige, Shafi Goldwasser, Carsten Lund, László Lovász, Rajeev Motwani, Shmuel Safra, Madhu Sudan, and Mario Szegedy
2000: Moshe Vardi and Pierre Wolper
1999: Peter W. Shor
1998: Seinosuke Toda
1997: Joseph Halpern and Yoram Moses
1996: Mark Jerrum and Alistair Sinclair
1995: Neil Immerman and Róbert Szelepcsényi
1994: Johan Håstad
1993: László Babai, Shafi Goldwasser, Silvio Micali, Shlomo Moran, and Charles Rackoff
論文一覧
2020: Robin A. Moser and Gábor Tardos
The 2020 Gödel Prize is awarded to Robin A. Moser and Gábor Tardos for their algorithmic version of the Lovász Local Lemma in the paper:
“A constructive proof of the general Lovász Local Lemma,” Journal of the ACM 57(2): 11:1-11:15 (2010).
https://arxiv.org/pdf/0903.0544.pdf, 2009
References
[Knu69] Donald E. Knuth. The Art of Computer Programming, Vol. I, Addison Wesley, London, 1969, p. 396 (Exercise 11).
[EL75] Paul Erdo ̋s and La ́szl ́o Lov ́asz. Problems and results on 3-chromatic hypergraphs and some related ques- tions. In A. Hajnal, R. Rado and V.T. So ́s, editors, Infinite and Finite Sets (Colloq., Keszthely, 1973; dedicated to P. Erdo ̋s on his 60th birthday), volume II, pages 609–627. North-Holland, 1975.
[ES91] Paul Erdo ̋s and Joel Spencer. Lopsided Lova ́sz Local Lemma and Latin Transversals. Discrete Applied Mathematics, 30:151-154, 1991.
[Bec91] J ́oszef Beck. An Algorithmic Approach to the Lova ́sz Local Lemma. Random Structures and Algorithms, 2(4):343–365, 1991.
[Alo91] Noga Alon. A parallel algorithmic version of the local lemma. Random Structures and Algorithms, 2(4):367–378, 1991.
[KST93] JanKratochv ́ılandPetrSavicky ́andZsoltTuza.Onemoreoccurrenceofvariablesmakessatisfiability jump from trivial to NP-complete. SIAM J. Comput., Vol. 22, No. 1, pp. 203–210, 1993.
[MR98] Michael Molloy and Bruce Reed. Further Algorithmic Aspects of the Local Lemma. In Proceedings of the 30th Annual ACM Symposium on the Theory of Computing, pages 524–529, 1998.
[CS00] Artur Czumaj and Christian Scheideler. Coloring non-uniform hypergraphs: a new algorithmic approach to the general Lova ́sz local lemma. Symposium on Discrete Algorithms, 30–39, 2000.
[BKS03] Piotr Berman, Marek Karpinski, and Alexander D. Scott. Approximation hardness and satisfiability of bounded occurrence instances of SAT. Electronic Colloquium on Computational Complexity (ECCC), 10(022), 2003.
[Mos06] Robin A. Moser. On the Search for Solutions to Bounded Occurrence Instances of SAT. Not published. Semester Thesis, ETH Zu ̈rich. 2006.
[PT09] J ́anos Pach and G ́abor Tardos. Conflict-free colorings of graphs and hypergraphs. Manuscript, 2009.
[Sri08] Aravind Srinivasan. Improved algorithmic versions of the Lova ́sz Local Lemma. Proceedings of the nine- teenth annual ACM-SIAM symposium on Discrete algorithms (SODA), San Francisco, California, pp. 611–620, 2008.
[Wel08] Emo Welzl. Boolean Satisfiability - Combinatorics and Algorithms. Lecture notes, Version Fall 2008.
[Mos08] Robin A. Moser. Derandomizing the Lova ́sz Local Lemma more Effectively. Eprint, arXiv:0807.2120v2,
2008.
[Mos09] Robin A. Moser. A constructive proof of the Lova ́sz Local Lemma. Proceedings of the 41st annual ACM Symposium on Theory of Computing (STOC 2009), to appear. Available at arXiv:0810.4812v2, 2008.
####2019: Irit Dinur
https://sigact.org/prizes/gödel/citation2019.pdf
The 2019 Gödel Prize is awarded to Irit Dinur for her proof of the PCP Theorem in the paper:
The PCP theorem by gap amplification,
Journal of the ACM, Vol 54 (3), Article 12, 2007.
(preliminary version in the proceedings of the 38th Symposium on Theory of Computing, STOC 2006).
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=CC1C896ABF24E8D7EA957CD543AAACBB?doi=10.1.1.103.2644&rep=rep1&type=pdf
References
[1] S.Arora.Probabilisticcheckingofproofsandthehardnessofapproximationproblems.PhDthesis, U.C. Berkeley, 1994. Available via anonymous ftp as Princeton TR94-476.
[2] S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof verification and intractability of approximation problems. J. ACM, 45(3):501–555, 1998.
[3] S. Arora and S. Safra. Probabilistic checking of proofs: A new characterization of NP. J. ACM, 45(1):70–122, 1998.
[4] L.Babai.Tradinggrouptheoryforrandomness.InProc.17thACMSymp.onTheoryofComputing, pages 421–429, 1985.
[5] L. Babai, L. Fortnow, and C. Lund. Non-deterministic exponential time has two-prover interactive protocols. Computational Complexity, 1:3–40, 1991.
[6] M. Ben-or, S. Goldwasser, J. Kilian, and A. Wigderson. Multi prover interactive proofs: How to remove intractability assumptions. In Proc. 20th ACM Symp. on Theory of Computing, pages 113–131, 1988.
[7] E. Ben-Sasson, O. Goldreich, P. Harsha, M. Sudan, and S. Vadhan. Robust PCPs of proximity, shorter PCPs and applications to coding. In Proc. 36th ACM Symp. on Theory of Computing, 2004.
[8] E. Ben-Sasson and M. Sudan. Robust locally testable codes and products of codes. In RANDOM: International Workshop on Randomization and Approximation Techniques in Computer Science, 2004.
[9] E. Ben-Sasson, M. Sudan, S. P. Vadhan, and A. Wigderson. Randomness-efficient low degree tests and short PCPs via epsilon-biased sets. In Proc. 35th ACM Symp. on Theory of Computing, pages 612–621, 2003.
[10] A. Bogdanov. Gap amplification fails below 1/2. Comment on ECCC TR05-046, can be found at http://eccc.uni-trier.de/eccc-reports/2005/TR05-046/commt01.pdf, 2005.
[11] I. Dinur and O. Reingold. Assignment testers: Towards combinatorial proofs of the PCP theorem. In Proceedings of the 45th Symposium on Foundations of Computer Science (FOCS), 2004.
[12] U. Feige, S. Goldwasser, L. Lova ́sz, S. Safra, and M. Szegedy. Approximating clique is almost NP-complete. Journal of the ACM, 43(2):268–292, 1996.
[13] U. Feige and J. Kilian. Impossibility results for recycling random bits in two-prover proof systems. In Proc. 27th ACM Symp. on Theory of Computing, pages 457–468, 1995.
[14] L. Fortnow, J. Rompel, and M. Sipser. On the power of multi-prover interactive protocols. Theo- retical Computer Science, 134(2):545–557, 1994.
35
[15] E. Friedgut, G. Kalai, and A. Naor. Boolean functions whose fourier transform is concentrated on the first two levels. Adv. in Applied Math., 29:427–437, 2002.
[16] O. Goldreich. A sample of samplers a computational perspective on sampling. Electronic Collo- quium on Computational Complexity TR97-020, 1997.
[17] O.GoldreichandS.Safra.AcombinatorialconsistencylemmawithapplicationtoprovingthePCP theorem. In RANDOM: International Workshop on Randomization and Approximation Techniques in Computer Science. LNCS, 1997.
[18] O. Goldreich and M. Sudan. Locally testable codes and PCPs of almost-linear length. In Proc. 43rd IEEE Symp. on Foundations of Computer Science, pages 13–22, 2002.
[19] O. Goldreich and A. Wigderson. Tiny families of functions with random properties: A qualitysize tradeoff for hashing. Journal of Random structures and Algorithms, 11(4):315–343, 1997.
[20] S. Goldwasser, S. Micali, and C. Rackoff. The knowledge complexity of interactive proofs. SIAM Journal on Computing, 18:186–208, 1989.
[21] P. Harsha and M. Sudan. Small PCPs with low query complexity. In STACS, pages 327–338, 2001.
[22] J. Ha ̊stad. Some optimal inapproximability results. Journal of ACM, 48:798–859, 2001.
[23] N. Linial and A. Wigderson. Expander graphs and their applications. Lecture notes of a course: http://www.math.ias.edu/ boaz/ExpanderCourse/, 2003.
[24] C. Lund, L. Fortnow, H. Karloff, and N. Nisan. Algebraic methods for interactive proof systems. Journal of the ACM, 39(4):859–868, October 1992.
[25] R. O’Donnell and V. Guruswami. Lecture notes from a course on: the PCP theorem and hardness of approximation. 2005.
[26] C. Papadimitriou and M. Yannakakis. Optimization, approximation and complexity classes. Jour- nal of Computer and System Sciences, 43:425–440, 1991.
[27] A. Polishchuk and D. Spielman. Nearly linear size holographic proofs. In Proc. 26th ACM Symp. on Theory of Computing, pages 194–203, 1994.
[28] J. Radhakrishnan. Private communication. 2005.
[29] R. Raz. A parallel repetition theorem. SIAM Journal on Computing, 27(3):763–803, June 1998.
[30] O. Reingold. Undirected st-connectivity in log-space. In Proc. 37th ACM Symp. on Theory of Computing, 2005.
[31] O. Reingold, S. Vadhan, and A. Wigderson. Entropy waves, the zig-zag graph product, and new constant-degree expanders and extractors. Annals of Mathematics, 155(1):157–187, 2002.
[32] A. Shamir. IP = PSPACE. Journal of the ACM, 39(4):869–877, October 1992. Prelim. version in 1990 FOCS, pages 11–15.
[33] M. Sipser and D. A. Spielman. Expander codes. IEEE Trans. Inform. Theory, 42(6, part 1):1710– 1722, 1996. Codes and complexity.
2018: Oded Regev
The 2018 Gödel Prize is awarded to Professor Oded Regev for his paper:
On lattices, learning with errors, random linear codes, and cryptography Journal of the ACM, volume 56, issue 6, 2009 (preliminary version in the 37th annual Symposium on Theory of Computing, STOC 2005.)
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.215.3543&rep=rep1&type=pdf
2017: Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith
The 2017 Gödel Prize is awarded to Cynthia Dwork, Frank McSherry, Kobbi Nissim and Adam Smith for their work on Differential Privacy in the paper:
Calibrating Noise to Sensitivity in Private Data Analysis, Journal of Privacy and Confidentiality, Volume 7, Issue 3, 2016 (preliminary version in Theory of Cryptography, TCC 2006).
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=CC1C896ABF24E8D7EA957CD543AAACBB?doi=10.1.1.131.9267&rep=rep1&type=pdf
(Calibrating Data to Sensitivity in Private Data Analysis https://arxiv.org/pdf/1203.3453.pdf, 2014)
References
[1] N. R. Adam and J. C. Wortmann. Security-control methods for statistical data- bases: a comparative study. ACM Computing Surveys, 25(4), December 1989.
[2] Dakshi Agrawal and Charu C. Aggarwal. On the design and quantification of
privacy preserving data mining algorithms. In Proceedings of the Twentieth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Sys- tems. ACM, 2001.
[3] Rakesh Agrawal and Ramakrishnan Srikant. Privacy-preserving data mining. In Weidong Chen, Jeffrey F. Naughton, and Philip A. Bernstein, editors, SIGMOD Conference, pages 439–450. ACM, 2000.
[4] EliBen-Sasson,PrahladhHarsha,andSofyaRaskhodnikova.Some3cnfproperties are hard to test. In STOC, pages 345–354. ACM, 2003.
[5] Web page for the Bertinoro CS-Statistics workshop on privacy and confidentiality. Available from http://www.stat.cmu.edu/~hwainer, July 2005.
[6] Avrim Blum, Cynthia Dwork, Frank McSherry, and Kobbi Nissim. Practical privacy: The sulq framework. In PODS, 2005.
[7] Shuchi Chawla, Cynthia Dwork, Frank McSherry, Adam Smith, and Hoeteck Wee. Toward privacy in public databases. In Theory of Cryptography Confer- ence (TCC), pages 363–385, 2005.
[8] Shuchi Chawla, Cynthia Dwork, Frank McSherry, and Kunal Talwar. On the utility of privacy-preserving histograms. In 21st Conference on Uncertainty in Artificial Intelligence (UAI), 2005.
[9] Dorothy E. Denning. Secure statistical databases with random sample queries. ACM Transactions on Database Systems, 5(3):291–315, September 1980.
[10] Irit Dinur and Kobbi Nissim. Revealing information while preserving privacy. In
Proceedings of the Twenty-Second ACM SIGACT-SIGMOD-SIGART Symposium
on Principles of Database Systems, pages 202–210, 2003.
[11] Cynthia Dwork and Kobbi Nissim. Privacy-preserving datamining on vertically
partitioned databases. In Matthew K. Franklin, editor, CRYPTO, volume 3152
of Lecture Notes in Computer Science, pages 528–544. Springer, 2004.
[12] AlexandreV.Evfimievski,JohannesGehrke,andRamakrishnanSrikant.Limiting privacy breaches in privacy preserving data mining. In Proceedings of the Twenty- Second ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database
Systems, pages 211–222, 2003.
18 Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith
[13] Shafi Goldwasser and Silvio Micali. Probabilistic encryption. Journal of Computer and System Sciences, 28(2):270–299, April 1984.
[14] Gina Roque. Masking microdata with mixtures of normal distributions. University of California, Riverside, 2000. Doctoral Dissertation.
[15] Latanya Sweeney. k-anonymity: A model for protecting privacy. International Journal on Uncertainty, Fuzziness and Knowledge-based Systems, 10(5):557–570, 2002.
####2016: Stephen Brookes and Peter W. O’Hearn
https://eatcs.org/index.php/component/content/article/1-news/2280-2016-godel-prize
The 2016 Gödel Prize is awarded to Stephen Brookes and Peter W. O'Hearn for their invention of Concurrent Separation Logic, as described in the following two papers:
S. Brookes, A Semantics for Concurrent Separation Logic. Theoretical Computer Science 375(1-3): 227-270 (2007)
https://www.cs.cmu.edu/~brookes/papers/seplogicrevisedfinal.pdf
References
[1] G. Andrews. Concurrent Programming: Principles and Practice.
Benjamin/Cummings, 1991.
[2] L. Birkedal, N. Torp-Smith, and J.C. Reynolds. Local Reasoning about a Copying Garbage Collector. Proc. POPL Conference, Venice, pp. 220- 231, January 2004.
[3] R. Bornat, C. Calcagno, P. W. O’Hearn, and M. Parkinson. Permission accounting in separation logic. Proc. POPL 2005, pp. 59-70.
[4] R. Bornat, C. Calcagno, and P. W. O’Hearn. Local reasoning, separa- tion, and aliasing. Proc. 2nd ACM/SIGPLAN Workshop on Semantics, Program Analysis, and Computing Environments for Memory Manage- ment, SPACE 2004, January 2004.
[5] C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe program- ming: Preventing data races and deadlocks. Proc. OOPSLA 2002: 211- 230, 2002.
[6] J. Boyland. Checking interference with fractional permissions. Proc. 10th Symposium on Static Analysis, R. Cousot, editor. Springer LNCS vol. 2694, pp. 55-72, 2003.
[7] P. Brinch Hansen. Structured multiprogramming. Comm. ACM, 15(7):574-578, July 1972.
[8] P. Brinch Hansen. Concurrent programming concepts. ACM Computing Surveys 5(4):223-245, December 1973.
[9] P. Brinch Hansen. Operating System Principles. Prentice Hall, 1973.
70
[10] P. Brinch Hansen. The programming language Concurrent Pascal. IEEE Trans. on Software Engr, SE-1(2):196-206. June 1975.
[11] S. Brookes. A semantics for concurrent separation logic. Invited paper, CONCUR 2004, London. August 2004. Springer LNCS 3170.
[12] S. Brookes, Traces, pomsets, fairness and full abstraction for communi- cating processes. Proc. CONCUR 2002, Brno. Springer LNCS vol. 2421, pp. 466-482. August 2002.
[13] S. Brookes. The essence of Parallel Algol. Proc. 11th Symposium on Logic in Computer Science, IEEE Computer Society Press (1996), pp. 164–173. Journal version: Inf. Comp. 179(1): 118-149, 2002.
[14] S. Brookes. Communicating Parallel Processes: Deconstructing CSP. In: Millenium Perspectives in Computer Science, Proc. 1999 Oxford- Microsoft Symposium in honour of Sir Tony Hoare. Palgrave, 2000.
[15] S. Brookes. Idealized CSP: Combining Procedures with Communicating Processes, 13th MFPS Conference, Pittsburgh, March 1997. Electronic Notes in Theoretical Computer Science 6, Elsevier, 1997.
[16] S. Brookes. Full abstraction for a shared-variable parallel language. Proc. 8th IEEE Symposium on Logic in Computer Science, IEEE Com- puter Society Press (1993), 98–109. Journal version in: Inf. Comp., vol 127(2):145-163, Academic Press, June 1996.
[17] S. Brookes and A.W. Roscoe. Deadlock Analysis in networks of commu- nicating processes. Distributed Computing 4:209-230, 1991.
[18] E. W. Dijkstra. Hierarchical ordering of sequential processes. Acta In- formatica, 1(2):115-138, 1972.
[19] E. W. Dijkstra. The structure of the “THE” multiprogramming system, Comm. ACM 11(5):341-346, May 1968.
[20] E. W. Dijkstra. Cooperating sequential processes. In: Programming Languages, F. Genuys (editor), pp. 43-112. Academic Press, 1968.
[21] C.A.R. Hoare. A structured paging system. Computer Journal 16(3):209- 215, 1973.
71
[22] C.A.R. Hoare. Parallel programming: an axiomatic approach. Computer Languages 1, 151-160, 1975.
[23] C.A.R. Hoare, Monitors: An operating system structuring concept, CACM 17(10): 549-557, October 1974.
[24] C.A.R. Hoare, Towards a Theory of Parallel Programming. In Oper- ating Systems Techniques, Hoare and Perrot, editors, pp. 61-71, Academic Press, 1972.
[25] S. Isthiaq and P. W. O’Hearn. BI as an assertion language for mutable data structures. Proc. 28th POPL conference, pp. 36-49, London, Jan- uary 2001.
[26] C.B. Jones. Development Methods for Computer Programs including a Notion of Interference. Ph.D. thesis, Oxford University, June 1981. Tech- nical Monograph PRG-25, Programming Reseacrh Group, Oxford Uni- versity Computing Laboratory.
[27] C.B. Jones. Specification and design of (parallel) programs. Proc. IFIP Conference, 1983.
[28] J. Misra and M. Chandy. Proofs of networks of processes. IEEE Trans- actions on Software Engineering, 7:417-426 (1981).
[29] H.C. Lauer. Correctness in operating systems. Ph. D. thesis, Carnegie Mellon University, 1973.
[30] P. W. O’Hearn. Notes on separation logic for shared-variable concur- rency. Unpublished manuscript, January 2002.
[31] P.W. O’Hearn. Resources, Concurrency, and Local Reasoning. Invited paper, CONCUR 2004, London, August 2004. Springer LNCS 3170. Complete paper in this volume.
[32] P.W. O’Hearn, H. Yang, and J.C. Reynolds. Separation and Information Hiding. Proc. 31st POPL conference, pp 268-280, Venice. ACM Press, January 2004.
[33] P.W. O’Hearn, J.C. Reynolds, and H. Yang. Local reasoning about pro- grams that alter data structures. Proc. 15th Conference of the European
72
Association for Computer Science Logic, Springer LNCS, vol. 2142, pp 1-19, 2001.
[34] P. W. O’Hearn and D. J. Pym. The logic of bunched implications. Bul- letin of Symbolic Logic, 5(2):215-244, June 1999.
[35] S. Owicki and L. Lamport, Proving liveness properties of concurrent programs, ACM TOPLAS, 4(3): 455-495, July 1982.
[36] S. Owicki and D. Gries. An axiomatic proof technique for parallel pro- grams I. Acta Informatica, 6:319-340, 1976.
[37] S. Owicki and D. Gries, Verifying properties of parallel programs: An axiomatic approach, Comm. ACM. 19(5):279-285, 1976.
[38] D. Park, On the semantics of fair parallelism. In: Abstract Software Specifications, Springer-Verlag LNCS vol. 86, 504–526, 1979.
[39] A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13(1):45-60, 1981.
[40] J. C. Reynolds. Intuitionistic reasoning about shared mutable data struc- ture. In J.Davies, A. W. Roscoe, and J. Woodcock, eds., Millenium per- spectives in computer science, pp. 303-321. Palgrave, 2000.
[41] J.C. Reynolds, Separation logic: a logic for shared mutable data struc- tures, Invited paper. Proc. 17th IEEE Conference on Logic in Computer Science, LICS 2002, pp. 55-74. IEEE Computer Society, 2002.
[42] J. C. Reynolds. Lecture notes on separation logic (15-819A3), chapter 8, page 178. Department of Computer Science, Carnegie-Mellon University, Spring 2003. Revised May 23, 2003.
[43] J. C. Reynolds, Towards a grainless semantics for shared-variable con- currency. Slides from Invited Lecture, 31st POPL concerence, Venice, January 2004.
[44] H. Yang. An example of local reasoning in BI pointer logic: The Schorr- Waite graph marking algorithm. Proc. SPACE 2001 Workshop on Se- mantics, Program Analysis and Computing Environments for Memory Management, pp. 41-68. IT University of Copenhagen, 2001.
P. W. O’Hearn, Resources, Concurrency, and Local Reasoning. Theoretical Computer Science 375(1-3): 271-307 (2007)
http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf
References
[1] G. Andrews. Concurrent programming: principles and practice. Benjamin/Cummings, 1991.
[2] A. Banerjee and D. A. Naumann. Representation independence, confinement and access con- trol. In 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002.
[3] J. Berdine, C. Calcagno, and P. O’Hearn. A decidable fragment of separation logic. In Proceedings of FSTTCS, pages 97–109, 2004. LNCS 3328.
[4] R. Bornat. Variables as resource in Separation Logic. Proceedings of the 21st Conference on Mathematical Foundations of Computer Science, Springer LNCS, to appear, 2005.
[5] R. Bornat, C. Calcagno, P. O’Hearn, and M. Parkinson. Permission accounting in separation logic. In 32nd POPL, pages 59–70, 2005.
[6] C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. OOPSLA, 2002.
[7] J. Boyland. Checking interference with fractional permissions. In R. Cousot, editor, Static Analysis: 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 55–72, Berlin, Heidelberg, New York, 2003. Springer.
[8] P. Brinch Hansen. The nucleus of a multiprogramming system. Comm. ACM, 13(4):238–250, 1970.
[9] P. Brinch Hansen. Structured multiprogramming. Comm. ACM, 15(7):574–578, 1972. Reprinted in [11].
[10] P. Brinch Hansen. Operating System Principles. Prentice Hall, 1973.
[11] P. Brinch Hansen, editor. The Origin of Concurrent Programming. Springer-Verlag, 2002.
[12] S. D. Brookes. A semantics for concurrent separation logic. Theoretical Computer Science, this Volume. Preliminary version appeared in Proceedings of the 15th CONCUR (2004), LNCS 3170, pp16-34., 2005.
[13] L. Caires. Behavioral and spatial observations in a logic for the pi-calculus. Proceedings of FOSSACS, LNCS 2987, 2004.
[14] L. Cardelli and L Caires. A spatial logic for concurrency. In 4th International Symposium on Theoretical Aspects of Computer Science, LNCS 2255:1–37, Springer, 2001.
[15] L. Cardelli and A. D. Gordon. Anytime, anywhere. Modal logics for mobile ambients. In 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 365–377, 2000.
[16] D. Clarke, J. Noble, and J. Potter. Simple ownership types for object containment. Proceedings of the 15th European Conference on Object-Oriented Programming, pages 53-76, Springer LNCS 2072, 2001.
[17] E. W. Dijkstra. Cooperating sequential processes. In F. Genuys, editor, Programming Lan- guages, pages 43–112. Academic Press, 1968. Reprinted in [11].
[18] E. W. Dijkstra. Hierarchical ordering of sequential processes. Acta Informatica, 1 2:115–138, October 1971. Reprinted in [11].
[19] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
[20] A. N. Habermann. Synchronization of communicating processes. Comm. ACM, 15(3):171–
176, 1972.
[21] T. Harris and K. Fraser. Language support for lightweight transactions. In Proceedings of
OOPSLA, pages 388–402, 2003.
[22] C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In E. Engler, editor, Symposium on the Semantics of Algebraic Languages, pages 102–116. Springer, 1971. Lecture Notes in Math. 188.
[23] C. A. R. Hoare. Towards a theory of parallel programming. In Hoare and Perrot, editors, Operating Systems Techniques. Academic Press, 1972. Reprinted in [11].
[24] C. A. R. Hoare. Monitors: An operating system structuring concept. Comm. ACM, 17(10):549–557, 1974. Reprinted in [11].
[25] C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[26] C. B. Jones. Specification and design of (parallel) programs. IFIP Conference, 1983.
[27] C. B. Jones. Interference revisited. In J.E. Nicholls, editor, Proceedings of the 5th Annual Z User Meeting: Z User Workshop, Oxford, UK, pages 58–73, 1991. Springer-Verlag.
[28] C. B. Jones. Wanted: A compositional approach to concurrency. In A. McIver and C. Morgan, editors, Programming Methodology, pages 1–15, 2003. Springer-Verlag.
[29] H. T. Kung and P. L. Lehman. Concurrent manipulation of binary search trees. ACM Trans. Database Systems ,5, 354-382, 2005.
[30] M. Michael. Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst., 15(6):491–504, 2004.
[31] R. Milner. The polyadic pi-calculus: a tutorial. In F. L. Bauer, W. Brauer, and H. Schwicht- enberg, editors, Logic and Algebra of Specification, pages 203–246. Springer-Verlag, 1993.
[32] J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Trans. Software Eng., 7(4):417–426, 1981.
[33] D. A. Naumann and M. Barnett. Towards imperative modules: Reasoning about invariants and sharing of mutable state. Manuscript, 2 February, 2004.
[34] P. O’Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data struc- tures. In Proceedings of 15th Annual Conference of the European Association for Computer Science Logic, LNCS, pages 1–19. Springer-Verlag, 2001.
[35] P. W. O’Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, June 99.
[36] P. W. O’Hearn and R. D. Tennent, editors. Algol-like Languages. Two volumes, Birkhauser, Boston, 1997.
[37] P. W. O’Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 268– 280, Venice, January 2004.
[38] S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, (19):319–340, 1976.
[39] S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. Comm. ACM, 19(5):279–285, 1976.
[40] A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13(1), 45–60, 1981.
[41] D.J. Pym and C. Tofts. A calculus and logic of resources and processes. HP Labs Technical Report HPL-2004-170, 2004.
[42] J. C. Reynolds. Syntactic control of interference. In 5th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 39–46, Tucson, Arizona, January 1978. ACM, New York. Also in [36], vol 1.
[43] J. C. Reynolds. Separation logic: a logic for shared mutable data structures. Invited Paper, Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pages 55-74, 2002.
[44] J. C. Reynolds. Shared variable concurrency. Chapter 6 of class notes from CS-819 C, CMU, 15 March, 2002.
[45] J. C. Reynolds. Towards a grainless semantics for shared variable concurrency. In Proceedings of FSTTCS, pages 35–48, 2004. LNCS 3328.
[46] F. Smith, D. Walker, and G. Morrisett. Alias types. Proceedings of ESOP’99.
2015: Daniel A. Spielman and Shang-Hua Teng
The 2015 Gödel Prize is awarded to Daniel A. Spielman and Shang-Hua Teng for their series of papers on nearly-linear-time Laplacian solvers:
Spectral sparsification of graphs. SIAM J. Computing 40:981-1025, 2011.
https://arxiv.org/pdf/0808.4134.pdf
References
[ACL06] Reid Andersen, Fan Chung, and Kevin Lang. Local graph partitioning using pager- ank vectors. Proceedings of the 47th Annual Symposium on Foundations of Computer Science, pages 475–486, 2006.
[AM01] Dimitris Achlioptas and Frank McSherry. Fast computation of low rank matrix approximations. In Proceedings of the 33rd Annual ACM Symposium on Theory of Computing, pages 611–618, 2001.
[AP09] Reid Andersen and Yuval Peres. Finding sparse cuts locally using evolving sets. In STOC ’09: Proceedings of the 41st annual ACM symposium on Theory of computing, pages 235–244, New York, NY, USA, 2009. ACM.
[Axe85] O. Axelsson. A survey of preconditioned iterative methods for linear systems of algebraic equations. BIT Numerical Mathematics, 25(1):165–187, March 1985.
[BGH+06] M. Bern, J. Gilbert, B. Hendrickson, N. Nguyen, and S. Toledo. Support-graph preconditioners. SIAM J. Matrix Anal. & Appl, 27(4):930–951, 2006.
[BH03] Erik G. Boman and Bruce Hendrickson. Support theory for preconditioning. SIAM Journal on Matrix Analysis and Applications, 25(3):694–717, 2003.
[BK96]
[Bol98] [BSS09]
[Che70] [Che89] [Chu97] [DR98] [DS91] [FK81] [GR01] [KMP10] [KVV04] [LPS88]
Andra ́s A. Benczu ́r and David R. Karger. Approximating s-t minimum cuts in O(n2) time. In Proceedings of The Twenty-Eighth Annual ACM Symposium On The Theory Of Computing (STOC ’96), pages 47–55, May 1996.
B ́ela Bollob ́as. Modern graph theory. Springer-Verlag, New York, 1998.
Joshua D. Batson, Daniel A. Spielman, and Nikhil Srivastava. Twice-Ramanujan sparsifiers. In Proceedings of the 41st Annual ACM Symposium on Theory of com- puting, pages 255–262, 2009.
J. Cheeger. A lower bound for smallest eigenvalue of laplacian. In Problems in Analysis, pages 195–199, In R.C. Gunning editor,, Princeton University Press, 1970.
Paul Chew. There are planar graphs almost as good as the complete graph. J. Comput. Syst. Sci., 39:205–219, 1989.
Fan R. K. Chung. Spectral Graph Theory. CBMS Regional Conference Series in Mathematics. American Mathematical Society, 1997.
Devdatt Dubhashi and Desh Ranjan. Balls and bins: a study in negative dependence. Random Structures and Algorithms, 13(2):99–124, 1998.
Persi Diaconis and Daniel Stroock. Geometric bounds for eigenvalues of markov chains. The Annals of Applied Probability, 1(1):36–61, 1991.
Z. Fu ̈redi and J. Komlo ́s. The eigenvalues of random symmetric matrices. Combi- natorica, 1(3):233–241, 1981.
Chris Godsil and Gordon Royle. Algebraic Graph Theory. Graduate Texts in Math- ematics. Springer, 2001.
Ioannis Koutis, Gary L. Miller, and Richard Peng. Approaching optimality for solving sdd systems. March 2010. Available at http://arxiv.org/abs/1003.2958v1.
Ravi Kannan, Santosh Vempala, and Adrian Vetta. On clusterings: Good, bad and spectral. J. ACM, 51(3):497–515, 2004.
A. Lubotzky, R. Phillips, and P. Sarnak. Ramanujan graphs. Combinatorica, 8(3):261–277, 1988.
[Mar88] G. A. Margulis. Explicit group theoretical constructions of combinatorial schemes and their application to the design of expanders and concentrators. Problems of Information Transmission, 24(1):39–46, July 1988.
[Moh91] Bojan Mohar. The Laplacian spectrum of graphs. In Graph Theory, Combinatorics, and Applications, pages 871–898. Wiley, 1991.
[Rag88] Prabhakar Raghavan. Probabilistic construction of deterministic algorithms: Ap- proximating packing integer programs. J. Comput. Syst. Sci., 37:130–143, 1988.
[SJ89] Alistair Sinclair and Mark Jerrum. Approximate counting, uniform generation and rapidly mixing Markov chains. Information and Computation, 82(1):93–133, July 1989.
[SS08] Daniel A. Spielman and Nikhil Srivastava. Graph sparsification by effective resis- tances. In Proceedings of the 40th annual ACM Symposium on Theory of Computing, pages 563–568, 2008.
[ST04] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems. In Proceedings of the thirty-sixth annual ACM Symposium on Theory of Computing, pages 81–90, 2004. Full version available at http://arxiv.org/abs/cs.DS/0310051.
[ST08a] Daniel A. Spielman and Shang-Hua Teng. A local clustering algorithm for mas- sive graphs and its application to nearly-linear time graph partitioning. CoRR, abs/0809.3232, 2008. Available at http://arxiv.org/abs/0809.3232. Submitted to SICOMP.
[ST08b] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for pre- conditioning and solving symmetric, diagonally dominant linear systems. CoRR, abs/cs/0607105, 2008. Available at http://www.arxiv.org/abs/cs.NA/0607105. Submitted to SIMAX.
[Tar75] R. E. Tarjan. Efficiency of a good but not linear set union algorithm. Journal of the ACM, 22(2):448–501, 1975.
[TB97] L. N. Trefethen and D. Bau. Numerical Linear Algebra. SIAM, Philadelphia, PA, 1997.
[Tre05] Lucan Trevisan. Approximation algorithms for unique games. Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science, pages 197–205, Oct. 2005.
[Vu07] Van Vu. Spectral norm of random matrices. Combinatorica, 27(6):721–736, 2007.
A local clustering algorithm for massive graphs and its application to nearly linear time
graph partitioning. SIAM J. Computing 42:1-26, 2013.
https://arxiv.org/pdf/0809.3232.pdf
References
[ABC+ 07] Reid Andersen, Christian Borgs, Jennifer T. Chayes, John E. Hopcraft, Vahab S. Mirrokni, and Shang-Hua Teng. Local computation of pagerank contributions. In Anthony Bonato and Fan R. K. Chung, editors, WAW, volume 4863 of Lecture Notes in Computer Science, pages 150–165. Springer, 2007.
[ACL06] Reid Andersen, Fan Chung, and Kevin Lang. Local graph partitioning using pager- ank vectors. Proceedings: 47th Annual Symposium on Foundations of Computer Science, pages 475–486, 2006.
[ACL07] Reid Andersen, Fan R. K. Chung, and Kevin J. Lang. Local partitioning for directed graphs using pagerank. In Anthony Bonato and Fan R. K. Chung, editors, WAW, volume 4863 of Lecture Notes in Computer Science, pages 166–178. Springer, 2007.
[AHK04] Sanjeev Arora, Elad Hazan, and Satyen Kale. 0(sqrt (log n)) approximation to Sparsest Cut in ̃o(n2) time. In FOCS: IEEE Symposium on Foundations of Com- puter Science (FOCS), pages 238–247, 2004.
[AK07] Sanjeev Arora and Satyen Kale. A combinatorial, primal-dual approach to semidef- inite programs. In STOC ’07: Proceedings of the thirty-ninth annual ACM sympo- sium on Theory of computing, pages 227–236, New York, NY, USA, 2007. ACM.
[And08] Reid Andersen. A local algorithm for finding dense subgraphs. In Proceedings of the Nineteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2008, San Francisco, California, USA, January 20-22, 2008, pages 1003–1009. SIAM, 2008.
[ARV04] Sanjeev Arora, Satish Rao, and Umesh Vazirani. Expander flows, geometric embed- dings and graph partitioning. In STOC ’04: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing, pages 222–231, New York, NY, USA, 2004. ACM.
[Cor05] Intel Corporation. Morre’s law. ftp://download.intel.com/museum/Moores Law/Printed Mater 2005.
[GS05] A. Gulli and A. Signorini. The indexable web is more than 11.5 billion pages. In
WWW ’05: Special interest tracks and posters of the 14th international conference on World Wide Web, pages 902–903. ACM, 2005.
[KRV06] Rohit Khandekar, Satish Rao, and Umesh Vazirani. Graph partitioning using sin- gle commodity flows. In STOC ’06: Proceedings of the thirty-eighth annual ACM symposium on Theory of computing, pages 385–390, New York, NY, USA, 2006. ACM.
[KVV04] Ravi Kannan, Santosh Vempala, and Adrian Vetta. On clusterings: Good, bad and spectral. J. ACM, 51(3):497–515, 2004.
[LH08] Jure Leskovec and Eric Horvitz. Planetary-scale views on a large instant-messaging network. In WWW ’08: Proceeding of the 17th international conference on World Wide Web, pages 915–924. ACM, 2008.
[LR99] Tom Leighton and Satish Rao. Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms. Journal of the ACM, 46(6):787– 832, November 1999.
[LS90] L. Lovasz and M. Simonovits. The mixing rate of Markov chains, an isoperimetric inequality, and computing the volume. In IEEE, editor, Proceedings: 31st Annual Symposium on Foundations of Computer Science: October 22–24, 1990, St. Louis, Missouri, volume 1, pages 346–354, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 1990. IEEE Computer Society Press.
[LS93] Lovasz and Simonovits. Random walks in a convex body and an improved volume algorithm. RSA: Random Structures & Algorithms, 4:359–412, 1993.
[OSVV08] Lorenzo Orecchia, Leonard J. Schulman, Umesh V. Vazirani, and Nisheeth K. Vish- noi. On partitioning graphs via single commodity flows. In STOC ’08: Proceedings of the 40th annual ACM symposium on Theory of computing, pages 461–470, New York, NY, USA, 2008. ACM.
[PBMW98] Lawrence Page, Sergey Brin, Rajeev Motwani, and Terry Winograd. The pagerank citation ranking: Bringing order to the web. Technical report, Stanford Digital
Library Technologies Project, Stanford University, Stanford, CA, USA, November 1998.
[SLM+ 02] Ashish Sharma, Xinlian Liu, Paul Miller, Aiichiro Nakano, Rajiv K. Kalia, Priya Vashishta, Wei Zhao, Timothy J. Campbell, and Andy Haas. Immersive and in- teractive exploration of billion-atom systems. In VR ’02: Proceedings of the IEEE Virtual Reality Conference 2002, page 217. IEEE Computer Society, 2002.
[SS06] Jir ́ı S ́ıma and Satu Elisa Schaeffer. On the NP-completeness of some graph cluster measures. In Jir ́ı Wiedermann, Gerard Tel, Jaroslav Pokorny ́, M ́aria Bielikov ́a, and Julius Stuller, editors, SOFSEM, volume 3831 of Lecture Notes in Computer Science, pages 530–537. Springer, 2006.
[ST03] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems. available at http://arxiv.org/abs/cs.DS/0310051. An extended abstract appeared in Pro- ceedings of the thirty-sixth annual ACM symposium on Theory of computing, 81–90, 2003.
[ST08a] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for pre- conditioning and solving symmetric, diagonally dominant linear systems. CoRR, abs/cs/0607105, 2008. Available at http://www.arxiv.org/abs/cs.NA/0607105.
[ST08b] Daniel A. Spielman and Shang-Hua Teng. Spectral sparsification of graphs. CoRR, abs/0808.4134, 2008. Available at http://arxiv.org/abs/0808.4134.
Nearly linear time algorithms for preconditioning and solving symmetric, diagonally dominant linear systems. SIAM J. Matrix Anal. Appl. 35:835-885, 2014.
https://arxiv.org/pdf/cs/0607105.pdf
References
[ABN08] I. Abraham, Y. Bartal, and O. Neiman. Nearly tight low stretch spanning trees. In Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science, pages 781–790, Oct. 2008.
[AKPW95] Noga Alon, Richard M. Karp, David Peleg, and Douglas West. A graph-theoretic game and its application to the k-server problem. SIAM Journal on Computing, 24(1):78–100, February 1995.
[AM85] [AN12]
[Axe85] [BCHT04]
[BCPT05]
[BGH+06] [BH01] [BH03a]
William N. Anderson and Thomas D. Morley. Eigenvalues of the laplacian of a graph. Linear and Multilinear Algebra, 18(2):141–145, 1985.
Ittai Abraham and Ofer Neiman. Using petal-decompositions to build a low stretch spanning tree. In Proceedings of the 44th Annual ACM Symposium on the Theory of Computing (STOC ’12), pages 395–406, 2012.
O. Axelsson. A survey of preconditioned iterative methods for linear systems of algebraic equations. BIT Numerical Mathematics, 25(1):165–187, March 1985.
Erik G. Boman, Doron Chen, Bruce Hendrickson, and Sivan Toledo. Maximum- weight-basis preconditioners. Numerical linear algebra with applications, 11(8– 9):695–721, October/November 2004.
Erik G. Boman, Doron Chen, Ojas Parekh, and Sivan Toledo. On factor width and symmetric h-matrices. Linear Algebra and its Applications, 405(1):239–248, August 2005.
M. Bern, J. Gilbert, B. Hendrickson, N. Nguyen, and S. Toledo. Support-graph preconditioners. SIAM J. Matrix Anal. & Appl, 27(4):930–951, 2006.
Erik Boman and B. Hendrickson. On spanning tree preconditioners. Manuscript, Sandia National Lab., 2001.
Mario Bebendorf and Wolfgang Hackbusch. Existence of H-matrix approximants to the inverse FE-matrix of elliptic operators with L∞-coefficients. Numerische Mathematik, 95(1):1–28, July 2003.
[BH03b]
[BHM01] W. L. Briggs, V. E. Henson, and S. F. McCormick. A Multigrid Tutorial, 2nd
Erik G. Boman and Bruce Hendrickson. Support theory for preconditioning. SIAM Journal on Matrix Analysis and Applications, 25(3):694–717, 2003.
Edition. SIAM, 2001.
[BHV08] Erik G. Boman, Bruce Hendrickson, and Stephen A. Vavasis. Solving elliptic finite element systems in near-linear time with support preconditioners. SIAM J. on Numerical Analysis, 46(6):3264–3284, 2008.
[BMN04] M. Belkin, I. Matveeva, and P. Niyogi. Regularization and semi-supervised learning on large graphs. Proc. 17th Conf. on Learning Theory, pages 624–638, 2004.
[BSS09]
[CKM+11]
[CT03] [CW82] [Dem89] [DER86] [DS07] [DS08]
[EEST08] [FG04] [Fie73] [Geo73] [GMZ95]
[GO88]
Joshua D. Batson, Daniel A. Spielman, and Nikhil Srivastava. Twice-Ramanujan sparsifiers. In Proceedings of the 41st Annual ACM Symposium on Theory of com- puting, pages 255–262, 2009.
Paul Christiano, Jonathan A. Kelner, Aleksander Madry, Daniel A. Spielman, and Shang-Hua Teng. Electrical flows, laplacian systems, and faster approximation of maximum flow in undirected graphs. In Proceedings of the 43rd annual ACM sym- posium on Theory of computing, STOC ’11, pages 273–282, New York, NY, USA, 2011. ACM.
Doron Chen and Sivan Toledo. Vaidya’s preconditioners: implementation and ex- perimental study. Electronic Transactions on Numerical Analysis, 16:30–49, 2003.
D. Coppersmith and S. Winograd. On the asymptotic complexity of matrix multi- plication. SIAM Journal on Computing, 11(3):472–492, August 1982.
James Demmel. On floating point errors in cholesky. Technical report, Courant Institute, 1989. LAPACK Working Note 14.
I. S. Duff, A. M. Erisman, and J. K. Reid. Direct Methods for Sparse Matrices. Oxford Science Publications, 1986.
Samuel I. Daitch and Daniel A. Spielman. Support-graph preconditioners for 2- dimensional trusses. CoRR, abs/cs/0703119, 2007.
Samuel I. Daitch and Daniel A. Spielman. Faster approximate lossy generalized flow via interior point algorithms. In Proceedings of the 40th Annual ACM Symposium on Theory of Computing, pages 451–460, 2008.
Michael Elkin, Yuval Emek, Daniel A. Spielman, and Shang-Hua Teng. Lower- stretch spanning trees. SIAM Journal on Computing, 32(2):608–628, 2008.
A. Frangioni and C. Gentile. New preconditioners for KKT systems of network flow problems. SIAM Journal on Optimization, 14(3):894–913, 2004.
Miroslav Fiedler. Algebraic connectivity of graphs. Czechoslovak Mathematical Journal, 23(98):298–305, 1973.
J. A. George. Nested dissection of a regular finite element mesh. SIAM J. Numer. Anal., 10:345–363, 1973.
Keith D. Gremban, Gary L. Miller, and Marco Zagha. Performance evaluation of a new parallel preconditioner. In Proceedings of the 9th International Symposium on Parallel Processing, pages 65–69. IEEE Computer Society, 1995.
G. H. Golub and M. Overton. The convergence of inexact Chebychev and Richardson iterative methods for solving linear systems. Numerische Mathematik, 53:571–594, 1988.
[Gre96]
[GT87] [GV61]
[Har72] [Hig02]
[Jor69] [Jos97] [KM07]
[KM10]
[KMP10]
[KMP11]
[KMP12]
[KMST10]
[LRT79]
Keith Gremban. Combinatorial Preconditioners for Sparse, Symmetric, Diagonally Dominant Linear Systems. PhD thesis, Carnegie Mellon University, CMU-CS-96- 123, 1996.
John R. Gilbert and Robert Endre Tarjan. The analysis of a nested dissection algorithm. Numerische Mathematik, 50(4):377–404, February 1987.
Gene H. Golub and Richard S. Varga. Chebyshev semi-iterative methods, successive overrelaxation iterative methods, and second order richardson iterative methods. Numerische Mathematik, 3:157–168, 1961. 10.1007/BF01386014.
Frank Harary. Graph Theory. Addison-Wesley, 1972.
Nicholas J. Higham. Accuracy and Stability of Numerical Algorithms. Society for
Industrial and Applied Mathematics, Philadelphia, PA, USA, second edition, 2002. Camille Jordan. Sur les assemblages de lignes. Journal fu ̈r die reine und angewandte
Mathematik, 70:185–190, 1869.
Anil Joshi. Topics in Optimization and Sparse Linear Systems. PhD thesis, UIUC,
1997.
Ioannis Koutis and Gary L. Miller. A linear work, o(n1/6) time, parallel algorithm for solving planar Laplacians. In Proceedings of the 18th Annual ACM-SIAM Sym- posium on Discrete Algorithms, pages 1002–1011, 2007.
J.A. Kelner and A. Madry. Faster generation of random spanning trees. In Foun- dations of Computer Science, 2009. FOCS’09. 50th Annual IEEE Symposium on, pages 13–21. IEEE, 2010. This result was substantially improved as a result of an observation by James Propp. He will be added as a coauthor on the journal version.
I. Koutis, G.L. Miller, and R. Peng. Approaching optimality for solving sdd linear systems. In Foundations of Computer Science (FOCS), 2010 51st Annual IEEE Symposium on, pages 235 –244, 2010.
I. Koutis, G.L. Miller, and R. Peng. A nearly-mlogn time solver for sdd linear systems. In Foundations of Computer Science (FOCS), 2011 52nd Annual IEEE Symposium on, pages 590–598, 2011.
Jonathan A. Kelner, Gary L. Miller, and Richard Peng. Faster approximate mul- ticommodity flow using quadratically coupled flows. In Proceedings of the 44th symposium on Theory of Computing, STOC ’12, pages 1–18, New York, NY, USA, 2012. ACM.
Alexandra Kolla, Yury Makarychev, Amin Saberi, and Shang-Hua Teng. Subgraph sparsification and nearly optimal ultrasparsifiers. In Proceedings of the 42nd ACM symposium on Theory of computing, STOC ’10, pages 57–66, 2010.
Richard J. Lipton, Donald J. Rose, and Robert Endre Tarjan. Generalized nested dissection. SIAM Journal on Numerical Analysis, 16(2):346–358, April 1979.
[Mal00] A. N. Malyshev. A note on the stablity of gauss-jordan elimination for diagonally dominant matrices. Computing, 65:281–284, 2000.
[Mih89] Milena Mihail. Conductance and convergence of Markov chains—A combinatorial treatment of expanders. In 30th Annual IEEE Symposium on Foundations of Com- puter Science, pages 526–531, 1989.
[MMP+05] Bruce M. Maggs, Gary L. Miller, Ojas Parekh, R. Ravi, and Shan Leung Maverick Woo. Finding effective support-tree preconditioners. In Proceedings of the seven- teenth annual ACM symposium on Parallelism in algorithms and architectures, pages 176–185, 2005.
[Rei98] John Reif. Efficient approximate solution of sparse linear systems. Computers and Mathematics with Applications, 36(9):37–58, 1998.
[Sot10] Andrew Sothers. On the complexity of matrix multiplication. PhD thesis, University of Edinburg, 2010.
[SS08] Daniel A. Spielman and Nikhil Srivastava. Graph sparsification by effective resis- tances. In Proceedings of the 40th annual ACM Symposium on Theory of Computing, pages 563–568, 2008.
[SST06] Arvind Sankar, Daniel A. Spielman, and Shang-Hua Teng. Smoothed analysis of the condition numbers and growth factors of matrices. SIAM Journal on Matrix Analysis and Applications, 28(2):446–476, 2006.
[ST] Daniel A. Spielman and Shang-Hua Teng. A local clustering algorithm for massive graphs and its application to nearly-linear time graph partitioning. SIAM Journal on Computing. To appear.
[ST04] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems. In Proceedings of the thirty-sixth annual ACM Symposium on Theory of Computing, pages 81–90, 2004. Full version available at http://arxiv.org/abs/cs.DS/0310051.
[ST08] Gil Shklarski and Sivan Toledo. Rigidity in finite-element matrices: Sufficient con- ditions for the rigidity of structures and substructures. SIAM Journal on Matrix Analysis and Applications, 30(1):7–40, 2008.
[ST11] Daniel A. Spielman and Shang-Hua Teng. Spectral sparsification of graphs. SIAM Journal on Computing, 40(4):981–1025, 2011.
[Str86] Gilbert Strang. Introduction to Applied Mathematics. Wellesley-Cambridge Press, 1986.
[SW09] Daniel A. Spielman and Jaeoh Woo. A note on preconditioning by low-stretch spanning trees. CoRR, abs/0903.2816, 2009. Available at http://arxiv.org/abs/0903.2816.
[TB97] [Vai90]
[Wil12]
[ZBL+ 03]
[ZGL03]
[Zha05]
L. N. Trefethen and D. Bau. Numerical Linear Algebra. SIAM, Philadelphia, PA, 1997.
Pravin M. Vaidya. Solving linear equations with symmetric diagonally dominant matrices by constructing good preconditioners. Unpublished manuscript UIUC 1990. A talk based on the manuscript was presented at the IMA Workshop on Graph Theory and Sparse Matrix Computation, October 1991, Minneapolis., 1990.
V. Vassilevska Williams. Multiplying matrices faster than coppersmith-winograd. In Proceedings of the 44th Annual ACM Symposium on the Theory of Computing (STOC ’12), pages 887–898, 2012.
Dengyong Zhou, Olivier Bousquet, Thomas Navin Lal, Jason Weston, and Bernhard Scho ̈lkopf. Learning with local and global consistency. In Adv. in Neural Inf. Proc. Sys. 16, pages 321–328, 2003.
Xiaojin Zhu, Zoubin Ghahramani, and John D. Lafferty. Semi-supervised learning using Gaussian fields and harmonic functions. In Proc. 20th Int. Conf. on Mach. Learn., 2003.
Fuzhen Zhang, editor. The Schur Complement and its Applications, volume 4 of Numerical Methods and Algorithms. Springer, 2005.
####2014: Ronald Fagin, Amnon Lotem, and Moni Naor
Optimal Aggregation Algorithms for Middleware
https://arxiv.org/pdf/cs/0204046.pdf
####2013: Antoine Joux, Dan Boneh, and Matthew K. Franklin
A One Round Protocol for Tripartite Diffie–Hellman
Antoine Joux, Journal of Cryptology volume 17, pages263–276(2004)
https://link.springer.com/content/pdf/10.1007/s00145-004-0312-y.pdf
Identity-Based Encryption from the Weil Pairing
Dan Boneh∗ Matthew Franklin
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.66.1131&rep=rep1&type=pdf
Nisan, Noam; Ronen, Amir (2001). "Algorithmic Mechanism Design". Games and Economic Behavior. 35 (1–2): 166–196.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.21.1731&rep=rep1&type=pdf
####2012: Elias Koutsoupias, Christos H.Papadimitriou, Tim Roughgarden, Éva Tardos, Noam Nisan, and Amir Ronen
Koutsoupias, Elias; Papadimitriou, Christos (2009). "Worst-case equilibria". Computer Science Review. 3 (2): 65–69. doi:10.1016/j.cosrev.2009.04.003.
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=08343A18C75A6F5A0E57B25562499E5C?doi=10.1.1.102.6991&rep=rep1&type=pdf
Roughgarden, Tim; Tardos, Éva (2002). "How bad is selfish routing?". Journal of the ACM. 49 (2): 236–259. CiteSeerX 10.1.1.147.1081. doi:10.1145/506147.506153.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.147.1081&rep=rep1&type=pdf
Nisan, Noam; Ronen, Amir (2001). "Algorithmic Mechanism Design". Games and Economic Behavior. 35 (1–2): 166–196. CiteSeerX 10.1.1.21.1731. doi:10.1006/game.1999.0790.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.21.1731&rep=rep1&type=pdf
####2011: Johan T. Håstad
https://sigact.org/prizes/gödel/2011.html
The 2011 Gödel Prize is awarded to Johan T. Håstad for his paper:
Some optimal inapproximability results, Journal of the ACM, 48: 798--859, 2001.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.638.2808&rep=rep1&type=pdf
####2010: Sanjeev Arora and Joseph S. B. Mitchell
https://sigact.org/prizes/gödel/2010.html
The 2010 Gödel Prize is awarded to
Sanjeev Arora and Joseph S.B. Mitchell for their concurrent discovery of a polynomial-time approximation scheme (PTAS) for the Euclidean Travelling Salesman Problem (ETSP):
Sanjeev Arora. (1998). Polynomial-time approximation schemes for Euclidean TSP and other geometric problems, Journal ACM 45(5), 753-782.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.23.6765&rep=rep1&type=pdf
Joseph S.B. Mitchell (1999). Guillotine subdivisions approximate polygonal subdivisions: A simple polynomial-time approximation scheme for geometric TSP, k-MST, and related problems, SIAM J. Computing 28(4), 1298-1309.
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=EBC1BCCD86A8ECD59B018C11236ECA89?doi=10.1.1.56.4805&rep=rep1&type=pdf
####2009: Omer Reingold, Salil Vadhan, and Avi Wigderson
https://sigact.org/prizes/gödel/2009.html
The 2009 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to
(1) Entropy waves, the zig-zag graph product and new constant degree expanders. Omer Reingold, Salil Vadhan and Avi Wigderson, Annals of Mathematics, Vol 155, (2002), 157-187
https://arxiv.org/pdf/math/0406038.pdf
and
(2) Undirected connectivity in Log-Space. Omer Reingold, Journal of ACM, Vol 55 (4) (2007).
- Requested.
####2008: Dan Spielman and Shang-Hua Teng
https://sigact.org/prizes/gödel/2008.html
The 2008 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to
Daniel A. Spielman and Shang-Hua Teng for their paper: Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time by Daniel A. Spielman and Shang-Hua Teng, Journal of the ACM (JACM), 51(3), May 2004, 385-463.
First presented at the Annual ACM Symposium on the Theory of Computing (STOC 01), 2001, 296-305.
https://arxiv.org/pdf/math/0212413.pdf
####2007: Alexander A. Razborov and Steven Rudich
https://sigact.org/prizes/gödel/2007.html
The 2007 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to Alexander A. Razborov and Steven Rudich for their paper:
Natural Proofs, Journal of Computer and System Sciences, Vol. 55, No. 1, 1997, pp. 24-35.
First presented at the Twenty-sixth Annual ACM Symposium on Theory of computing, Montreal, Quebec, Canada. 1994, pp. 204-213.
https://reader.elsevier.com/reader/sd/pii/S002200009791494X?token=9E8D5C0FAA5F8E450DFB32BDEDED9B07CACDC4BD40EA21B35A33BF9E74A24E840B6AF2E6FF1C20F6ED02778CA1FC109C
####2006: Manindra Agrawal, Neeraj Kayal, and Nitin Saxena
https://sigact.org/prizes/gödel/2006.html
The 2006 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to Manindra Agrawal, Neeraj Kayal, and Nitin Saxena for their paper:
PRIMES is in P. Annals of Mathematics 160(2), 781-793, 2004.
https://web.archive.org/web/20110607101302/http://math.berkeley.edu/~coleman/Courses/Fall08/Cryptography/primality_v6.pdf
2005: Noga Alon, Yossi Matias and Mario Szegedy
The 2005 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to
Noga Alon, Yossi Matias and Mario Szegedy for their paper: The space complexity of approximating the frequency moments. Journal of Computer and System Sciences 58 (1999), 137-147 First presented at the 28th ACM Symposium on Theory of Computing, 1996.
http://www.math.tau.ac.il/~nogaa/PDFS/amsz4.pdf
2004: Maurice Herlihy and Nir Shavit / Michael Saks and Fotios Zaharoglou
The 2004 Gödel Prize for outstanding journal articles in theoretical computer science is shared between the papers:
"The Topological Structure of Asynchronous Computation" by Maurice Herlihy and Nir Shavit, Journal of the ACM, Vol. 46 (1999), 858-923,
http://cs.brown.edu/~mph/HerlihyS99/p858-herlihy.pdf
and
"Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge" by Michael Saks and Fotios Zaharoglou, SIAM J. on Computing, Vol. 29 (2000), 1449-1483.
- Requested.
2003: Yoav Freund and Robert Schapire
The prize was awarded to
Yoav Freund and Robert Schapire for their paper "A Decision Theoretic Generalization of On-Line Learning and an Application to Boosting," Journal of Computer and System Sciences 55 (1997), pp. 119-139.
https://www-ai.cs.tu-dortmund.de/LEHRE/PG/PG445/literatur/freund_schapire_97a.pdf
2002: Géraud Sénizergues
Geraud Senizergues, for "L(A)=L(B)? Decidability results from complete formal systems", Theoretical Computer Science 251 (2001), pp.1-166.
https://reader.elsevier.com/reader/sd/pii/S0304397500002851?token=64A2B37155D426438B12D3E16D9DA7D657C01E4E4944CA307F3319EB3724727119FF108137109C77E438B12E754C1179
2001: Sanjeev Arora, Uriel Feige, Shafi Goldwasser, Carsten Lund, László Lovász, Rajeev Motwani, Shmuel Safra, Madhu Sudan, and Mario Szegedy
The 2001 Gödel Prize for outstanding journal article in the area of theoretical computer science is awarded to
Sanjeev Arora, Uriel Feige, Shafi Goldwasser, Carsten Lund, Laszlo Lovász, R. Motwani, Shmuel Safra, Madhu Sudan, and Mario Szegedy for the following series of papers:
"Interactive Proofs and the Hardness of Approximating Cliques". Uriel Feige, Shafi Goldwasser, Laszlo Lovász, Shmuel Safra, and Mario Szegedy. Journal of the ACM 43 (1996), 268-292.
https://www.researchgate.net/profile/Mario_Szegedy/publication/234783217_Interactive_proofs_and_the_hardness_of_approximating_cliques/links/09e41514878e8c2f78000000/Interactive-proofs-and-the-hardness-of-approximating-cliques.pdf
"Probabilistic Checking of Proofs: A New Characterization of NP". Sanjeev Arora and Shmuel Safra. Journal of the ACM 45 (1998), 70-122.
https://web.archive.org/web/20110610101051/http://www.cs.umd.edu/~gasarch/pcp/AS.pdf
"Proof Verification and the Hardness of Approximation Problems". Sanjeev Arora, Carsten Lund, Rajeev Motwani, Madhu Sudan, and Mario Szegedy. Journal of the ACM 45 (1998), 501-555.
https://web.archive.org/web/20110610101241/https://www.cs.umd.edu/~gasarch/pcp/ALMSS.pdf
2000: Moshe Vardi and Pierre Wolper
The 2000 Gödel Prize is awarded to
Moshe Vardi and Pierre Wolper for their paper:
Reasoning about infinite computations. Moshe Y. Vardi, Pierre Wolper. Information and Computation 115 (1994), 1-37.
https://web.archive.org/web/20110825210914/http://reference.kfupm.edu.sa/content/r/e/reasoning_about_infinite_computations__102167.pdf
1999: Peter W. Shor
The 1999 Gödel Prize for outstanding journal article in the area of theoretical computer science is awarded to
Peter W. Shor for his paper "Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer", SIAM Journal on Computing 26 (1997), 1484-1509.
https://arxiv.org/pdf/quant-ph/9508027.pdf
1998: Seinosuke Toda
The 1998 Gödel Prize for outstanding journal article in the area of theoretical computer science will be awarded to
Seinosuke Toda for his paper "PP is as Hard as the Polynomial-Time Hierarchy," SIAM Journal on Computing 20 (1991), 865-877.
https://people.engr.tamu.edu/j-chen3/courses/637/2008/pres/korben.pdf
1997: Joseph Halpern and Yoram Moses
The 1997 Gödel Prize for outstanding journal articles in the area of theoretical computer science will be awarded to
Joseph Halpern and Yoram Moses for their paper "Knowledge and Common Knowledge in a Distributed Environment," J. ACM 37} (1990), 549-587.
https://www.cs.cornell.edu/home/halpern/papers/common_knowledge.pdf
1996: Mark Jerrum and Alistair Sinclair
The 1996 Gödel Prize for outstanding journal articles in the area of theoretical computer science was awarded on May 23, 1996 jointly to
Mark Jerrum and Alistair Sinclair for their papers "Approximate counting, unform generation and rapidly mixing Markov chains," Information and Computation 82 (1989), 93-133, by Sinclair and Jerrum,
https://reader.elsevier.com/reader/sd/pii/0890540189900679?token=518EF4273B015187831CB0A883A601D699224964F2F448061BEE0B856FC0FE6A24FCDD1567B81553115DC281EB962793
and
"Approximating the permanent," SIAM Journal on Computing 18 (1989), 1149-1178, by Jerrum and Sinclair.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.431.4190&rep=rep1&type=pdf
1995: Neil Immerman and Róbert Szelepcsényi
The Gödel prize committee has selected the co-recipients of the Gödel Prize for 1995. The prize is awarded for the following two papers:
Neil Immerman, "Nondeterministic space is closed under complementation," SIAM Journal on Computing 17 (1988), 935-938
https://people.cs.umass.edu/~immerman/pub/space.pdf
and
Róbert Szelepcsényi, "The method of forced enumeration for nondeterministic automata," Acta Informatica 26 (1988), 279-284.
https://dml.cz/bitstream/handle/10338.dmlcz/120489/ActaOstrav_03-1995-1_10.pdf
1994: Johan Håstad
Johan Håstad, "Almost optimal lower bounds for small depth circuits," Advances in Computing Research 5 (1989), 143-170.
https://web.archive.org/web/20120222163102/http://reference.kfupm.edu.sa/content/a/l/almost_optimal_lower_bounds_for_small_de_134215.pdf
1993: László Babai, Shafi Goldwasser, Silvio Micali, Shlomo Moran, and Charles Rackoff
The 1993 Gödel Prize was shared by two papers,
László Babai and Shlomo Moran, "Arthur-Merlin games: a randomized proof system and a hierarchy of complexity classes," Journal of Computer and System Sciences, 36 (1988), 254-276,
http://crypto.cs.mcgill.ca/~crepeau/COMP647/2007/TOPIC01/AMgames-Babai-Moran.pdf
and
Shafi Goldwasser, Silvio Micali, and Charles Rackoff, "The knowledge complexity of interactive proof systems," SIAM Journal on Computing 18 (1989), 186-208.
http://crypto.cs.mcgill.ca/~crepeau/COMP647/2007/TOPIC02/GMR89.pdf
#作業場(work space)
まずゲーテルの論文の単語帳。
自分のPCにあるフォルダ名が
/Users/administrator/Downloads/godel
の場合
$ docker run -v /Users/administrator/Downloads/godel:/tmp/godel -it kaizenjapan/godel /bin/bash
いつもは上位１００語を表示する。
数式が多く、１語は式でしか現れないかもしれない。
１０語以上だと上位１３６位まで。
整列は表計算ソフトに読み込んで並べ替えをした。
| work | count |
|---|---|
| the | 413 |
| x | 395 |
| of | 255 |
| a | 237 |
| is | 211 |
| n | 182 |
| y | 159 |
| and | 146 |
| to | 120 |
| that | 119 |
| for | 112 |
| v | 106 |
| in | 102 |
| r | 80 |
| we | 77 |
| by | 75 |
| i | 73 |
| z | 71 |
| not | 69 |
| are | 66 |
| number | 63 |
| this | 59 |
| p | 58 |
| formula | 55 |
| it | 51 |
| provable | 49 |
| q | 48 |
| primitive | 47 |
| one | 46 |
| as | 44 |
| be | 43 |
| if | 43 |
| with | 43 |
| forall | 41 |
| sign | 39 |
| axiom | 37 |
| length | 37 |
| class | 36 |
| k | 36 |
| free | 35 |
| item | 35 |
| or | 35 |
| recursive | 35 |
| from | 34 |
| subst | 34 |
| which | 34 |
| there | 33 |
| an | 32 |
| proof | 32 |
| relation | 31 |
| type | 31 |
| system | 30 |
| theorem | 30 |
| formulae | 29 |
| variable | 29 |
| all | 28 |
| numbers | 28 |
| where | 28 |
| will | 28 |
| can | 27 |
| e | 27 |
| you | 27 |
| axioms | 26 |
| on | 26 |
| s | 25 |
| xn | 25 |
| b | 24 |
| have | 23 |
| every | 22 |
| natural | 22 |
| paper | 22 |
| succ | 22 |
| other | 21 |
| such | 21 |
| but | 19 |
| following | 19 |
| sequence | 19 |
| go | 18 |
| translation | 18 |
| would | 18 |
| also | 17 |
| rq | 17 |
| u | 17 |
| consistency | 16 |
| consistent | 16 |
| del | 16 |
| then | 16 |
| basic | 15 |
| finite | 15 |
| text | 15 |
| undecidable | 15 |
| variables | 15 |
| any | 14 |
| defined | 14 |
| function | 14 |
| has | 14 |
| pm | 14 |
| seq | 14 |
| signs | 14 |
| argmin | 13 |
| because | 13 |
| call | 13 |
| concepts | 13 |
| does | 13 |
| now | 13 |
| only | 13 |
| first | 12 |
| formal | 12 |
| holds | 12 |
| more | 12 |
| no | 12 |
| prooffor | 12 |
| used | 12 |
| was | 12 |
| at | 11 |
| decision | 11 |
| define | 11 |
| fact | 11 |
| functions | 11 |
| its | 11 |
| let | 11 |
| schema | 11 |
| set | 11 |
| so | 11 |
| systems | 11 |
| these | 11 |
| c | 10 |
| example | 10 |
| hand | 10 |
| my | 10 |
| obtained | 10 |
| proposition | 10 |
| quantor | 10 |
| relations | 10 |
| some | 10 |
| well | 10 |
受賞論文
２論文が未入手、２論文が事前投稿論文。
式の中に２文字の記号を含むと仮定すると
676語は式中の記号の可能性がある。
ひとまず出現頻度が100までの683語を示す。
残りは、最後に記載したのDocker Hub上にファイルあり。
./ptt.sh
cat text/* > all.txt
awk -f wc.awk all.txt > wc.txt
| word | count | note |
|---|---|---|
| the | 29214 | |
| a | 19144 | |
| of | 18139 | |
| and | 11769 | |
| is | 11715 | |
| in | 10220 | |
| y | 9933 | |
| f | 9700 | |
| i | 9139 | |
| to | 9012 | |
| x | 8913 | |
| that | 8803 | |
| b | 8657 | |
| s | 8465 | |
| n | 8129 | |
| h | 7348 | |
| we | 7335 | |
| u | 7322 | |
| for | 6999 | |
| q | 6720 | |
| p | 5916 | |
| c | 5906 | |
| g | 5442 | |
| k | 5207 | |
| m | 4554 | |
| e | 4407 | |
| v | 4307 | |
| by | 4258 | |
| t | 4257 | |
| d | 4090 | |
| be | 4043 | |
| j | 4022 | |
| this | 3882 | |
| r | 3542 | |
| l | 3330 | |
| as | 3196 | |
| with | 3119 | |
| on | 3094 | |
| an | 2935 | |
| if | 2741 | |
| it | 2565 | |
| are | 2553 | |
| let | 2399 | |
| then | 2198 | |
| at | 2137 | |
| w | 2051 | |
| proof | 2000 | |
| from | 1929 | |
| can | 1921 | |
| z | 1873 | |
| lemma | 1717 | |
| which | 1700 | |
| o | 1692 | |
| not | 1646 | |
| all | 1577 | |
| such | 1562 | |
| have | 1509 | |
| each | 1419 | |
| log | 1411 | |
| set | 1407 | |
| theorem | 1394 | |
| where | 1315 | |
| there | 1278 | |
| algorithm | 1201 | |
| some | 1187 | |
| one | 1186 | |
| random | 1172 | |
| time | 1143 | |
| any | 1132 | |
| will | 1130 | |
| our | 1090 | |
| probability | 1053 | |
| or | 1041 | |
| every | 1019 | |
| has | 998 | |
| _ | 993 | |
| polynomial | 959 | |
| number | 957 | |
| case | 920 | |
| two | 895 | |
| given | 887 | |
| only | 883 | |
| bi | 856 | |
| since | 844 | |
| graph | 825 | |
| so | 823 | |
| function | 821 | |
| most | 802 | |
| problem | 776 | |
| these | 743 | |
| when | 739 | |
| using | 722 | |
| section | 719 | |
| also | 715 | |
| its | 714 | |
| follows | 710 | |
| de | 696 | |
| first | 683 | |
| now | 682 | |
| use | 677 | |
| following | 661 | |
| size | 649 | |
| least | 645 | |
| us | 639 | |
| computer | 635 | |
| input | 624 | |
| ii | 616 | |
| than | 615 | |
| thus | 611 | |
| value | 611 | |
| system | 599 | |
| more | 594 | |
| over | 594 | |
| but | 592 | |
| no | 589 | |
| show | 588 | |
| see | 587 | |
| linear | 575 | |
| hence | 548 | |
| prove | 543 | |
| state | 543 | |
| other | 529 | |
| definition | 518 | |
| same | 512 | |
| pp | 511 | |
| note | 509 | |
| xu | 507 | |
| science | 505 | |
| np | 504 | |
| above | 503 | |
| may | 503 | |
| free | 495 | |
| ca | 477 | |
| do | 475 | |
| variables | 459 | |
| vertex | 459 | |
| constant | 457 | |
| result | 448 | |
| bound | 446 | |
| consider | 442 | |
| new | 441 | |
| problems | 435 | |
| algorithms | 433 | |
| TRUE | 429 | |
| approximation | 428 | |
| verifier | 425 | |
| paper | 424 | |
| does | 421 | |
| protocol | 421 | |
| assume | 413 | |
| deterministic | 411 | |
| was | 409 | |
| step | 407 | |
| vol | 407 | |
| exists | 398 | |
| between | 397 | |
| degree | 397 | |
| th | 395 | |
| complexity | 394 | |
| denote | 391 | |
| point | 390 | |
| xi | 390 | |
| output | 389 | |
| define | 384 | |
| pr | 384 | |
| si | 383 | |
| edges | 381 | |
| example | 380 | |
| edge | 379 | |
| resource | 379 | |
| used | 376 | |
| fact | 373 | |
| theory | 371 | |
| values | 371 | |
| must | 366 | |
| graphs | 361 | |
| bits | 357 | |
| oracle | 357 | |
| both | 351 | |
| max | 351 | |
| length | 349 | |
| assignment | 345 | |
| functions | 343 | |
| their | 342 | |
| form | 339 | |
| key | 339 | |
| would | 336 | |
| they | 335 | |
| process | 334 | |
| results | 331 | |
| computing | 328 | |
| matrix | 327 | |
| work | 327 | |
| defined | 325 | |
| acm | 324 | |
| condition | 323 | |
| under | 318 | |
| list | 316 | |
| proofs | 316 | |
| test | 316 | |
| possible | 315 | |
| way | 314 | |
| min | 313 | |
| lower | 311 | |
| systems | 311 | |
| suppose | 307 | |
| mod | 306 | |
| property | 306 | |
| here | 304 | |
| cost | 303 | |
| small | 303 | |
| order | 301 | |
| instance | 300 | |
| into | 300 | |
| get | 298 | |
| sequence | 297 | |
| tree | 296 | |
| how | 294 | |
| distribution | 292 | |
| second | 291 | |
| well | 291 | |
| whose | 289 | |
| un | 288 | |
| emp | 287 | |
| wi | 287 | |
| non | 286 | |
| however | 285 | |
| obtain | 283 | |
| ai | 281 | |
| implies | 281 | |
| ui | 280 | |
| within | 280 | |
| been | 279 | |
| vi | 279 | |
| need | 278 | |
| vertices | 277 | |
| map | 275 | |
| factor | 273 | |
| quantum | 273 | |
| based | 272 | |
| access | 271 | |
| complex | 271 | |
| part | 270 | |
| optimal | 269 | |
| model | 267 | |
| points | 266 | |
| even | 265 | |
| independent | 265 | |
| analysis | 264 | |
| make | 261 | |
| nite | 261 | |
| symposium | 261 | |
| about | 260 | |
| simplex | 260 | |
| vector | 260 | |
| al | 259 | |
| because | 259 | |
| bounded | 256 | |
| path | 253 | |
| proceedings | 253 | |
| computation | 252 | |
| sum | 252 | |
| yjv | 252 | |
| say | 251 | |
| sets | 251 | |
| string | 251 | |
| variable | 251 | |
| class | 250 | |
| program | 248 | |
| corresponding | 246 | |
| large | 246 | |
| main | 245 | |
| while | 245 | |
| hard | 244 | |
| ud | 244 | |
| udc | 244 | |
| depth | 243 | |
| automata | 241 | |
| known | 241 | |
| procedure | 241 | |
| automaton | 240 | |
| construction | 239 | |
| natural | 236 | |
| sj | 236 | |
| accepts | 235 | |
| bit | 235 | |
| bounds | 235 | |
| either | 234 | |
| formula | 234 | |
| ta | 234 | |
| give | 233 | |
| theoretical | 233 | |
| particular | 232 | |
| logic | 231 | |
| object | 231 | |
| objects | 228 | |
| general | 227 | |
| check | 226 | |
| nition | 225 | |
| last | 223 | |
| many | 221 | |
| chosen | 220 | |
| space | 220 | |
| proposition | 218 | |
| udy | 218 | |
| otherwise | 217 | |
| simple | 217 | |
| zero | 216 | |
| et | 215 | |
| notion | 213 | |
| states | 213 | |
| ratio | 212 | |
| sorted | 212 | |
| properties | 211 | |
| local | 210 | |
| product | 210 | |
| interactive | 209 | |
| parallel | 209 | |
| call | 208 | |
| approximate | 207 | |
| equations | 207 | |
| complete | 206 | |
| full | 206 | |
| claim | 204 | |
| di | 204 | |
| holds | 203 | |
| integer | 203 | |
| ti | 203 | |
| find | 202 | |
| finite | 202 | |
| next | 202 | |
| ne | 201 | |
| satisfying | 200 | |
| inequality | 199 | |
| pi | 199 | |
| similar | 199 | |
| up | 199 | |
| xud | 199 | |
| ia | 198 | |
| close | 197 | |
| just | 197 | |
| mechanism | 197 | |
| poly | 196 | |
| annual | 195 | |
| hhv | 195 | |
| processes | 195 | |
| recall | 195 | |
| circuit | 193 | |
| gives | 193 | |
| unsat | 193 | |
| left | 192 | |
| weight | 192 | |
| choose | 191 | |
| conditions | 191 | |
| task | 191 | |
| therefore | 190 | |
| very | 190 | |
| flow | 188 | |
| ned | 188 | |
| corollary | 187 | |
| times | 187 | |
| arbitrary | 186 | |
| called | 185 | |
| line | 185 | |
| standard | 185 | |
| subdivision | 185 | |
| top | 185 | |
| proc | 183 | |
| compute | 182 | |
| cannot | 181 | |
| queries | 181 | |
| uniform | 181 | |
| contains | 180 | |
| expected | 180 | |
| structure | 180 | |
| ieee | 179 | Institute of Electrical and Electronics Engineers |
| probabilistic | 179 | |
| running | 179 | |
| chain | 178 | |
| languages | 178 | |
| enizergues | 177 | human name |
| induction | 177 | |
| language | 177 | |
| group | 176 | |
| shown | 176 | |
| reduction | 175 | |
| type | 175 | |
| code | 174 | |
| distance | 174 | |
| information | 174 | |
| obtained | 174 | |
| required | 174 | |
| rule | 173 | |
| agent | 172 | |
| describe | 172 | |
| without | 171 | |
| after | 170 | |
| construct | 170 | |
| figure | 170 | |
| exactly | 169 | |
| should | 169 | |
| assumption | 168 | |
| cau | 168 | |
| could | 168 | |
| hypothesis | 168 | |
| satis | 168 | |
| what | 168 | |
| almost | 167 | |
| positive | 167 | |
| matrices | 166 | |
| three | 166 | |
| uses | 166 | |
| grade | 165 | |
| satisfies | 165 | |
| described | 164 | |
| below | 162 | |
| fixed | 162 | |
| good | 162 | |
| nu | 162 | |
| out | 162 | |
| ri | 162 | |
| solution | 162 | |
| version | 162 | |
| knowledge | 160 | |
| pair | 160 | |
| terms | 160 | |
| counting | 159 | |
| different | 159 | |
| whether | 159 | |
| alphabet | 158 | |
| connected | 158 | |
| constraint | 158 | |
| ji | 158 | |
| siam | 158 | Society for Industrial and Applied Mathematics |
| vectors | 158 | |
| choice | 157 | |
| clearly | 157 | |
| efficient | 157 | |
| sat | 157 | |
| steps | 157 | |
| agents | 156 | |
| cs | 156 | computer science |
| inputs | 156 | |
| pages | 156 | |
| programs | 156 | |
| those | 156 | |
| public | 154 | |
| shows | 153 | |
| special | 152 | |
| them | 152 | |
| easy | 151 | |
| fraction | 151 | |
| less | 151 | |
| proved | 151 | |
| approximating | 150 | |
| pcp | 150 | |
| apply | 149 | |
| decision | 149 | |
| high | 149 | |
| notation | 149 | |
| right | 149 | |
| scheme | 149 | |
| similarly | 149 | |
| am | 147 | |
| before | 147 | |
| prover | 147 | |
| abort | 146 | |
| cases | 146 | |
| were | 146 | |
| another | 145 | |
| cut | 145 | |
| finally | 145 | |
| know | 145 | |
| through | 145 | |
| discrete | 144 | |
| id | 144 | identifier |
| method | 144 | |
| arora | 143 | |
| au | 142 | |
| outputs | 142 | |
| constraints | 141 | |
| ei | 141 | |
| error | 141 | |
| view | 141 | |
| elements | 140 | |
| makes | 140 | |
| rst | 140 | |
| regular | 139 | |
| rules | 139 | |
| subset | 139 | |
| takes | 139 | |
| fp | 138 | |
| lattice | 138 | |
| memory | 138 | |
| optimality | 138 | |
| prime | 138 | |
| much | 137 | |
| relation | 137 | |
| requires | 136 | |
| single | 136 | |
| again | 135 | |
| being | 135 | |
| equivalent | 135 | |
| series | 135 | |
| hand | 134 | |
| satisfy | 134 | |
| nodes | 133 | |
| partition | 133 | |
| programming | 133 | |
| boolean | 132 | |
| gf | 132 | |
| observe | 132 | |
| st | 132 | |
| total | 132 | |
| vb | 132 | |
| words | 132 | |
| field | 131 | |
| game | 131 | |
| machine | 131 | |
| self | 131 | |
| write | 131 | |
| answer | 130 | |
| numbers | 130 | |
| power | 130 | |
| real | 130 | |
| argument | 129 | |
| basic | 129 | |
| database | 129 | |
| done | 129 | |
| might | 129 | |
| owned | 129 | |
| run | 129 | |
| take | 129 | |
| able | 128 | |
| accept | 128 | |
| curve | 128 | |
| seen | 128 | |
| springer | 128 | |
| start | 128 | |
| useful | 128 | |
| circuits | 127 | |
| equal | 127 | |
| moreover | 127 | |
| present | 127 | |
| always | 126 | |
| pairing | 126 | |
| entries | 125 | |
| markov | 125 | |
| put | 125 | |
| accesses | 124 | |
| comput | 124 | |
| level | 124 | |
| merlin | 124 | |
| original | 124 | |
| remark | 124 | |
| context | 123 | |
| combinatorial | 122 | |
| dom | 122 | |
| further | 122 | |
| idea | 122 | |
| nd | 122 | |
| tsp | 122 | |
| ci | 121 | |
| cr | 121 | |
| execution | 121 | |
| notes | 121 | |
| simplicial | 121 | |
| xk | 121 | |
| aw | 120 | |
| exist | 120 | |
| low | 120 | |
| randomized | 120 | |
| rather | 120 | |
| aggregation | 119 | |
| applications | 119 | |
| formal | 119 | |
| notice | 119 | |
| operations | 119 | |
| exp | 118 | |
| family | 118 | |
| inv | 118 | |
| perfect | 118 | |
| query | 118 | |
| sense | 118 | |
| upper | 118 | |
| aq | 117 | |
| bk | 117 | |
| restriction | 117 | |
| square | 117 | |
| trace | 117 | |
| transition | 117 | |
| approach | 116 | |
| equation | 116 | |
| polynomials | 116 | |
| root | 116 | |
| heap | 115 | |
| word | 115 | |
| conclude | 113 | |
| encoding | 113 | |
| hardness | 113 | |
| made | 113 | |
| maximum | 113 | |
| previous | 113 | |
| techniques | 113 | |
| uj | 113 | |
| element | 112 | |
| private | 112 | |
| separation | 112 | |
| simply | 112 | |
| strategy | 112 | |
| design | 111 | |
| event | 111 | |
| journal | 111 | |
| lists | 111 | |
| nc | 111 | |
| writes | 111 | |
| arthur | 110 | |
| encryption | 110 | |
| er | 110 | |
| instances | 110 | |
| ny | 110 | |
| soundness | 110 | |
| yj | 110 | |
| chromatic | 109 | |
| equivalence | 109 | |
| generator | 109 | |
| li | 109 | |
| models | 109 | |
| nonzero | 109 | |
| respectively | 109 | |
| completeness | 108 | |
| dl | 108 | |
| lecture | 108 | |
| security | 108 | |
| acceptance | 107 | |
| buf | 107 | |
| bw | 107 | |
| open | 107 | |
| checking | 106 | |
| classes | 106 | |
| iff | 106 | |
| minimum | 106 | |
| tb | 106 | |
| formulas | 105 | |
| important | 105 | |
| initial | 105 | |
| read | 105 | |
| side | 105 | |
| unique | 105 | |
| xn | 105 | |
| conductance | 104 | |
| latency | 104 | |
| paths | 104 | |
| appear | 103 | |
| bn | 103 | |
| boundary | 103 | |
| distinct | 103 | |
| oracles | 103 | |
| sequential | 103 | |
| still | 103 | |
| strings | 103 | |
| accepting | 102 | |
| ap | 102 | |
| computed | 102 | |
| long | 102 | |
| node | 102 | |
| question | 102 | |
| associated | 101 | |
| easily | 101 | |
| im | 101 | |
| udn | 101 | |
| gate | 100 | |
| like | 100 | |
| matching | 100 | |
| means | 100 | |
| ownership | 100 | |
| partial | 100 | |
| provided | 100 | |
| row | 100 | |
| symmetric | 100 | |
| weighted | 100 |
tools
単語出現頻度計数
# Print list of word frequencies
# https://researchmap.jp/jomd7nobo-45644/
# https://qiita.com/kaizen_nagoya/items/670d4d332e07fd2e5fc2
# This is for papers, not for programming.
# remove _ from gsub list 20200101 @kaizen_nagoya
{
$0 = tolower($0) #
gsub(/[^a-z \t]/, " ", $0) #
for (i = 1; i <= NF; i++)
freq[$i]++
}
END {
for (word in freq)
printf "%s\t%d\n", word, freq[word]
}
一括処理
#!/bin/bash
# https://news.mynavi.jp/article/bashonwindows-17/
# https://qiita.com/kaizen_nagoya/items/319672853519990cee42
cd ../pdf
for File in *; do
case ${File##*.} in
pdf|PDF )
echo "Convert the PDF:" ${File}
pdftotext -q ${File} ../text/${File}.txt ;;
*) ;;
esac
done
docker hub登録
docker 起動（最初）
$ docker run -v /Users/administrator/Downloads/godel:/tmp/godel -it ubuntu /bin/bash
dockerでの作業
# apt update; apt -y upgrade
# apt install -y poppler-utils vim wget
# wget http://hirzels.com/martin/papers/canon00-goedel.pdf
# pdftotext -q canon00-goedel.pdf canon00-goedel.txt
# awk -f wc.awk canon00-goedel.txt >godelwc.txt
docker hub 登録
$ docker commit 7aa98d94d8da kaizenjapan/godel
$ docker push kaizenjapan/godel
次回起動
$ docker run -v /Users/administrator/Downloads/godel:/tmp/godel -it kaizenjapan/godel /bin/bash
文書履歴(document history)
ver. 0.01 初稿 20201020
ver. 0.02 ゲーデル論文URL記載 20201024午前
ver. 0.03 ゲーテル論文単語帳 20201024午後
ver. 0.04 単語帳作成、docker登録 20201024 夜
ver. 0.05 Reference 追記 20201025