{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T16:20:05Z","timestamp":1794414005369,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287169","type":"print"},{"value":"9783642287176","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28717-6_10","type":"book-chapter","created":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T10:13:04Z","timestamp":1331028784000},"page":"92-106","source":"Crossref","is-referenced-by-count":5,"title":["Querying Proofs"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ewen","family":"Denney","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","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. Electr. Notes Theor. Comput. Sci.\u00a0155, 341\u2013359 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"3","key":"10_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":"10_CR3","doi-asserted-by":"crossref","unstructured":"Angles, R., Gutierrez, C.: Survey of graph database models. ACM Comput. Surv. 40 (February 2008)","DOI":"10.1145\/1322432.1322433"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11526988_3","volume-title":"Reasoning Web","author":"J. Bailey","year":"2005","unstructured":"Bailey, J., Bry, F., Furche, T., Schaffert, S.: Web and Semantic Web Query Languages: A Survey. In: Eisinger, N., Ma\u0142uszy\u0144ski, J. (eds.) Reasoning Web. LNCS, vol.\u00a03564, pp. 35\u2013133. Springer, Heidelberg (2005)"},{"issue":"1","key":"10_CR5","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":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-44659-1_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2000","unstructured":"Berghofer, S., Nipkow, T.: Proof Terms for Simply Typed Higher Order Logic. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 38\u201352. Springer, Heidelberg (2000)"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A skeptic\u2019s approach to combining HOL and Maple. Journal of Automated Reasoning\u00a021, 279\u2013294 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11814771_7","volume-title":"Automated Reasoning","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP Language for Writing Derivations and Finite Interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 67\u201381. Springer, Heidelberg (2006)"},{"issue":"4","key":"10_CR9","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1016\/j.jal.2005.10.005","volume":"4","author":"S.F. Allen","year":"2006","unstructured":"Allen, S.F., Bickford, M., Constable, R.L., Eaton, R., Kreitz, C., Lorigo, L., Moran, E.: Innovations in computational type theory using Nuprl. Journal of Applied Logic\u00a04(4), 428\u2013469 (2006)","journal-title":"Journal of Applied Logic"},{"key":"10_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10721959_3","volume-title":"Automated Deduction - CADE-17","author":"G. Necula","year":"2000","unstructured":"Necula, G., Lee, P.: Proof Generation in the Touchstone Theorem Prover. In: McAllester, D. (ed.) CADE-17. LNCS (LNAI), vol.\u00a01831, pp. 25\u201344. Springer, Heidelberg (2000)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-44659-1_8","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Denney","year":"2000","unstructured":"Denney, E.: A Prototype Proof Translator from HOL to Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"10_CR12","unstructured":"Pons, O., Bertot, Y., Rideau, L.: Notions of dependency in proof assistants. In: Proc. User Interfaces for Theorem Provers, UITP 1998 (1998)"},{"issue":"4","key":"10_CR13","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1016\/j.jal.2005.10.004","volume":"4","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Applied Logic\u00a04(4), 414\u2013427 (2006)","journal-title":"J. Applied Logic"},{"key":"10_CR14","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library for automated theorem proving, Homepage and online tools, \n                  \n                    http:\/\/www.tptp.org\n                  \n                  \n                 (visited November 2011)"},{"key":"10_CR15","unstructured":"da Silva, P.P., Sutcliffe, G., Chang, C., Ding, L., Rio, N.D., McGuinness, D.L.: Presenting TSTP proofs with inference web tools. In: Konev, B., Schmidt, R.A., Schulz, S. (eds.) PAAR\/ESHOL. CEUR Workshop Proceedings, vol.\u00a0373. CEUR-WS.org (2008)"},{"issue":"4-5","key":"10_CR16","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/j.is.2005.02.003","volume":"31","author":"P.P. Silva da","year":"2006","unstructured":"da Silva, P.P., McGuinness, D., Fikes, R.: A proof markup language for semantic web services. Information Systems\u00a031(4-5), 381\u2013395 (2006)","journal-title":"Information Systems"},{"key":"10_CR17","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":"10_CR18","unstructured":"Crew, R.F.: ASTLOG: A language for examining abstract syntax trees. In: DSL, USENIX (1997)"},{"issue":"3","key":"10_CR19","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1109\/32.667879","volume":"24","author":"S. Jarzabek","year":"1998","unstructured":"Jarzabek, S.: Design of flexible static program analyzers with PQL. IEEE Trans. Software Eng.\u00a024(3), 197\u2013215 (1998)","journal-title":"IEEE Trans. Software Eng."}],"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-28717-6_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:07:09Z","timestamp":1620112029000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28717-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287169","9783642287176"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28717-6_10","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-28717-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}