{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:19:36Z","timestamp":1725761976547},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642452208"},{"type":"electronic","value":"9783642452215"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_4","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"53-70","source":"Crossref","is-referenced-by-count":1,"title":["A Semantic Basis for Proof Queries and Transformations"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ewen","family":"Denney","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Aho, A.V.: Algorithms for finding patterns in strings. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0A. MIT Press, Cambridge (1990)","DOI":"10.1016\/B978-0-444-88071-0.50010-2"},{"issue":"3","key":"4_CR2","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s11786-010-0025-6","volume":"3","author":"D. Aspinall","year":"2010","unstructured":"Aspinall, D., Denney, E., L\u00fcth, C.: Tactics for hierarchical proof. Mathematics in Computer Science\u00a03(3), 309\u2013330 (2010)","journal-title":"Mathematics in Computer Science"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-28717-6_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Aspinall","year":"2012","unstructured":"Aspinall, D., Denney, E., L\u00fcth, C.: Querying proofs. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 92\u2013106. Springer, Heidelberg (2012)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/3-540-46439-5_35","volume-title":"Advances in Database Technology - EDBT 2000","author":"S. Flesca","year":"2000","unstructured":"Flesca, S., Greco, S.: Querying graph databases. In: Zaniolo, C., Grust, T., Scholl, M.H., Lockemann, P.C. (eds.) EDBT 2000. LNCS, vol.\u00a01777, pp. 510\u2013524. Springer, Heidelberg (2000)"},{"key":"4_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-31374-5_3","volume-title":"Intelligent Computer Mathematics","author":"T. Bourke","year":"2012","unstructured":"Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and experiences in managing large-scale proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol.\u00a07362, pp. 32\u201348. Springer, Heidelberg (2012)"},{"key":"4_CR6","unstructured":"Buneman, P., Cheney, J., Kostylev, E.V.: Hierarchical models of provenance. In: Proceedings of the 4th USENIX Conference on Theory and Practice of Provenance, p. 10 (2012)"},{"issue":"1","key":"4_CR7","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/s007780050084","volume":"9","author":"P. Buneman","year":"2000","unstructured":"Buneman, P., Fernandez, M., Suciu, D.: UnQL: a query language and algebra for semistructured data based on structural recursion. The VLDB Journal\u00a09(1), 76\u2013110 (2000)","journal-title":"The VLDB Journal"},{"key":"4_CR8","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1145\/1040305.1040328","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"C. Calcagno","year":"2005","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 271\u2013282. ACM, New York (2005)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/3-540-45465-9_51","volume-title":"Automata, Languages and Programming","author":"L. Cardelli","year":"2002","unstructured":"Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 597\u2013610. Springer, Heidelberg (2002)"},{"key":"4_CR10","unstructured":"Chamberlin, D.D., et al.: XQuery update facility 1.0 (W3C recommendation) (2011)"},{"issue":"9","key":"4_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1411203.1411209","volume":"43","author":"J. Cheney","year":"2008","unstructured":"Cheney, J.: FLUX: functional updates for XML. SIGPLAN Not.\u00a043(9), 3\u201314 (2008)","journal-title":"SIGPLAN Not."},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/3-540-55179-4_6","volume-title":"Computer Aided Verification","author":"R. Cleaveland","year":"1992","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 48\u201358. Springer, Heidelberg (1992)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-38088-4_37","volume-title":"NASA Formal Methods","author":"E. Denney","year":"2013","unstructured":"Denney, E., Pai, G., Whiteside, I.: Hierarchical safety cases. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol.\u00a07871, pp. 478\u2013483. Springer, Heidelberg (2013)"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/j.entcs.2005.11.063","volume":"155","author":"E. Denney","year":"2006","unstructured":"Denney, E., Power, J., Tourlas, K.: Hiproofs: A hierarchical notion of proof tree. Electronic Notes in Theoretical Computer Science\u00a0155, 341\u2013359 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Dietrich, D., Whiteside, I., Aspinall, D.: POLAR: A framework for proof refactoring. In: Logic for Programming, Artificial Intelligence, and Reasoning (2013)","DOI":"10.1007\/978-3-642-45221-5_52"},{"key":"4_CR16","volume-title":"Fundamentals of algebraic graph transformation","author":"H. Ehrig","year":"2006","unstructured":"Ehrig, H.: Fundamentals of algebraic graph transformation. Springer, Berlin (2006)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G. Gonthier","year":"2013","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O\u2019Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 163\u2013179. Springer, Heidelberg (2013)"},{"issue":"4","key":"4_CR18","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1051\/ita:2004017","volume":"38","author":"M. Grohe","year":"2004","unstructured":"Grohe, M., Schweikardt, N.: Comparing the succinctness of monadic query languages over finite trees. RAIRO - Theoretical Informatics and Applications\u00a038(4), 343\u2013373 (2004)","journal-title":"RAIRO - Theoretical Informatics and Applications"},{"key":"4_CR19","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-39320-4_28","volume-title":"Intelligent Computer Mathematics","author":"J. Heras","year":"2013","unstructured":"Heras, J., Komendantskaya, E.: ML4PG in computer algebra verification. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 354\u2013358. Springer, Heidelberg (2013)"},{"issue":"2","key":"4_CR20","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/767193.767195","volume":"3","author":"H. Hosoya","year":"2003","unstructured":"Hosoya, H., Pierce, B.C.: XDuce: a statically typed XML processing language. ACM Trans. Internet Technol.\u00a03(2), 117\u2013148 (2003)","journal-title":"ACM Trans. Internet Technol."},{"key":"4_CR21","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-39320-4_12","volume-title":"Intelligent Computer Mathematics","author":"S. Obua","year":"2013","unstructured":"Obua, S., Adams, M., Aspinall, D.: Capturing hiproofs in HOL light. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 184\u2013199. Springer, Heidelberg (2013)"},{"key":"4_CR22","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-31374-5_10","volume-title":"Intelligent Computer Mathematics","author":"F. Rabe","year":"2012","unstructured":"Rabe, F.: A query language for formal mathematical libraries. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol.\u00a07362, pp. 143\u2013158. Springer, Heidelberg (2012)"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-14128-7_37","volume-title":"Intelligent Computer Mathematics","author":"C. Tankink","year":"2010","unstructured":"Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: A tool for proof re-animation. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 440\u2013454. Springer, Heidelberg (2010)"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-39320-4_10","volume-title":"Intelligent Computer Mathematics","author":"C. Tankink","year":"2013","unstructured":"Tankink, C., Kaliszyk, C., Urban, J., Geuvers, H.: Formal mathematics on display: A wiki for flyspeck. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol.\u00a07961, pp. 152\u2013167. Springer, Heidelberg (2013)"},{"key":"4_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J. Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Vicknair, C., et al.: A comparison of a graph database and a relational database: a data provenance perspective. In: Proceedings of the 48th Annual Southeast Regional Conference, pp. 42:1\u201342:6. ACM, New York (2010)","DOI":"10.1145\/1900008.1900067"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards formal proof script refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS (LNAI), vol.\u00a06824, pp. 260\u2013275. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22673-1_18"}],"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\/978-3-642-45221-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,18]],"date-time":"2022-03-18T20:34:10Z","timestamp":1647635650000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}