{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:01Z","timestamp":1725490201091},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745648"},{"type":"electronic","value":"9783540745655"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74565-5_34","type":"book-chapter","created":{"date-parts":[[2007,8,25]],"date-time":"2007-08-25T06:01:04Z","timestamp":1188021664000},"page":"435-439","source":"Crossref","is-referenced-by-count":4,"title":["Deep Inference for Automated Proof Tutoring?"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominik","family":"Dietrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marvin","family":"Schiller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serge","family":"Autexier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"34_CR1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","author":"S. Autexier","year":"2005","unstructured":"Autexier, S.: The core calculus. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"},{"key":"34_CR2","unstructured":"Benzm\u00fcller, C., Vo, Q.B.: Mathematical domain reasoning tasks in natural language tutorial dialog on proofs. In: Proc.\u00a0AAAI-05, AAAI Press\/The MIT Press (2005)"},{"key":"34_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70934-3_1","volume-title":"Cognitive Systems","author":"C. Benzm\u00fcller","year":"2007","unstructured":"Benzm\u00fcller, C., et al.: Natural language dialog with a tutor system for mathematical proofs. In: Ullrich, C., Siekmann, J.H., Lu, R. (eds.) Cognitive Systems. LNCS (LNAI), vol.\u00a04429, Springer, Heidelberg (2007)"},{"key":"34_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69912-5_13","volume-title":"KI 2006: Advances in Artificial Intelligence","author":"C. Benzm\u00fcller","year":"2007","unstructured":"Benzm\u00fcller, C., et al.: Diawoz-II - a tool for wizard-of-oz experiments in mathematics. In: Freksa, C., Kohlhase, M., Schill, K. (eds.) KI 2006. LNCS (LNAI), vol.\u00a04314, Springer, Heidelberg (2007)"},{"key":"34_CR5","unstructured":"Benzm\u00fcller, C., et al.: Proof planning: A fresh start? In: Proc. of IJCAR 2001 Workshop: Future Directions in Automated Reasoning, Siena, Italy (2001)"},{"key":"34_CR6","unstructured":"Dietrich, D., Buckley, M.: Verification of Proof Steps for Tutoring Mathematical Proofs. In: Proc. AIED 2007 (to appear)"},{"issue":"4","key":"34_CR7","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J. Siekmann","year":"2006","unstructured":"Siekmann, J., et al.: Computer supported mathematics with omega. J. Applied Logic\u00a04(4), 533\u2013559 (2006)","journal-title":"J. Applied Logic"},{"key":"34_CR8","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Mathematical Knowledge Management","author":"S. Autexier","year":"2006","unstructured":"Autexier, S., Dietrich, D.: Synthesizing Proof Planning Methods and Oants Agents from Mathematical Knowledge. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, Springer, Heidelberg (2006)"},{"key":"34_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/3-540-45653-8_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. McMath","year":"2001","unstructured":"McMath, D., Rozenfeld, M., Sommer, R.: A computer environment for writing ordinary mathematical proofs. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 507\u2013516. Springer, Heidelberg (2001)"},{"key":"34_CR10","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1093\/jigpal\/11.4.457","volume":"11","author":"C. Zinn","year":"2003","unstructured":"Zinn, C.: A computational framework for understanding mathematical discourse. Logic J. of the IGPL\u00a011, 457\u2013484 (2003)","journal-title":"Logic J. of the IGPL"},{"key":"34_CR11","unstructured":"Dietrich, D.: The tasklayer of the omega system. Master\u2019s thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (2006)"}],"container-title":["Lecture Notes in Computer Science","KI 2007: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74565-5_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:24:59Z","timestamp":1619519099000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74565-5_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745648","9783540745655"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74565-5_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}