{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T21:24:06Z","timestamp":1743801846129},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_12","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"144-149","source":"Crossref","is-referenced-by-count":23,"title":["Proof Development with \u03a9mega"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Siekmann","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]},{"given":"Vladimir","family":"Brezhnev","sequence":"additional","affiliation":[]},{"given":"Lassaad","family":"Cheikhrouhou","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Fiedler","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Franke","sequence":"additional","affiliation":[]},{"given":"Helmut","family":"Horacek","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Meier","sequence":"additional","affiliation":[]},{"given":"Erica","family":"Melis","sequence":"additional","affiliation":[]},{"given":"Markus","family":"Moschner","sequence":"additional","affiliation":[]},{"given":"Immanuel","family":"Normann","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Pollet","sequence":"additional","affiliation":[]},{"given":"Volker","family":"Sorge","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Ullrich","sequence":"additional","affiliation":[]},{"given":"Claus-Peter","family":"Wirth","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Zimmer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"S. Allen, R. Constable, R. Eaton, C. Kreitz, and L. Lorigo. The Nuprl open logical environment. In Proc. of CADE-17, LNAI 1831. Springer, 2000.","DOI":"10.1007\/10721959_12"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller et al. \u03a9mega: Towards a mathematical assistant. In Proc. of CADE-14, LNAI 1249. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"12_CR3","unstructured":"C. Benzm\u00fcller and V. Sorge. \u03a9-Ants-An open Approach at Combining Interactive and Automated Theorem Proving. In Proc. of Calculemus-2000. AK Peters, 2001."},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W.W. Bledsoe","year":"1990","unstructured":"W.W. Bledsoe. Challenge problems in elementary analysis. Journal of Automated Reasoning, 6:341\u2013359, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CADE-9","author":"A. Bundy","year":"1988","unstructured":"A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In Proc. of CADE-9, LNCS 310. Springer, 1988."},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303\u2013324, 1991. Earlier version available from Edinburgh as DAI Research Paper No 413.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR7","unstructured":"L. Cheikhrouhou and V. Sorge. PDS \u2014 A Three-Dimensional Data Structure for Proof Plans. In Proc. of ACIDCA\u20192000, 2000."},{"key":"12_CR8","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":"12_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CAV-96","author":"S. Owre","year":"1996","unstructured":"S. Owre et al. PVS: Combining specification, proof checking and model checking. In Proc. of CAV-96, LNCS 1102. Springer, 1996."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"A. Fiedler. P.rex: An interactive proof explainer. In Proc. of IJCAR 2001, LNAI 2083. Springer, 2001.","DOI":"10.1007\/3-540-45744-5_33"},{"key":"12_CR11","unstructured":"M. Kohlhase and J. Zimmer. System description: The MathWeb Software Bus for Distributed Mathmatical Reasoning. In Proc. of CADE-18, LNAI. Springer, 2002."},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"A. Franke and M. Kohlhase. System description: MBase, an open mathematical knowledge base. In Proc. of CADE-17, LNAI 1831. Springer, 2000.","DOI":"10.1007\/10721959_36"},{"key":"12_CR13","unstructured":"M. Gordon and T. Melham. Introduction to HOL-A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"12_CR14","volume-title":"Technical Report ANL-94-6","author":"W. McCune","year":"1994","unstructured":"W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94-6, Argonne National Laboratory, Argonne, Illinois 60439, USA, 1994."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"A. Meier. TRAMP: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In Proc. of CADE-17, LNAI 1831. Springer, 2000.","DOI":"10.1007\/10721959_37"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"A. Meier, M. Pollet, and V. Sorge. Comparing Approaches to Explore the Domain of Residue Classes. Journal of Symbolic Computations, 2002. forthcoming.","DOI":"10.1006\/jsco.2002.0550"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"E. Melis and A. Meier. Proof Planning with Multiple Strategies. In Proc. of CL-2000, LNAI 1861. Springer, 2000.","DOI":"10.1007\/3-540-44957-4_43"},{"issue":"1","key":"12_CR18","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":"12_CR19","doi-asserted-by":"crossref","unstructured":"E. Melis, J. Zimmer, and T. M\u00fcller. Integrating constraint solving into proof planning. In Proc. of FroCoS 2000, LNAI 1794. Springer, 2000.","DOI":"10.1007\/10720084_3"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"J.D.C Richardson, A. Smaill, and I.M. Green. System description: Proof planning in higher-order logic with \u03bb-CLAM. In Proc. of CADE-15, LNAI 1421, Springer, 1998.","DOI":"10.1007\/BFb0054254"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/s001650050053","volume":"11","author":"J. Siekmann","year":"1999","unstructured":"J. Siekmann et al. $$ \\mathcal{L}\\mathcal{O}\\mathcal{U}\\mathcal{I}{\\text{: }}\\mathcal{L}{\\text{ovely}} $$ \u03a9mega $$ \\mathcal{U}{\\text{ser }}\\mathcal{I}{\\text{nterface}} $$ . Formal Aspects of Computing, 11:326\u2013342, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"V. Sorge. Non-Trivial Computations in Proof Planning. In Proc. of FroCoS 2000, LNAI 1794. Springer, 2000.","DOI":"10.1007\/10720084_9"},{"key":"12_CR23","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA. see http:\/\/coq.inria.fr\/doc\/main.html ."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:56:23Z","timestamp":1556754983000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}