{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,14]],"date-time":"2024-03-14T23:10:19Z","timestamp":1710457819365},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2009,6,30]],"date-time":"2009-06-30T00:00:00Z","timestamp":1246320000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2010,2]]},"DOI":"10.1007\/s10817-009-9138-5","type":"journal-article","created":{"date-parts":[[2009,6,29]],"date-time":"2009-06-29T10:53:12Z","timestamp":1246272792000},"page":"79-110","source":"Crossref","is-referenced-by-count":3,"title":["Crystal: Integrating Structured Queries into a Tactic Language"],"prefix":"10.1007","volume":"44","author":[{"given":"Dominik","family":"Dietrich","sequence":"first","affiliation":[]},{"given":"Ewaryst","family":"Schulz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,6,30]]},"reference":[{"key":"9138_CR1","first-page":"367","volume-title":"Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991","author":"F Andersen","year":"1992","unstructured":"Andersen, F., Petersen, K.D.: Recursive boolean functions in HOL. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991, pp.\u00a0367\u2013377. IEEE Computer Society, Silver Spring (1992)"},{"issue":"1\u20133","key":"9138_CR2","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1023\/A:1022907629104","volume":"38","author":"A Asperti","year":"2003","unstructured":"Asperti, A., Padovani, L., Coen, C.S., Guidi, F., Schena, I.: Mathematical knowledge management in helm. Ann. Math. Artif. Intell. 38(1\u20133), 27\u201346 (2003)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9138_CR3","series-title":"LNCS","first-page":"17","volume-title":"Post-Proceedings of the Types 2004 International Conference","author":"A Asperti","year":"2004","unstructured":"Asperti, A., Guidi, F., Coen, C.S., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: whelp. In: Post-Proceedings of the Types 2004 International Conference. LNCS, vol. 3839, pp.\u00a017\u201332. Springer, New York (2004)"},{"key":"9138_CR4","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A Asperti","year":"2006","unstructured":"Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: User interaction with the matita proof assistant. J. Autom. Reason. 39, 109\u2013139 (2006)","journal-title":"J. Autom. Reason."},{"key":"9138_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/11618027_5","volume-title":"Mathematical Knowledge Management MKM 2005","author":"D Aspinall","year":"2006","unstructured":"Aspinall, D., L\u00fcth, C., Wolff, B.: Assisted proof document authoring. In: Kohlhase, M. (ed.) Mathematical Knowledge Management MKM 2005, Lecture Notes in Artificial Intelligence, vol. 3863, pp.\u00a065\u201380. Springer, New York (2006)"},{"key":"9138_CR6","series-title":"LNAI","volume-title":"Proceedings of CADE-20, Tallinn, Estonia","author":"S Autexier","year":"2005","unstructured":"Autexier, S.: The CoRe calculus. In: Nieuwenhuis, R. (ed.) Proceedings of CADE-20, Tallinn, Estonia. LNAI, vol. 3632. Springer, New York (2005)"},{"key":"9138_CR7","series-title":"LNAI","first-page":"94","volume-title":"Proceedings of MKM\u201906","author":"S Autexier","year":"2006","unstructured":"Autexier, S., Dietrich, D.: Synthesizing proof planning methods and Omega-Ants agents from mathematical knowledge. In: Borwein, J., Farmer, B. (eds.) Proceedings of MKM\u201906. LNAI, vol. 4108, pp.\u00a094\u2013109. Springer, New York (2006)"},{"key":"9138_CR8","series-title":"LNAI","volume-title":"Festschrift in Honor of J. Siekmann","author":"S Autexier","year":"2006","unstructured":"Autexier, S., Hutter, D.: Formal software development in maya. In: Hutter, D., Stephan, W. (eds.) Festschrift in Honor of J. Siekmann. LNAI, vol. 2605. Springer, New York (2006)"},{"key":"9138_CR9","series-title":"LNCS","volume-title":"Proceedings 9th International Conference on Algebraic Methodology And Software Technology (AMAST\u201902)","author":"S Autexier","year":"2002","unstructured":"Autexier, S., Hutter, D., Mossakowski, T., Schairer, A.: The development graph manager MAYA. In: Kirchner, H., Ringeissen, Ce. (eds.) Proceedings 9th International Conference on Algebraic Methodology And Software Technology (AMAST\u201902). LNCS, vol. 2422. Springer, New York (2002)"},{"key":"9138_CR10","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/s11786-008-0054-6","volume":"2","author":"S Autexier","year":"2008","unstructured":"Autexier, S., Benzm\u00fcller, C., Dietrich, D., Wagner, M.: Organisation, transformation, and propagation of mathematical knowledge in omega. J. Math. Comput. Sci. 2, 253\u2013277 (2008)","journal-title":"J. Math. Comput. Sci."},{"key":"9138_CR11","first-page":"266","volume-title":"Proceedings of MKM\u201906","author":"G Bancerek","year":"2006","unstructured":"Bancerek, G.: Information retrieval and rendering with mml query. In: Proceedings of MKM\u201906, pp.\u00a0266\u2013279. Springer, New York (2006)"},{"key":"9138_CR12","first-page":"119","volume-title":"Proceedings of MKM\u201903","author":"G Bancerek","year":"2003","unstructured":"Bancerek, G., Rudnicki, P.: Information retrieval in mml. In: Proceedings of MKM\u201903, pp.\u00a0119\u2013132. Springer, London (2003)"},{"issue":"1835","key":"9138_CR13","doi-asserted-by":"crossref","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","volume":"363","author":"H Barendregt","year":"2005","unstructured":"Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Philos. Trans.\u2014Royal Soc., Math. Phys. Eng. Sci. 363(1835), 2351\u20132375 (2005)","journal-title":"Philos. Trans.\u2014Royal Soc., Math. Phys. Eng. Sci."},{"key":"9138_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, New York (2004)"},{"key":"9138_CR15","volume-title":"Proceedings of International Workshop on Theory and Practice of Algebraic Specifications ASF+SDF 97, Workshops in Computing","author":"P Borovansk\u00fd","year":"1997","unstructured":"Borovansk\u00fd, P., Kirchner, H.: Strategies of elan: meta-interpretation and partial evaluation. In: Proceedings of International Workshop on Theory and Practice of Algebraic Specifications ASF+SDF 97, Workshops in Computing. Springer, Amsterdam (1997)"},{"issue":"1","key":"9138_CR16","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1142\/S0129054101000412","volume":"12","author":"P Borovansky","year":"2001","unstructured":"Borovansky, P., Kirchner, C., Kirchner, H., Ringeissen, C.: Rewriting with strategies in ELAN: a functional semantics. Int. J. Found. Comput. Sci. 12(1), 69\u201395 (2001)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"9138_CR17","series-title":"LNAI","first-page":"111","volume-title":"Proceedings CADE-9","author":"A Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk. R., Overbeek, R. (eds.) Proceedings CADE-9. LNAI, pp.\u00a0111\u2013120. Springer, New York (1988)"},{"key":"9138_CR18","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BF00881866","volume":"10","author":"J Christian","year":"1993","unstructured":"Christian, J.: Flatterms, discrimination nets, and fast term rewriting. J. Autom. Reason. 10, 95\u2013113 (1993)","journal-title":"J. Autom. Reason."},{"key":"9138_CR19","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"RL Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D.J., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"9138_CR20","series-title":"Lecture Notes in Computer Science","first-page":"69","volume-title":"TYPES","author":"P Corbineau","year":"2007","unstructured":"Corbineau, P.: A declarative language for the coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES. Lecture Notes in Computer Science, vol. 4941, pp.\u00a069\u201384. Springer, New York (2007)"},{"key":"9138_CR21","volume-title":"Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark). ENTCS, vol. 70(2)","author":"D Delahaye","year":"2002","unstructured":"Delahaye, D.: A proof dedicated meta-language. In: Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark). ENTCS, vol. 70(2). Elsevier, Amsterdam (2002)"},{"key":"9138_CR22","unstructured":"Dietrich, D.: The task-layer of the \u03a9mega system. Diploma thesis, FR 6.2 Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken (2006)"},{"key":"9138_CR23","unstructured":"Dixon, L.: A proof planning framework for Isabelle. Ph.D. thesis, University of Edinburgh (2005)"},{"issue":"4","key":"9138_CR24","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1016\/j.jal.2005.10.007","volume":"4","author":"L Dixon","year":"2005","unstructured":"Dixon, L., Fleuriot, J.D.: A proof-centric approach to mathematical assistants. J. Appl. Logic 4(4), 505\u2013532 (2005)","journal-title":"J. Appl. Logic"},{"key":"9138_CR25","doi-asserted-by":"crossref","first-page":"653","DOI":"10.1007\/BF00881906","volume":"11","author":"W Farmer","year":"1993","unstructured":"Farmer, W., Guttman, J., Thayer, F.J.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11, 653\u2013654 (1993)","journal-title":"J. Autom. Reason."},{"key":"9138_CR26","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s12046-009-0001-5","volume":"34","author":"H Geuvers","year":"2009","unstructured":"Geuvers, H.: Proof assistants: history, ideas and future. Sadahana 34, 3\u201325 (2009) (Special Issue on Interactive Theorem Proving and Proof Checking)","journal-title":"Sadahana"},{"key":"9138_CR27","unstructured":"Geuvers, H., Mamane, L.E.L.: A document-oriented Coq Plugin for Texmacs (2006)"},{"key":"9138_CR28","doi-asserted-by":"crossref","first-page":"169","DOI":"10.7551\/mitpress\/5641.003.0012","volume-title":"Proof, Language, and Interaction","author":"M Gordon","year":"2000","unstructured":"Gordon, M.: From lcf to hol: a short history. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, pp.\u00a0169\u2013186. MIT, Cambridge (2000)"},{"key":"9138_CR29","volume-title":"LNCS, vol. 78","author":"MJ Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF\u2014a mechanised logic of computation. In: LNCS, vol. 78. Springer, New York (1979)"},{"key":"9138_CR30","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design (FMCAD\u201996)","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: Hol light: a tutorial introduction. In: Formal Methods in Computer-Aided Design (FMCAD\u201996), pp.\u00a0265\u2013269. Springer, New York (1996)"},{"key":"9138_CR31","volume-title":"DISKI, no. 112","author":"X Huang","year":"1996","unstructured":"Huang, X.: Human oriented proof presentation: a reconstructive approach. In: DISKI, no. 112. Infix, Sankt Augustin (1996)"},{"key":"9138_CR32","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-57186-8_92","volume-title":"PLILP \u201993: Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming","author":"AA Letichevsky","year":"1993","unstructured":"Letichevsky, A.A.: Development of rewriting strategies. In: PLILP \u201993: Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, pp.\u00a0378\u2013390. Springer, London (1993)"},{"key":"9138_CR33","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"417","volume-title":"Mart\u00ed-Oliet, N. (ed.) Proceedings Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, 27 March\u20134 April, 2004","author":"N Mart\u00ed-Oliet","year":"2005","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for Maude. In: Mart\u00ed-Oliet, N. (ed.) Proceedings Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, 27 March\u20134 April, 2004. Electronic Notes in Theoretical Computer Science, vol. 117, pp.\u00a0417\u2013441. Elsevier, Amsterdam (2005)"},{"issue":"1","key":"9138_CR34","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 7(1), 41\u201357 (2009). doi: 10.1016\/j.jal.2007.07.004","journal-title":"J. Appl. Logic"},{"key":"9138_CR35","series-title":"LNCS","volume-title":"CASL reference manual","year":"2004","unstructured":"Mosses, P.D. (ed.): CASL reference manual. In: LNCS, no. 2960. Springer, New York (2004)"},{"key":"9138_CR36","volume-title":"LNCS, vol. 2283","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014a proof assistant for higher-order logic. In: LNCS, vol. 2283. Springer, New York (2002)"},{"issue":"2","key":"9138_CR37","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"LC Paulson","year":"1983","unstructured":"Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119\u2013149 (1983)","journal-title":"Sci. Comput. Program."},{"key":"9138_CR38","first-page":"119","volume-title":"Proc. FTP\u00a097","author":"W Reif","year":"1998","unstructured":"Reif, W., Schellhorn, G.: Theorem proving in large theories. In: Proc. FTP\u00a097, pp.\u00a0119\u2013124. Kluwer, Dordrecht (1998)"},{"key":"9138_CR39","doi-asserted-by":"crossref","unstructured":"Richardson, J.: A semantics for proof plans with applications to interactive proof planning. In: Lecture Notes in Computer Science (2002)","DOI":"10.1007\/3-540-36078-6_23"},{"key":"9138_CR40","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/BFb0054254","volume-title":"15th International Conference on Automated Deduction","author":"J Richardson","year":"1998","unstructured":"Richardson, J., Smaill, A., Green, I.: System description: proof planning in higher-order logic with clam. In: 15th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 1421, pp.\u00a0129\u2013133. Springer, New York (1998)"},{"issue":"4","key":"9138_CR41","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J Siekmann","year":"2006","unstructured":"Siekmann, J., Benzm\u00fcller, C., Autexier, S.: Computer supported mathematics with omega. J. Appl. Logic 4(4), 533\u2013559 (2006) (Special issue on Mathematics Assistance Systems)","journal-title":"J. Appl. Logic"},{"key":"9138_CR42","doi-asserted-by":"crossref","unstructured":"Trybulec, A., Blair, H.: Computer assisted reasoning with Mizar. In: Joshi, A. (ed.) Proceedings of the 9th Int. Joint Conference on Artifical Intelligence. M. Kaufmann (1985)","DOI":"10.1007\/3-540-15648-8_30"},{"issue":"1","key":"9138_CR43","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J Urban","year":"2006","unstructured":"Urban, J.: MoMM\u2014fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. Artif. Intell. Tools 15(1), 109\u2013130 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9138_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/3-540-45127-7_27","volume-title":"Rewriting Techniques and Applications (RTA 2001)","author":"E Visser","year":"2001","unstructured":"Visser, E.: Stratego: a language for program transformation based on rewriting strategies. System description of Stratego 0.5. In: Middeldorp, A. (ed.) Rewriting Techniques and Applications (RTA 2001). Lecture Notes in Computer Science, vol. 2051, pp.\u00a0357\u2013361. Springer, New York (2001)"},{"key":"9138_CR45","volume-title":"Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics. Series in Artificial Intelligence","author":"L Wallen","year":"1990","unstructured":"Wallen, L.: Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics. Series in Artificial Intelligence. MIT, Cambridge (1990)"},{"key":"9138_CR46","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction\u2014CADE-18","author":"C Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobalt, C., Topi\u0107, D.: SPASS version 2.0. In: Voronkov, A. (ed.) Automated Deduction\u2014CADE-18. LNAI, no. 2392 , pp.\u00a0275\u2013279. Springer, New York (2002)"},{"key":"9138_CR47","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs\u201999","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics: TPHOLs\u201999. LNCS, vol. 1690, pp.\u00a0167\u2013184. Springer, New York (1999)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9138-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9138-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9138-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,14]],"date-time":"2024-03-14T22:52:59Z","timestamp":1710456779000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9138-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,30]]},"references-count":47,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["9138"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9138-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,6,30]]}}}