{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:04:21Z","timestamp":1742925861333,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319456409"},{"type":"electronic","value":"9783319456416"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-45641-6_10","type":"book-chapter","created":{"date-parts":[[2016,9,8]],"date-time":"2016-09-08T10:30:29Z","timestamp":1473330629000},"page":"134-155","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Incompleteness, Undecidability and Automated Proofs"],"prefix":"10.1007","author":[{"given":"Cristian S.","family":"Calude","sequence":"first","affiliation":[]},{"given":"Declan","family":"Thompson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,9]]},"reference":[{"key":"10_CR1","unstructured":"Alf homepage. http:\/\/homepages.inf.ed.ac.uk\/wadler\/realworld\/alf.html . Accessed 25 Oct 2014"},{"key":"10_CR2","unstructured":"Archive of formal proofs. http:\/\/afp.sourceforge.net . Accessed 18 May 2016"},{"key":"10_CR3","unstructured":"Coq homepage. http:\/\/coq.inria.fr\/ . Accessed 25 Oct 2014"},{"key":"10_CR4","unstructured":"HOL4 homepage. http:\/\/hol.sourceforge.net\/ . Accessed 25 Oct 2014"},{"key":"10_CR5","unstructured":"Isabelle homepage. http:\/\/isabelle.in.tum.de\/ . Accessed 20 Oct 2014"},{"key":"10_CR6","unstructured":"Matita hompage. http:\/\/matita.cs.unibo.it\/ . Accessed 25 Oct 2014"},{"key":"10_CR7","unstructured":"Flyspeck project, September 2014. http:\/\/aperiodical.com\/2014\/09\/the-flyspeck-project-is-complete-we-know-how-to-stack-balls"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-32621-9_1","volume-title":"Logic, Language, Information and Computation","author":"A Asperti","year":"2012","unstructured":"Asperti, A., Ricciotti, W.: Formalizing turing machines. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 1\u201325. Springer, Heidelberg (2012)"},{"key":"10_CR9","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: Automating G\u00f6del\u2019s ontological proof of God\u2019s existence with higher-order automated theorem provers. In: Schaub, T., Friedrich, G., O\u2019Sullivan, B. (eds.) ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93\u201398. IOS Press (2014)"},{"key":"10_CR10","unstructured":"Du Bois-Reymond, E.H.: \u00dcber die Grenzen des Naturerkennens; Die sieben Weltr\u00e4thsel, zwei Vortr\u00e4ge. Von Veit, Leipzig (1898)"},{"key":"10_CR11","volume-title":"Theory of Sets. Elements of Mathematics","author":"N Bourbaki","year":"1968","unstructured":"Bourbaki, N.: Theory of Sets. Elements of Mathematics. Springer, Heidelberg (1968)"},{"key":"10_CR12","doi-asserted-by":"crossref","first-page":"vii","DOI":"10.1016\/S0167-5060(08)70408-4","volume-title":"Theories of Computational Complexity","author":"Cristian Calude","year":"1988","unstructured":"Calude, C.: Theories of Computational Complexity, North-Holland, Amsterdam (1988)"},{"key":"10_CR13","first-page":"167","volume":"84","author":"CS Calude","year":"2004","unstructured":"Calude, C.S., Calude, E., Marcus, S.: Passages of proof. Bull. Eur. Assoc. Theor. Comput. Sci. 84, 167\u2013188 (2004)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1093\/jigpal\/jzp015","volume":"17","author":"CS Calude","year":"2009","unstructured":"Calude, C.S., Hay, N.J.: Every computably enumerable random real is provably computably enumerable random. Logic J. IGPL 17, 325\u2013350 (2009)","journal-title":"Logic J. IGPL"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-02614-0_20","volume-title":"Intelligent Computer Mathematics","author":"CS Calude","year":"2009","unstructured":"Calude, C.S., M\u00fcller, C.: Formal proof: reconciling correctness and understanding. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 217\u2013232. Springer, Heidelberg (2009)"},{"key":"10_CR16","volume-title":"Computability Theory","author":"SB Cooper","year":"2004","unstructured":"Cooper, S.B.: Computability Theory. Chapman Hall\/CRC, London (2004)"},{"issue":"4","key":"10_CR17","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/2892710","volume":"59","author":"C Edwards","year":"2016","unstructured":"Edwards, C.: Automated proofs. Math struggles with the usability of formal proofs. Commun. ACM 59(4), 13\u201315 (2016)","journal-title":"Commun. ACM"},{"issue":"2","key":"10_CR18","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1093\/philmat\/nkj003","volume":"14","author":"S Feferman","year":"2006","unstructured":"Feferman, S.: Are there absolutely unsolvable problems? G\u00f6del\u2019s dichotomy. Philosophia Math. 14(2), 134\u2013152 (2006)","journal-title":"Philosophia Math."},{"key":"10_CR19","unstructured":"G\u00f6del, K.: Some basic theorems on the foundations of mathematics and their implications. In: Feferman, S., Dawson Jr., J.W., Goldfarb, W., Parsons, C., Solovay, R.M. (eds.) Collected Works. Unpublished Essays and Lectures. vol. III, pp. 304\u2013323. Oxford University Press (1995)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Gordon, M.: From LCF to HOL: a short history. In: Proof, Language, and Interaction, pp. 169\u2013186 (2000)","DOI":"10.7551\/mitpress\/5641.003.0012"},{"issue":"3","key":"10_CR21","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","volume":"162","author":"TC Hales","year":"2005","unstructured":"Hales, T.C.: A proof of the Kepler conjecture. Ann. Math. 162(3), 1065\u20131185 (2005)","journal-title":"Ann. Math."},{"key":"10_CR22","unstructured":"Hern\u00e1ndez-Orozco, S., Hern\u00e1ndez-Quiroz, F., Zenil, H., Sieg, W.: Rare speed-up in automatic theorem proving reveals tradeoff between computational time and information value (2015). http:\/\/arxiv.org\/abs\/1506.04349"},{"key":"10_CR23","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"Marijn J. H. Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean Pythagorean triples problem via cube-and-conquer (2016). http:\/\/arxiv.org\/abs\/1605.00723v1 [cs.DM]"},{"key":"10_CR24","unstructured":"Hilbert, D.: Hilbert\u2019s 1930 radio speech. https:\/\/www.youtube.com\/watch?v=EbgAu_X2mm4"},{"key":"10_CR25","unstructured":"Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)"},{"key":"10_CR26","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u00f6s discrepancy conjecture (2014). http:\/\/arxiv.org\/abs\/1402.2184v2"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Verification then and now. In: De Pauli-Schimanovich, W., Koehler, E., Stadler, F. (eds.) The Foundational Debate, Complexity and Constructivity in Mathematics and Physics, pp. 187\u2013196. Kluwer, Dordrecht (1995)","DOI":"10.1007\/978-94-017-3327-4_14"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-22863-6_22","volume-title":"Interactive Theorem Proving","author":"M Norrish","year":"2011","unstructured":"Norrish, M.: Mechanised computability theory. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 297\u2013311. Springer, Heidelberg (2011)"},{"key":"10_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02460-7","volume-title":"Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets","author":"RI Soare","year":"1987","unstructured":"Soare, R.I.: Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets. Springer, Heidelberg (1987)"},{"key":"10_CR30","unstructured":"Szasz, N.: A machine checked proof that Ackermann\u2019s function is not primitive recursive. In: Huet, G. (ed.) Logical Environments, pp. 31\u20137. University Press (1991)"},{"key":"10_CR31","unstructured":"Tao, T.: The Erd\u00f6s discrepancy problem (2015). http:\/\/arxiv.org\/abs\/1509.05363v5"},{"key":"10_CR32","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley and Los Angeles (1951)"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-319-21819-9_22","volume-title":"Unconventional Computation and Natural Computation","author":"D Thompson","year":"2015","unstructured":"Thompson, D.: Formalisation vs. understanding. In: Calude, C.S., Dinneen, M.J. (eds.) UCNC 2015. LNCS, vol. 9252, pp. 290\u2013300. Springer, Heidelberg (2015)"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-39634-2_13","volume-title":"Interactive Theorem Proving","author":"J Xu","year":"2013","unstructured":"Xu, J., Zhang, X., Urban, C.: Mechanising turing machines and computability theory in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 147\u2013162. Springer, Heidelberg (2013)"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0105420","volume-title":"Theorem Proving in Higher Order Logics","author":"V Zammit","year":"1996","unstructured":"Zammit, V.: A mechanisation of computability theory in HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996)"},{"key":"10_CR36","unstructured":"Zammit, V.: On the Readability of Machine Checkable Formal Proofs. Ph.D. Thesis, University of Kent, March 1999"}],"container-title":["Lecture Notes in Computer Science","Computer Algebra in Scientific Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45641-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,19]],"date-time":"2024-06-19T07:52:45Z","timestamp":1718783565000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45641-6_10"}},"subtitle":["(Invited Talk)"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319456409","9783319456416"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45641-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 September 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CASC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Computer Algebra in Scientific Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bucharest","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Romania","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"casc2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}