{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:33:00Z","timestamp":1725485580471},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_25","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:48:36Z","timestamp":1180666116000},"page":"367-387","source":"Crossref","is-referenced-by-count":6,"title":["Proof Development with \u03a9MEGA: \u221a2 Is Irrational"],"prefix":"10.1007","author":[{"given":"J.","family":"Siekmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Benzm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Fiedler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Meier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Pollet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"S. Allen, R. Constable, R. Eaton, C. Kreitz, and L. Lorigo. The Nuprl open logical environment. In McAllester [29].","DOI":"10.1007\/10721959_12"},{"issue":"3","key":"25_CR2","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P. Andrews","year":"1996","unstructured":"P. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321\u2013353, 1996.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR3","unstructured":"R. Bartle and D. Sherbert. Introduction to Real Analysis. Wiley, 2 edition, 1982."},{"key":"25_CR4","unstructured":"C. Benzm\u00fcller. Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Department of Computer Science, Saarland University, 1999."},{"key":"25_CR5","first-page":"188","volume":"5","author":"C. Benzm\u00fcller","year":"1999","unstructured":"C. Benzm\u00fcller, M. Bishop, and V. Sorge. Integrating TPS and \u03a9mega. Journal of Universal Computer Science, 5:188\u2013207, 1999.","journal-title":"Journal of Universal Computer Science"},{"key":"25_CR6","unstructured":"C. Benzm\u00fcller, A. Fiedler, A. Meier, and M. Pollet. Irrationality of \u221a2 - a case study in \u03a9mega. Seki-Report SR-02-03, Department of Computer Science, Saarland University, 2002."},{"key":"25_CR7","series-title":"LNAI","volume-title":"Proceedings of the 15th International Conference on Automated Deduction (CADE-15)","author":"C. Benzm\u00fcller","year":"1998","unstructured":"C. Benzm\u00fcller and M. Kohlhase. LEO-a higher-order theorem prover. In Proceedings of the 15th International Conference on Automated Deduction (CADE-15), LNAI, LINDAU, Germany, 1998."},{"key":"25_CR8","unstructured":"C. Benzm\u00fcller, A. Meier, and V. Sorge. Bridging theorem proving and mathematical knowledge retrieval. In Festschrift in Honour of J\u00f6rg Siekmann\u2019s 60s Birthday, LNAI, 2002."},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller and V. Sorge. A blackboard architecture for guiding interactive proofs. In Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA\u2019 98), LNAI, Sozopol, Bulgaria, 1998.","DOI":"10.1007\/BFb0057438"},{"key":"25_CR10","unstructured":"C. Benzm\u00fcller and V. Sorge. \u03a9-Ants-An open approach at combining Interactive and Automated Theorem Proving. In M. Kerber and M. Kohlhase, editors, Proceedings of the 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus-2000). AK Peters, 2001."},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"M. Bishop and P. Andrews. Selectively instantiating definitions. In H. Kirchner, editors. Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI. Springer Verlag, 1998. Kirchner and Kirchner [26].","DOI":"10.1007\/BFb0054272"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. Bledsoe","year":"1990","unstructured":"W. Bledsoe. Challenge problems in elementary calculus. Journal of Automated Reasoning, 6:341\u2013359, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"Proceedings of the 9th Conference on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th Conference on Automated Deduction, number 310 in LNCS, pages 111\u2013120, Argonne, Illinois, USA, 1988. Springer Verlag."},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"A. Bundy, editor. Proceedings of the 12th Conference on Automated Deduction, number 814 in LNAI, Nancy, France, 1994. Springer Verlag.","DOI":"10.1007\/3-540-58156-1"},{"key":"25_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-6996-1","volume-title":"First leaves: a tutorial introduction to Maple V","author":"B. Char","year":"1992","unstructured":"B. Char, K. Geddes, G. Gonnet, B. Leong, M. Monagan, and S. Watt. First leaves: a tutorial introduction to Maple V. Springer Verlag, Berlin, 1992."},{"key":"25_CR16","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0057443","volume-title":"Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA\u2019 98)","author":"L. Cheikhrouhou","year":"1998","unstructured":"L. Cheikhrouhou and J. Siekmann. Planning diagonalization proofs. In F. Giunchiglia, editor, Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA\u2019 98), pages 167\u2013180, Sozopol, Bulgaria, 1998. Springer Verlag, Berlin, Germany, LNAI 1480."},{"key":"25_CR17","unstructured":"L. Cheikhrouhou and V. Sorge. PDS-A Three-Dimensional Data Structure for Proof Plans. In Proceedings of the International Conference on Artificial and Computational Intelligence (ACIDCA\u20192000), 2000."},{"key":"25_CR18","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"The Journal of Symbolic Logic"},{"key":"25_CR19","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA. see http:\/\/coq.inria.fr\/doc\/main.html ."},{"key":"25_CR20","unstructured":"A. Fiedler. P.rex: An interactive proof explainer. In R. Gor\u00e9, A. Leitsch, and T. Nipkow, editors, Automated Reasoning-1st International Joint Conference, IJCAR 2001, number 2083 in LNAI. Springer, 2001."},{"key":"25_CR21","series-title":"PhD thesis","volume-title":"User-adaptive proof explanation","author":"A. Fiedler","year":"2001","unstructured":"A. Fiedler. User-adaptive proof explanation. PhD thesis, Naturwissenschaftlich-Technische Fakult\u00e4t I, Saarland University, Saarbr\u00fccken, Germany, 2001."},{"key":"25_CR22","unstructured":"A. Franke and M. Kohlhase. System description: MBase, an open mathematical knowledge base. In McAllester [29]."},{"key":"25_CR23","volume-title":"Master\u2019s thesis","author":"H. Gebhard","year":"1999","unstructured":"H. Gebhard. Beweisplanung f\u00fcr die beweise der vollst\u00e4ndigkeit verschiedener reso-lutionskalk\u00fcle in \u03a9mega. Master\u2019s thesis, Saarland University, Saarbr\u00fccken, Germany, 1999."},{"key":"25_CR24","unstructured":"M. Gordon and T. Melham. Introduction to HOL-A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"X. Huang. Reconstructing Proofs at the Assertion Level. In Bundy [14], pages 738\u2013752.","DOI":"10.1007\/3-540-58156-1_53"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner, editors. Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI. Springer Verlag, 1998.","DOI":"10.1007\/BFb0054239"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"H. Kirchner and C. Ringeissen, editors. Frontiers of combining systems: Third International Workshop, FroCoS 2000, volume 1794 of LNAI. Springer, 2000.","DOI":"10.1007\/10720084"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"M. Kohlhase and A. Franke. MBase: Representing knowledge and context for the integration of mathematical software systems. Journal of Symbolic Computation; Special Issue on the Integration of Computer algebra and Deduction Systems, 32(4):365\u2013402, September 2001.","DOI":"10.1006\/jsco.2000.0468"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"D. McAllester, editor. Proceedings of the 17th Conference on Automated Deduction, number 1831 in LNAI. Springer, 2000.","DOI":"10.1007\/10721959"},{"key":"25_CR30","unstructured":"A. Meier. TRAMP: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In McAllester [29]."},{"key":"25_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"494","DOI":"10.1007\/3-540-45654-6_39","volume-title":"A Selection of Papers from the 8th International Workshop on Computer Aided Systems Theory (Euro-CAST 2001)","author":"A. Meier","year":"2001","unstructured":"A. Meier, M. Pollet, and V. Sorge. Classifying Isomorphic Residue Classes. In R. Moreno-Diaz, B. Buchberger, and J.-L. Freire, editors, A Selection of Papers from the 8th International Workshop on Computer Aided Systems Theory (Euro-CAST 2001), volume 2178 of LNCS, pages 494\u2013508. Springer Verlag, 2001."},{"key":"25_CR32","doi-asserted-by":"crossref","unstructured":"A. Meier, M. Pollet, and V. Sorge. Comparing approaches to the exploration of the domain of residue classes. Journal of Symbolic Computation, forthcoming.","DOI":"10.1006\/jsco.2002.0550"},{"key":"25_CR33","unstructured":"E. Melis. Island planning and refinement. Seki-Report SR-96-10, Department of Computer Science, Saarland University, 1996."},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"E. Melis and A. Meier. Proof planning with multiple strategies. In J. Loyd, V. Dahl, U. Furbach, M. Kerber, K. Lau, C. Palamidessi, L.M. Pereira, Y. Sagi-vand, and P. Stuckey, editors, Proceedings of the First International Conference on Computational Logic, volume 1861 of LNAI, pages 644\u2013659. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44957-4_43"},{"issue":"1","key":"25_CR35","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0004-3702(99)00076-4","volume":"115","author":"E. Melis","year":"1999","unstructured":"E. Melis and J. Siekmann. Knowledge-based proof planning. Artificial Intelligence, 115(1):65\u2013105, 1999.","journal-title":"Artificial Intelligence"},{"key":"25_CR36","doi-asserted-by":"crossref","unstructured":"E. Melis, J. Zimmer, and T. M\u00fcller. Integrating constraint solving into proof planning. In C. Ringeissen, editors. Frontiers of combining systems: Third International Workshop, FroCoS 2000, volume 1794 of LNAI. Springer, 2000. Kirchner and Ringeissen [27].","DOI":"10.1007\/10720084_3"},{"key":"25_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer-Aided Verification, CAV\u2019 96","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T. Henzinger, editors, Computer-Aided Verification, CAV\u2019 96, volume 1102 of LNCS, pages 411\u2013414, New Brunswick, NJ, 1996. Springer-Verlag."},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"J. Richardson, A. Smaill, and I. Green. System description: Proof planning in higher-order logic with \u03bbclam. In H. Kirchner, editors. Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI. Springer Verlag, 1998. Kirchner and Kirchner [26].","DOI":"10.1007\/BFb0054254"},{"key":"25_CR39","volume-title":"GAP-Groups, Algorithms, and Programming","author":"M. Sch\u00f6nert","year":"1995","unstructured":"M. Sch\u00f6nert et a1. GAP-Groups, Algorithms, and Programming. Lehrstuhl D f\u00fcr Mathematik, Rheinisch Westf\u00e4lische Technische Hochschule, Aachen, Germany, 1995."},{"key":"25_CR40","unstructured":"J. Siekmann, C. Benzm\u00fcller, V. Brezhnev, L. Cheikhrouhou, A. Fiedler, A. Franke, H. Horacek, M. Kohlhase, A. Meier, E. Melis, M. Moschner, I. Normann, M. Pollet, V. Sorge, C. Ullrich, C.-P. Wirth, and J. Zimmer. Proof development with \u03a9mega. In Voronkov [47], pages 143\u2013148. See http:\/\/www.ags.uni-sb.de\/~omega\/ ."},{"key":"25_CR41","doi-asserted-by":"crossref","unstructured":"J. Siekmann, C. Benzm\u00fcller, A. Fiedler, A. Meier, and M. Pollet. Proof development with \u03a9mega: \u221a2 is not rational. Special Issue of Journal of Automated Reasoning, 2002. Submitted.","DOI":"10.1007\/3-540-36078-6_25"},{"key":"25_CR42","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/s001650050053","volume":"11","author":"J. Siekmann","year":"1999","unstructured":"J. Siekmann, S. Hess, C. Benzm\u00fcller, L. Cheikhrouhou, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, M. Pollet, and V. Sorge. LOUI: Lovely \u03a9mega User Interface. Formal Aspects of Computing, 11:326\u2013342, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"25_CR43","doi-asserted-by":"crossref","unstructured":"V. Sorge. Non-Trivial Computations in Proof Planning. In C. Ringeissen, editors. Frontiers of combining systems: Third International Workshop, FroCoS 2000, volume 1794 of LNAI. Springer, 2000. Kirchner and Ringeissen [27].","DOI":"10.1007\/10720084_9"},{"key":"25_CR44","series-title":"PhD thesis","volume-title":"\u03a9-Ants-A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning","author":"V. Sorge","year":"2001","unstructured":"V. Sorge. \u03a9-Ants-A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, Saarland University, Saarbr\u00fccken, Germany, 2001."},{"key":"25_CR45","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In Bundy [14].","DOI":"10.1007\/3-540-58156-1_18"},{"key":"25_CR46","unstructured":"The \u03a9mega group. POST. See at http:\/\/www.ags.uni-sb.de\/~omega\/primer\/post.html ."},{"key":"25_CR47","doi-asserted-by":"crossref","unstructured":"A. Voronkov, editor. Proceedings of the 18th International Conference on Automated Deduction, number 2392 in LNAI. Springer Verlag, 2002.","DOI":"10.1007\/3-540-45620-1"},{"key":"25_CR48","unstructured":"F. Wiedijk. The fifteen provers of the world. Unpublished Draft, 2002."},{"key":"25_CR49","unstructured":"J. Zimmer and M. Kohlhase. System description: The mathweb software bus for distributed mathematical reasoning. In Voronkov [47], pages 138\u2013142."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:18:27Z","timestamp":1556464707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}