{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:08Z","timestamp":1725533828902},"publisher-location":"Berlin, Heidelberg","reference-count":68,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026133"},{"type":"electronic","value":"9783642026140"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02614-0_20","type":"book-chapter","created":{"date-parts":[[2009,7,2]],"date-time":"2009-07-02T11:47:24Z","timestamp":1246535244000},"page":"217-232","source":"Crossref","is-referenced-by-count":4,"title":["Formal Proof: Reconciling Correctness and Understanding"],"prefix":"10.1007","author":[{"given":"Cristian S.","family":"Calude","sequence":"first","affiliation":[]},{"given":"Christine","family":"M\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"AFP. Archive of formal proofs (March 2009), http:\/\/afp.sourceforge.net"},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof general: A generic tool for proof development. In: Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp. 38\u201342. Springer, Heidelberg (2000)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Audebaud, P., Rideau, L.: TeXMacs as authoring tool for publication and dissemination of formal developments. In: Aspinall, D., Lueth, C. (eds.) User-Interface for Theorem Provers. Electronic Notes in Theoretical Computer Science, vol.\u00a0103, pp. 27\u201348 (2004)","DOI":"10.1016\/j.entcs.2004.09.012"},{"key":"20_CR4","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11618027_9","volume-title":"Mathematical Knowledge Management","author":"S. Autexier","year":"2006","unstructured":"Autexier, S., Benzm\u00fcller, C., Dietrich, D., Meier, A., Wirth, C.-P.: A generic modular data structure for proof attempts alternating on ideas and granularity. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 126\u2013142. Springer, Heidelberg (2006)"},{"key":"20_CR5","series-title":"LNAI","volume-title":"Intelligent Computer Mathematics","year":"2008","unstructured":"Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.): AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol.\u00a05144. Springer, Heidelberg (2008)"},{"key":"20_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-540-73086-6_16","volume-title":"Towards Mechanized Mathematical Assistants","author":"S. Autexier","year":"2007","unstructured":"Autexier, S., Fiedler, A., Neumann, T., Wagner, M.: Supporting user-defined notations when integrating scientific text-editors with proof assistance systems. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 176\u2013190. Springer, Heidelberg (2007)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Autexier, S., Benzm\u00fcller, C., Dietrich, D., Wagner, M.: Organisation, transformation, and propagation of mathematical knowledge in \u03a9mega. Journal of Mathematics in Computer Science (accepted, 2009)","DOI":"10.1007\/s11786-008-0054-6"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1093\/acprof:oso\/9780199296453.003.0013","volume-title":"The Philosophy of Mathematical Practice","author":"J. Avigad","year":"2008","unstructured":"Avigad, J.: Understanding proofs. In: Mancosu, P. (ed.) The Philosophy of Mathematical Practice, pp. 317\u2013353. Oxford University Press, Oxford (2008)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Berners-Lee, T., Fielding, R., Masinter, L.: Uniform Resource Identifier (URI): Generic Syntax. RFC 3986, Internet Engineering Task Force (2005)","DOI":"10.17487\/rfc3986"},{"key":"20_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"20_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":"20_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565663","volume-title":"Varieties of Constructive Mathematics","author":"D. Bridges","year":"1987","unstructured":"Bridges, D., Richman, F.: Varieties of Constructive Mathematics. Cambridge University Press, Cambridge (1987)"},{"key":"20_CR13","first-page":"178","volume-title":"Computational Logic \u2013 Essays in Honor of A. Robinson","author":"A. Bundy","year":"1989","unstructured":"Bundy, A.: A science of reasoning. In: Lassez, J.L., Plotkin, G. (eds.) Computational Logic \u2013 Essays in Honor of A. Robinson, pp. 178\u2013198. MIT Press, Cambridge (1989)"},{"key":"20_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04978-5","volume-title":"Information and Randomness: An Algorithmic Perspective","author":"C.S. Calude","year":"2002","unstructured":"Calude, C.S.: Information and Randomness: An Algorithmic Perspective, 2nd edn. Springer, Heidelberg (2002)","edition":"2"},{"key":"20_CR15","first-page":"167","volume":"84","author":"C.S. Calude","year":"2004","unstructured":"Calude, C.S., Calude, E., Marcus, S.: Passages of proof. Bull. Eur. Assoc. Theor. Comput. Sci. EATCS\u00a084, 167\u2013188 (2004)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci. EATCS"},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1142\/6577","volume-title":"Randomness and Complexity, From Leibniz to Chaitin","author":"C.S. Calude","year":"2007","unstructured":"Calude, C.S., Calude, E., Marcus, S.: Proving and programming. In: Calude, C. (ed.) Randomness and Complexity, From Leibniz to Chaitin, pp. 310\u2013321. World Scientific, Singapore (2007)"},{"issue":"6","key":"20_CR17","doi-asserted-by":"publisher","first-page":"1937","DOI":"10.1142\/S0218127407018130","volume":"17","author":"C.S. Calude","year":"2007","unstructured":"Calude, C.S., Dinneen, M.J.: Exact approximations of Omega numbers. Int. Journal of Bifurcation & Chaos\u00a017(6), 1937\u20131954 (2007)","journal-title":"Int. Journal of Bifurcation & Chaos"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-27812-2_2","volume-title":"Theory Is Forever","author":"C.S. Calude","year":"2004","unstructured":"Calude, C.S., Marcus, S.: Mathematical proofs at a crossroad? In: Karhum\u00e4ki, J., Maurer, H., P\u0103un, G., Rozenberg, G. (eds.) Theory Is Forever. LNCS, vol.\u00a03113, pp. 15\u201328. Springer, Heidelberg (2004)"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Calude, C.S., Hay, N.J.: Every Computably Enumerable Random Real Is Provably Computably Enumerable Random. Research Report of CDMTCS-328 (July 2008)","DOI":"10.1093\/jigpal\/jzp015"},{"key":"20_CR20","volume-title":"The Limits of Mathematics","author":"G.J. Chaitin","year":"1998","unstructured":"Chaitin, G.J.: The Limits of Mathematics. Springer, Heidelberg (1998)"},{"key":"20_CR21","unstructured":"Chaitin, G.J.: Meta Math! Pantheon (2005)"},{"key":"20_CR22","unstructured":"Cheikhrouhou, L., Sorge, V.: PDS \u2013 a three-dimensional data structure for proof plans. In: Proceedings of the International Conference on Artificial and Computational Intelligence for Decision, Control and Automation in Engineering and Industrial Applications (ACIDCA 2000), pp. 144\u2013149 (2000)"},{"key":"20_CR23","volume-title":"Set Theory and the Continuum Hypothesis","author":"P.J. Cohen","year":"1966","unstructured":"Cohen, P.J.: Set Theory and the Continuum Hypothesis. Addison-Wesley, Reading (1966)"},{"key":"20_CR24","unstructured":"Cooper, S.B.: Computability Theory. Chapman &Hall\/CRC (2004)"},{"volume-title":"Kurt G\u00f6del Collected Works","year":"1986","key":"20_CR25","unstructured":"Feferman, S., Dawson Jr., J., Kleene, S.C., Moore, G.H., Solovay, R.M., van Heijenoort, J., Velleman, D.J. (eds.): Kurt G\u00f6del Collected Works. Oxford University Press, Oxford (1986)"},{"key":"20_CR26","unstructured":"Fiedler, A.: User-adaptive Proof Explanation. PhD Thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (2001)"},{"key":"20_CR27","unstructured":"Giceva, J.: Capturing Rhetorical Aspects in Mathematical Documents using OMDoc and SALT. Technical Report, Jacobs University, Germany (2008)"},{"issue":"4","key":"20_CR28","first-page":"359","volume":"6","author":"J.A. Goguen","year":"1973","unstructured":"Goguen, J.A.: Realization is universal. Theory of Computing Systems\u00a06(4), 359\u2013374 (1973)","journal-title":"Theory of Computing Systems"},{"key":"20_CR29","unstructured":"Gonthier, G.: Formal proof \u2013 The Four-Color Theorem. Notices of the AMS\u00a0(11), 1382\u20131393 (2008)"},{"key":"20_CR30","doi-asserted-by":"publisher","DOI":"10.1093\/actrade\/9780192853615.001.0001","volume-title":"Mathematics. A Very Short Introduction","author":"T. Gowers","year":"2002","unstructured":"Gowers, T.: Mathematics. A Very Short Introduction. Oxford University Press, Oxford (2002)"},{"key":"20_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-21593-8","volume-title":"Fixed Point Theory","author":"A. Granas","year":"2003","unstructured":"Granas, A., Dugundji, J.: Fixed Point Theory. Springer, Heidelberg (2003)"},{"key":"20_CR32","unstructured":"Hales, T.C.: Formal proof. Notices of the AMS\u00a0(11), 1370\u20131380 (2008)"},{"key":"20_CR33","unstructured":"Harrison, J.: Formal proof \u2013 theory and practice. Notices of the AMS\u00a0(11), 1395\u20131406 (2008)"},{"key":"20_CR34","unstructured":"Hay, N.J.: Formal Proof for the Kraft-Chaitin Theorem (March 2009), http:\/\/www.cs.auckland.ac.nz\/~nickjhay\/KraftChaitin.thy"},{"key":"20_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11826095","volume-title":"OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]","author":"M. Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]. LNCS, vol.\u00a04180. Springer, Heidelberg (2006)"},{"key":"20_CR36","unstructured":"Kohlhase, M.: XSLT Stylesheet for converting OMDoc documents into XHTML (January 2008), http:\/\/kwarc.info\/projects\/xslt"},{"issue":"2","key":"20_CR37","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1023\/A:1004918402670","volume":"111","author":"S.M. Lane","year":"1997","unstructured":"Lane, S.M.: Despite physicists, proof is essential in mathematics. Synthese\u00a0111(2), 147\u2013154 (1997)","journal-title":"Synthese"},{"key":"20_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"832","DOI":"10.1007\/978-3-540-68234-9_68","volume-title":"The Semantic Web: Research and Applications","author":"C. Lange","year":"2008","unstructured":"Lange, C.: SWiM \u2013 a semantic wiki for mathematical knowledge management. In: Bechhofer, S., Hauswirth, M., Hoffmann, J., Koubarakis, M. (eds.) ESWC 2008. LNCS, vol.\u00a05021, pp. 832\u2013837. Springer, Heidelberg (2008)"},{"key":"20_CR39","unstructured":"Leedham-Green, C.: Personal communication to C. M\u00fcller, March 7 (2009)"},{"key":"20_CR40","volume-title":"The Pythagorean Proposition","author":"E.S. Loomis","year":"1968","unstructured":"Loomis, E.S.: The Pythagorean Proposition, 2nd edn. Oxford University Press, Oxford (1968)","edition":"2"},{"key":"20_CR41","unstructured":"Manin, Y.I.: Mathematics as Metaphor. American Mathematical Society (2007)"},{"key":"20_CR42","unstructured":"Manola, F., Miller, E.: RDF Primer. W3C Recommendation, World Wide Web Consortium (February 2004)"},{"issue":"2","key":"20_CR43","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1023\/A:1005936130801","volume":"22","author":"E. Melis","year":"1999","unstructured":"Melis, E., Whittle, J.: Analogy in inductive theorem proving. Journal of Automated Reasoning\u00a022(2), 117\u2013147 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR44","unstructured":"Mizar (March 2009), http:\/\/web.cs.ualberta.ca\/~piotr\/Mizar"},{"key":"20_CR45","unstructured":"M\u00fcller, C., Kohlhase, M.: Panta rhei. In: Hinneburg (ed.) LWA Conference Proceedings, pp. 318\u2013323. Martin-Luther-University (2007)"},{"key":"20_CR46","unstructured":"Nelson, E.: Syntax and Semantics (March 2009), http:\/\/www.math.princeton.edu\/~nelson\/papers\/s.pdf"},{"key":"20_CR47","first-page":"230","volume-title":"Software Engineering and Formal Methods (SEFM 2004)","author":"S. Berghofer","year":"2004","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Cuellar, J., Liu, Z. (eds.) Software Engineering and Formal Methods (SEFM 2004), pp. 230\u2013239. IEEE Computer Society, Los Alamitos (2004)"},{"key":"20_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"20_CR49","unstructured":"Normann, I.: Theory Morphisms. PhD Thesis, Jacobs University, Germany (2008)"},{"key":"20_CR50","unstructured":"OpenMathHome (March 2007), http:\/\/www.openmath.org"},{"key":"20_CR51","volume-title":"Mathematics and Plausible Reasoning Volume I: Induction and Analogy in Mathematics","author":"G. P\u00f3lya","year":"1969","unstructured":"P\u00f3lya, G.: Mathematics and Plausible Reasoning Volume I: Induction and Analogy in Mathematics. Princeton University Press, Princeton (1969)"},{"key":"20_CR52","unstructured":"Prud\u2019hommeaux, E., Seaborne, A.: SPARQL Query Language for RDF. W3C Recommendation (March 2009), http:\/\/www.w3.org\/TR\/2008\/REC-rdf-sparql-query-20080115\/"},{"key":"20_CR53","unstructured":"Rabe, F.: Representing Logics and Logic Translations. PhD Thesis, Jacobs University, Germany (2008)"},{"key":"20_CR54","doi-asserted-by":"crossref","unstructured":"Schiller, M., Dietrich, D., Benzm\u00fcller, C.: Proof step analysis for proof tutoring \u2013 a learning approach to granularity. Teaching Mathematics and Computer Science (in press) (2009)","DOI":"10.5485\/TMCS.2008.0183"},{"key":"20_CR55","volume-title":"Group Theory","author":"W.R. Scott","year":"1987","unstructured":"Scott, W.R.: Group Theory. Dover, New York (1987)"},{"key":"20_CR56","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-94-017-0253-9_11","volume-title":"Thirty Five Years of Automating Mathematics","author":"J. Siekmann","year":"2003","unstructured":"Siekmann, J., Benzm\u00fcller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M.: Proof development in OMEGA: The irrationality of square root of 2. In: Kamareddine, F. (ed.) Thirty Five Years of Automating Mathematics, pp. 271\u2013314. Kluwer, Dordrecht (2003)"},{"key":"20_CR57","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/3-540-36078-6_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Siekmann","year":"2002","unstructured":"Siekmann, J., Benzm\u00fcller, C., Fiedler, A., Meier, A., Pollet, M.: Proof development with Omega: Sqrt(2) is irrational. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 367\u2013387. Springer, Heidelberg (2002)"},{"issue":"3","key":"20_CR58","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1970696","volume":"38","author":"R.M. Solovay","year":"1970","unstructured":"Solovay, R.M.: A model of set-theory in which every set of reals is Lebesgue measurable. Annals of Mathematics\u00a038(3), 1\u201356 (1970)","journal-title":"Annals of Mathematics"},{"key":"20_CR59","unstructured":"Gnu TeXMacs (March 2009), http:\/\/www.texM.s.org"},{"key":"20_CR60","unstructured":"vdash: A Formal Math Wiki (March 2009), http:\/\/www.vdash.org"},{"issue":"3","key":"20_CR61","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2004.10.027","volume":"125","author":"T. Weber","year":"2005","unstructured":"Weber, T.: Bounded model generation for isabelle\/hol. Electronic Notes in Theoretical Computer Science\u00a0125(3), 103\u2013116 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"20_CR62","unstructured":"Wenzel, M.: Personal communication to C. M\u00fcller, March 7 (2009)"},{"key":"20_CR63","unstructured":"Wenzel, M.: Isabelle\/Isar \u2013 a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol.\u00a010(23), pp. 277\u2013298. University of Bia\u0142ystok (2007)"},{"key":"20_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M.T. Wenzel","year":"1999","unstructured":"Wenzel, M.T.: Isar \u2013 a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013184. Springer, Heidelberg (1999)"},{"key":"20_CR65","volume-title":"Principia Mathematica","author":"A.N. Whitehead","year":"1910","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica, 2nd edn., vol.\u00a0I. Cambridge University Press, Cambridge (1910)","edition":"2"},{"key":"20_CR66","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Formal proof \u2013 getting started. AMS Notices\u00a0(11), 1408\u20131414 (2008)","DOI":"10.5040\/9781501303920.ch-002"},{"key":"20_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-540-25931-2_57","volume-title":"Diagrammatic Representation and Inference","author":"D. Winterstein","year":"2004","unstructured":"Winterstein, D., Bundy, A., Gurr, C., Jamnik, M.: An experimental comparison of diagrammatic and algebraic logics. In: Blackwell, A.F., Marriott, K., Shimojima, A. (eds.) Diagrams 2004. LNCS, vol.\u00a02980, pp. 432\u2013434. Springer, Heidelberg (2004)"},{"key":"20_CR68","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172011","volume-title":"An Introduction to Hilbert Space","author":"N. Young","year":"1988","unstructured":"Young, N.: An Introduction to Hilbert Space. Cambridge University Press, Cambridge (1988)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02614-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T21:34:42Z","timestamp":1685050482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02614-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026133","9783642026140"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02614-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}