{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:03:02Z","timestamp":1725566582045},"publisher-location":"Berlin, Heidelberg","reference-count":100,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540231660"},{"type":"electronic","value":"9783540302216"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30221-6_2","type":"book-chapter","created":{"date-parts":[[2010,9,21]],"date-time":"2010-09-21T16:47:50Z","timestamp":1285087670000},"page":"3-28","source":"Crossref","is-referenced-by-count":1,"title":["\u03a9mega: Computer Supported Mathematics"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Siekmann","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Andrews, P.B., Bishop, M., Brown, C.E.: System description: TPS: A theorem proving system for type theory. In: Conference on Automated Deduction, pp. 164\u2013169 (2000)","DOI":"10.1007\/10721959_11"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2003.12.026","volume":"93","author":"S. Autexier","year":"2003","unstructured":"Autexier, S., Benzm\u00fcller, C., Fiedler, A., Horacek, H., Bao Vo, Q.: Assertion-level proof representation with under-specification. Electronic in Theoretical Computer Science\u00a093, 5\u201323 (2003)","journal-title":"Electronic in Theoretical Computer Science"},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P.B. Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning\u00a016(3), 321\u2013353 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Allen, S., Constable, R., Eaton, R., Kreitz, C., Lorigo, L.: The Nuprl open logical environment. In: McAllester [McA00]","DOI":"10.1007\/10721959_12"},{"key":"2_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36078-6_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Autexier","year":"2002","unstructured":"Autexier, S., Hutter, D.: Maintenance of formal software development by stratified verification. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, Springer, Heidelberg (2002)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-45719-4_34","volume-title":"Algebraic Methodology and Software Technology","author":"S. Autexier","year":"2002","unstructured":"Autexier, S., Hutter, D., Mossakowski, T., Schairer, A.: The development graph manager MAYA. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, p. 495. Springer, Heidelberg (2002)"},{"key":"2_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-45988-X_2","volume-title":"Frontiers of Combining Systems","author":"S. Autexier","year":"2002","unstructured":"Autexier, S., Mossakowski, T.: Integrating HOL-CASL into the development graph manager MAYA. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol.\u00a02309, pp. 2\u201317. Springer, Heidelberg (2002)"},{"key":"2_CR8","unstructured":"Autexier, S.: Hierarchical Contextual Reasoning. PhD thesis, Computer Science Department, Saarland University, Saarbr\u00fccken, Germany (2003) (forthcoming)"},{"key":"2_CR9","first-page":"188","volume":"5","author":"C. Benzm\u00fcller","year":"1999","unstructured":"Benzm\u00fcller, C., Bishop, M., Sorge, V.: Integrating TPS and \u03a9mega. Journal of Universal Computer Science\u00a05, 188\u2013207 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"2_CR10","unstructured":"Benzm\u00fcller, C.: Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany (1999)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U.: PROTEIN, a PROver with a Theory INterface. In: Bundy [Bun94], pp. 769\u2013773","DOI":"10.1007\/3-540-58156-1_57"},{"key":"2_CR12","unstructured":"Benzm\u00fcller, C., Fiedler, A., Gabsdil, M., Horacek, H., Kruijff-Korbayova, I., Pinkal, M., Siekmann, J., Tsovaltzi, D., Quoc Vo, B., Wolska, M.: Tutorial dialogs on mathematical proofs. In: Proceedings of IJCAI-03 Workshop on Knowledge Representation and Automated Reasoning for E-Learning Systems, Acapulco, Mexico, pp. 12\u201322 (2003)"},{"key":"2_CR13","unstructured":"Benzm\u00fcller, C., Fiedler, A., Meier, A., Pollet, M.: Irrationality of $\\sqrt{2}$ \u2013 a case study in \u03a9mega. Seki-Report SR-02-03, Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany (2002)"},{"issue":"1-3","key":"2_CR14","first-page":"3","volume":"38","author":"B. Buchberger","year":"2003","unstructured":"Buchberger, B., Gonnet, G., Hazewinkel, M.: Special issue on mathematical knowledge management. Annals of Mathematics and Artificial Intelligence\u00a038(1-3), 3\u2013232 (2003)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2_CR15","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: LEO \u2013 a higher-order theorem prover. In: Kirchner and Kirchner [KK98]"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. Bledsoe","year":"1990","unstructured":"Bledsoe, W.: Challenge problems in elementary calculus. Journal of Automated Reasoning\u00a06, 341\u2013359 (1990)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR17","unstructured":"Benzm\u00fcller, C., Meier, A., Sorge, V.: Bridging theorem proving and mathematical knowledge retrieval. In: Hutter and Stephan [HS04] (to appear)"},{"key":"2_CR18","volume-title":"Elements of Mathematics","author":"N. Bourbaki","year":"1968","unstructured":"Bourbaki, N.: Theory of sets. In: Elements of Mathematics, vol.\u00a01, Addison-Wesley, Reading (1968)"},{"key":"2_CR19","volume-title":"Introduction to Real Analysis","author":"R. Bartle","year":"1982","unstructured":"Bartle, R., Sherbert, D.: Introduction to Real Analysis, 2nd edn. Wiley, Chichester (1982)","edition":"2"},{"key":"2_CR20","unstructured":"Benzm\u00fcller, C., Sorge, V.: A blackboard architecture for guiding interactive proofs. In: Giunchiglia [Giu98]"},{"key":"2_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-48159-1_15","volume-title":"Progress in Artificial Intelligence","author":"C. Benzm\u00fcller","year":"1999","unstructured":"Benzm\u00fcller, C., Sorge, V.: Critical agents supporting interactive theorem proving. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS (LNAI), vol.\u00a01695, pp. 208\u2013221. Springer, Heidelberg (1999)"},{"key":"2_CR22","unstructured":"Benzm\u00fcller, C., Sorge, V.: \u03a9ants \u2013 An open approach at combining Interactive and Automated Theorem Proving. In: Kerber and Kohlhase[KK00]"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk and Overbeek [LO88], pp. 111\u2013120","DOI":"10.1007\/BFb0012826"},{"key":"2_CR24","first-page":"178","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"A. Bundy","year":"1991","unstructured":"Bundy, A.: A science of reasoning. In: Plotkin, G., Lasser, J.-L. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 178\u2013199. MIT Press, Cambridge (1991)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-12","year":"1994","unstructured":"Bundy, A. (ed.): CADE 1994. LNCS, vol.\u00a0814. Springer, Heidelberg (1994)"},{"key":"2_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45632-5_7","volume-title":"Computational Logic: Logic Programming and Beyond","author":"A. Bundy","year":"2002","unstructured":"Bundy, A.: A critique of proof planning. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol.\u00a02408, pp. 160\u2013177. Springer, Heidelberg (2002)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam System. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 647\u2013648. Springer, Heidelberg (1990)"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Carbonell, J., Blythe, J., Etzioni, O., Gil, Y., Joseph, R., Kahn, D., Knoblock, C., Minton, S., P\u00e9rez, M.A., Reilly, S., Veloso, M., Wang, X.: PRODIGY 4.0: The Manual and Tutorial. CMU Technical Report CMUCS- 92-150, Carnegie Mellon University (June 1992)","DOI":"10.21236\/ADA253970"},{"key":"2_CR29","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":"Char, B., Geddes, K., Gonnet, G., Leong, B., Monagan, M., Watt, S.: First leaves: a tutorial introduction to Maple V. Springer, Heidelberg (1992)"},{"key":"2_CR30","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR31","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA (1999-2003), See http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Cheikhrouhou, L., Siekmann, J.: Planning diagonalization proofs. In: Giunchiglia [Giu98], pp. 167\u2013180","DOI":"10.1007\/BFb0057443"},{"key":"2_CR33","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 (2000)"},{"volume-title":"The Undecidable: Basic Papers on undecidable Propositions, unsolvable Problems and Computable Functions","year":"1965","key":"2_CR34","unstructured":"Davis, M. (ed.): The Undecidable: Basic Papers on undecidable Propositions, unsolvable Problems and Computable Functions. Raven Press Hewlett, New York (1965)"},{"key":"2_CR35","volume-title":"Automation of Reasoning, Classical Papers on Computational Logic 1967\u20131970 of Symbolic Computation","author":"M. Davis","year":"1983","unstructured":"Davis, M.: The prehistory and early history of automated deduction. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning, Classical Papers on Computational Logic 1967\u20131970 of Symbolic Computation, vol.\u00a02, Springer, Heidelberg (1983)"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/B978-044450813-3\/50003-5","volume-title":"Handbook of Automated Reasoning","author":"M. Davis","year":"2001","unstructured":"Davis, M.: The early history of automated deduction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 1, pp. 3\u201315. Elsevier Science, Amsterdam (2001)"},{"key":"2_CR37","unstructured":"de Nivelle, H.: Bliksem 1.10 user manual. Technical report, Max-Planck- Institut f\u00fcr Informatik (1999)"},{"key":"2_CR38","unstructured":"The Doris system (2001), available at http:\/\/www.cogsci.ed.ac.uk\/jbos\/doris\/"},{"key":"2_CR39","unstructured":"Erol, K., Hendler, J., Nau, D.: Semantics for hierarchical task network planning. Technical Report CS-TR-3239, UMIACS-TR-94-31, Computer Science Department, University of Maryland (March 1994)"},{"key":"2_CR40","first-page":"1295","volume-title":"Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI)","author":"A. Fiedler","year":"2001","unstructured":"Fiedler, A.: Dialog-driven adaptation of explanations of proofs. In: Nebel, B. (ed.) Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI), Seattle, WA, pp. 1295\u20131300. Morgan Kaufmann, San Francisco (2001)"},{"key":"2_CR41","unstructured":"Fiedler, A.: P.rex: An interactive proof explainer. In: Gor\u00e9 et al. [GLN01]"},{"key":"2_CR42","unstructured":"Fiedler, A.: User-adaptive proof explanation. PhD thesis, Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany (2001)"},{"key":"2_CR43","unstructured":"Franke, A., Kohlhase, M.: System description: MBase, an open mathematical knowledge base. In: McAllester [McA00]"},{"key":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_36","volume-title":"Automated Deduction - CADE-17","author":"A. Franke","year":"2000","unstructured":"Franke, A., Kohlhase, M.: System description: Mbase, an open mathematical knowledge base. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, Springer, Heidelberg (2000)"},{"key":"2_CR45","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-16","year":"1999","unstructured":"Ganzinger, H. (ed.): CADE 1999. LNCS (LNAI), vol.\u00a01632. Springer, Heidelberg (1999)"},{"key":"2_CR46","unstructured":"H. Gebhard. Beweisplanung f\u00fcr die Beweise der Vollst\u00e4ndigkeit verschiedener Resolutionskalk\u00fcle in \u03a9mega. Master\u2019s thesis, Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany, 1999."},{"key":"2_CR47","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Artificial Intelligence: Methodology, Systems, and Applications","year":"1998","unstructured":"Giunchiglia, F. (ed.): AIMSA 1998. LNCS (LNAI), vol.\u00a01480. Springer, Heidelberg (1998)"},{"key":"2_CR48","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","year":"2001","unstructured":"Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.): IJCAR 2001. LNCS (LNAI), vol.\u00a02083. Springer, Heidelberg (2001)"},{"key":"2_CR49","volume-title":"Introduction to HOL \u2013 A theorem proving environment for higher order logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL \u2013 A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"2_CR50","unstructured":"Hadamard, J.: The Psychology of Invention in the Mathematical Field. Dover Publications, New York; edition 1949, 1944"},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"Th. Hillenbrand, A.: Jaeger, and B. L\u00f6chner. System description:Waldmeister \u2013 improvements in performance and ease of use. In: Ganzinger [Gan99], pp. 232\u2013236","DOI":"10.1007\/3-540-48660-7_20"},{"key":"2_CR52","series-title":"LNAI","volume-title":"Festschrift in Honour of J\u00f6rg Siekmann\u2019s 60s Birthday","year":"2004","unstructured":"Hutter, D., Stephan, W. (eds.): Festschrift in Honour of J\u00f6rg Siekmann\u2019s 60s Birthday. LNCS (LNAI). Springer, Heidelberg (2004) (to appear)"},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"Huang, X.: Reconstructing Proofs at the Assertion Level. In: Bundy [Bun94], pp. 738\u2013752","DOI":"10.1007\/3-540-58156-1_53"},{"key":"2_CR54","volume-title":"Proceedings of Automated Software Engineering, ASE-2000","author":"D. Hutter","year":"2000","unstructured":"Hutter, D.: Management of change in structured verification. In: Proceedings of Automated Software Engineering, ASE-2000, IEEE, Los Alamitos (2000)"},{"issue":"4","key":"2_CR55","first-page":"365","volume":"32","author":"M. Kohlhase","year":"2001","unstructured":"Kohlhase, M., Franke, A.: 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\u00a032(4), 365\u2013402 (2001)","journal-title":"Journal of Symbolic Computation; Special Issue on the Integration of Computer Algebra and Deduction Systems"},{"key":"2_CR56","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-15","year":"1998","unstructured":"Kirchner, C., Kirchner, H. (eds.): CADE 1998. LNCS (LNAI), vol.\u00a01421. Springer, Heidelberg (1998)"},{"volume-title":"8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus-2000)","year":"2000","key":"2_CR57","unstructured":"Kerber, M., Kohlhase, M. (eds.): 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus-2000). AK Peters, Wellesley (2000)"},{"key":"2_CR58","series-title":"Lecture Notes in Computer Science","volume-title":"Frontiers of Combining Systems","year":"2000","unstructured":"Kirchner, H., Ringeissen, C. (eds.): FroCos 2000. LNCS, vol.\u00a01794. Springer, Heidelberg (2000)"},{"key":"2_CR59","series-title":"Lecture Notes in Computer Science","volume-title":"9th International Conference on Automated Deduction","year":"1988","unstructured":"Lusk, E., Overbeek, R. (eds.): CADE 1988. LNCS, vol.\u00a0310. Springer, Heidelberg (1988)"},{"key":"2_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-45314-8_20","volume-title":"Fundamental Approaches to Software Engineering","author":"T. Mossakowski","year":"2001","unstructured":"Mossakowski, T., Autexier, S., Hutter, D.: Extending development graphs with hiding. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 269\u2013283. Springer, Heidelberg (2001)"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Manthey, R., Bry, F.: SATCHMO: A theorem prover implemented in Prolog. In: Lusk and Overbeek [LO88], pp. 415\u2013434","DOI":"10.1007\/BFb0012847"},{"key":"2_CR62","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-17","year":"2000","unstructured":"McAllester, D. (ed.): CADE 2000. LNCS, vol.\u00a01831. Springer, Heidelberg (2000)"},{"key":"2_CR63","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: Otter 3.0 reference manual and guide. Technical Report ANL-94-6, Argonne National Laboratory, Argonne, Illinois 60439, USA (1994)","DOI":"10.2172\/10129052"},{"issue":"3","key":"2_CR64","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR65","unstructured":"Meier, A.: TRAMP: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In: McAllester [McA00]"},{"key":"2_CR66","unstructured":"Meier, A.: Proof Planning with Multiple Strategies. PhD thesis, Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany (2003)"},{"key":"2_CR67","unstructured":"Melis, E.: Island planning and refinement. Seki-Report SR-96-10, Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany (1996)"},{"key":"2_CR68","first-page":"494","volume-title":"Proceedings of the 13th European Conference on Artifical Intelligence","author":"E. Melis","year":"1998","unstructured":"Melis, E.: AI-techniques in proof planning. In: Prade, H. (ed.) Proceedings of the 13th European Conference on Artifical Intelligence, Brighton, UK, pp. 494\u2013498. John Wiley & Sons, Chichester (1998)"},{"key":"2_CR69","first-page":"494","volume-title":"European Conference on Artificial Intelligence","author":"E. Melis","year":"1998","unstructured":"Melis, E.: AI-techniques in proof planning. In: European Conference on Artificial Intelligence, Brighton, pp. 494\u2013498. Kluwer, Dordrecht (1998)"},{"key":"2_CR70","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1007\/3-540-44957-4_43","volume-title":"Computational Logic - CL 2000","author":"E. Melis","year":"2000","unstructured":"Melis, E., Meier, A.: Proof planning with multiple strategies. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 644\u2013659. Springer, Heidelberg (2000)"},{"key":"2_CR71","unstructured":"Meier, A., Melis, E., Pollet, M.: Towards extending domain representations. Seki Report SR-02-01, Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany (2002)"},{"key":"2_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/3-540-45654-6_39","volume-title":"Computer Aided Systems Theory - EUROCAST 2001","author":"A. Meier","year":"2001","unstructured":"Meier, A., Pollet, M., Sorge, V.: Classifying Isomorphic Residue Classes. In: Moreno-D\u00edaz Jr., R., Buchberger, B., Freire, J.-L. (eds.) EUROCAST 2001. LNCS, vol.\u00a02178, pp. 494\u2013508. Springer, Heidelberg (2001)"},{"issue":"4","key":"2_CR73","first-page":"287","volume":"34","author":"A. Meier","year":"2002","unstructured":"Meier, A., Pollet, M., Sorge, V.: Comparing Approaches to the Exploration of the Domain of Residue Classes. Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems\u00a034(4), 287\u2013306 (2002)","journal-title":"Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems"},{"issue":"1","key":"2_CR74","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0004-3702(99)00076-4","volume":"115","author":"E. Melis","year":"1999","unstructured":"Melis, E., Siekmann, J.: Knowledge-based proof planning. Artificial Intelligence\u00a0115(1), 65\u2013105 (1999)","journal-title":"Artificial Intelligence"},{"key":"2_CR75","unstructured":"Meier, A., Sorge, V.: Exploring properties of residue classes. In: Kerber and Kohlhase [KK00]"},{"key":"2_CR76","unstructured":"Melis, E., Zimmer, J., M\u00fcller, T.: Integrating constraint solving into proof planning. In: Kirchner and Ringeissen [KR00]"},{"key":"2_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"2_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"2_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"2_CR80","volume-title":"How to Solve it","author":"G. Polya","year":"1973","unstructured":"Polya, G.: How to Solve it. Princeton University Press, Princeton (1973)"},{"issue":"1","key":"2_CR81","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM\u00a012(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"2_CR82","unstructured":"Richardson, J., Smaill, A., Green, I.: System description: Proof planning in higher-order logic with \u03bbClam. In: Kirchner and Kirchner [KK98]"},{"key":"2_CR83","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Gor\u00e9 et al. [GLN01]"},{"key":"2_CR84","unstructured":"Sch\u00f6nert, M., et al.: GAP \u2013 Groups, Algorithms, and Programming. Lehrstuhl D f\u00fcr Mathematik, Rheinisch Westf\u00e4lische Technische Hochschule, Aachen, Germany (1995)"},{"key":"2_CR85","series-title":"Lecture Notes in Artificial Intelligence","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)"},{"key":"2_CR86","series-title":"Kluwer Applied Logic series","doi-asserted-by":"crossref","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. Kluwer Applied Logic series, vol.\u00a0(28), pp. 271\u2013314. Kluwer Academic Publishers, Dordrecht (2003) ISBN 1-4020-1656-5"},{"key":"2_CR87","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/s001650050053","volume":"11","author":"J. Siekmann","year":"1999","unstructured":"Siekmann, J., Hess, S., Benzm\u00fcller, C., Cheikhrouhou, L., Fiedler, A., Horacek, H., Kohlhase, M., Konrad, K., Meier, A., Melis, E., Pollet, M., Sorge, V.: LOUI: Lovely \u03a9mega User Interface. Formal Aspects of Computing\u00a011, 326\u2013342 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"#cr-split#-2_CR88.1","unstructured":"Siekmann, J.: Geschichte des automatischen beweisens (history of automated deduction). In: Deduktionssysteme, Automatisierung des Logischen Denkens. R. Oldenbourg Verlag, 2nd edition (1992);"},{"key":"#cr-split#-2_CR88.2","unstructured":"Also in English with Elsewood"},{"key":"2_CR89","volume-title":"The Handbook of the History of Logic","author":"J. Siekmann","year":"2004","unstructured":"Siekmann, J.: History of computational logic. In: Gabbay, D., Woods, J. (eds.) The Handbook of the History of Logic, vol.\u00a0I-IX, Elsevier, Amsterdam (2004) (to appear)"},{"key":"2_CR90","doi-asserted-by":"crossref","unstructured":"Sorge, V.: Non-Trivial Computations in Proof Planning. In: Kirchner and Ringeissen [KR00]","DOI":"10.1007\/10720084_9"},{"key":"2_CR91","unstructured":"Sorge, V.: \u03a9ANTS \u2013 A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany (2001)"},{"key":"2_CR92","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy [Bun94]","DOI":"10.1007\/3-540-58156-1_18"},{"key":"2_CR93","doi-asserted-by":"crossref","unstructured":"van der Hoeven, J.: GNU TeXmacs: A free, structured, wysiwyg and technical text editor. In: Actes du congr\u00e8s Gutenberg, number 39-40 in Actes du congr\u00e8s Gutenberg, Metz, pp. 39\u201350 (May 2001)","DOI":"10.5802\/cg.292"},{"key":"2_CR94","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","year":"2002","unstructured":"Voronkov, A. (ed.): CADE 2002. LNCS (LNAI), vol.\u00a02392. Springer, Heidelberg (2002)"},{"key":"2_CR95","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., Topic, D.: System description: SPASS version 1.0.0. In: Ganzinger [Gan99], pp. 378\u2013382","DOI":"10.1007\/3-540-48660-7_34"},{"issue":"4","key":"2_CR96","first-page":"27","volume":"15","author":"D. Weld","year":"1994","unstructured":"Weld, D.: An introduction to least commitment planning. AI Magazine\u00a015(4), 27\u201361 (1994)","journal-title":"AI Magazine"},{"key":"2_CR97","unstructured":"Wiedijk, F.: The fifteen provers of the world. Unpublished Draft (2002)"},{"key":"2_CR98","unstructured":"Zimmer, J., Kohlhase, M.: System description: The Mathweb Software Bus for distributed mathematical reasoning. In: Voronkov [Vor02], pp. 138\u2013142"},{"key":"2_CR99","first-page":"298","volume-title":"Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI)","author":"J. Zhang","year":"1995","unstructured":"Zhang, J., Zhang, H.: SEM: A system for enumerating models. In: Mellish, C.S. (ed.) Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI), Montreal, Canada, pp. 298\u2013303. Morgan Kaufmann, San Mateo (1995)"}],"container-title":["Lecture Notes in Computer Science","KI 2004: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30221-6_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:50:34Z","timestamp":1605743434000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30221-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231660","9783540302216"],"references-count":100,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30221-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}