{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:31Z","timestamp":1725494311064},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_10","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"142-156","source":"Crossref","is-referenced-by-count":8,"title":["Presenting Proofs in a Human-Oriented Way"],"prefix":"10.1007","author":[{"given":"Helmut","family":"Horacek","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Christoph Benzm\u00fcller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, J\u00e4rg Siekmann, Volker Sorge....MEGA: Towards a Mathematical Assistant. In Proc. of CADE-97, 1997.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/0004-3702(76)90007-2","volume":"7","author":"D. Chester","year":"1976","unstructured":"Dan Chester. The Translation of Formal Proofs into English. In Artificial Intelligence 7, pp. 261\u2013278, 1976.","journal-title":"Artificial Intelligence"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Yann Coscoy, Gilles Kahn, Laurent Th ry, Extracting Text from Proof. In Typed Lambda Calculus and its Application, 1995.","DOI":"10.1007\/BFb0014048"},{"key":"10_CR4","unstructured":"Ingo Dahn. Using ILF as a User Interface for Many Theorem Provers. In Proc. of User Interfaces for Theorem Provers, Eindhoven, 1998."},{"key":"10_CR5","unstructured":"A. Edgar, Francis Pelletier. Natural Language Explanation of Natural Deduction Proofs. In Proc. of the First Conference of the Pacific Association for Computational Linguistics, Simon Fraser University, 1993."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Detlef Fehrer, Helmut Horacek. Presenting Inequations in Mathematical Proofs, to appear in Information Sciences, Special Issue on Logical Methods for Computational Intelligence, 1999.","DOI":"10.1016\/S0020-0255(98)10094-4"},{"key":"10_CR7","unstructured":"Detlef Fehrer, Helmut Horacek. Exploiting the Addressee\u2019s Inferential Capabilities in Presenting Mathematical Proofs, In Proc. of IJCAI-97, pp. 556\u2013560, Nagoya, 1997."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Nancy Green, Sandra Carberry. A Hybrid Reasoning Model for Indirect Answers. In Proc. of ACL-94, Las Cruces, New Mexico, 1994.","DOI":"10.3115\/981732.981741"},{"key":"10_CR9","first-page":"43","volume":"3","author":"H. Grice","year":"1975","unstructured":"H. Grice. Logic and Conversation. In Syntax and Semantics: Vol. 3, Speech Acts, pp. 43\u201358, Academic Press, 1975.","journal-title":"Syntax and Semantics"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1008297401272","volume":"7","author":"H. Horacek","year":"1997","unstructured":"Helmut Horacek. A Model for Adapting Explanations to the User\u2019s Likely Inferences. User Modeling and User Adapted Interaction, 7, pp. 1\u201355, 1997.","journal-title":"User Modeling and User Adapted Interaction"},{"key":"10_CR11","unstructured":"Helmut Horacek. Generating Inference-Rich Discourse Through Revisions of RST-Trees. In Proc. of AAAI-98, pp. 814\u2013820, 1998."},{"key":"10_CR12","unstructured":"Xiaorong Huang. Human Oriented Proof Presentation: A Reconstructive Approach. PhD Dissertation, University of the Saarland, 1994."},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Xiaorong Huang. Reconstructing Proofs at the Assertional Level. In Proc. of CADE-94, pp. 738\u2013752, 1994.","DOI":"10.1007\/3-540-58156-1_53"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Xiaorong Huang. Translating Machine-Generated Proofs into ND-Proofs at the Assertion Level. In Proc. of PRICAI-96, LNAI, Springer, 1996.","DOI":"10.1007\/3-540-61532-6_34"},{"key":"10_CR15","unstructured":"Xiaorong Huang, Armin Fiedler. Proof Presentation as an Application of NLG. In Proc. of IJCAI-97, pp. 965\u2013971, Nagoya, Japan, 1997."},{"key":"10_CR16","unstructured":"Philip Johnson-Laird, Ruth Byrne. Deduction. Ablex Publishing, 1990."},{"key":"10_CR17","unstructured":"William Mann, Sandra Thompson. Rhetorical Structure Theory: A Theory of Text Organization. 83\u2013115, ISI at University of Southern California, 1983."},{"key":"10_CR18","unstructured":"Andreas Meier. \u2020bersetzung automatisch erzeugter Beweise auf Faktenebene. Diploma thesis, University of the Saarland, 1997."},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"William McCune. Otter 3.0 Reference Manual and Guide.Technical Report ANL-94\/6, Argonne National Laboratory, 1994.","DOI":"10.2172\/10129052"},{"issue":"3","key":"10_CR20","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"William McCune. Solution of the Robins Problem. Journal of Automated Reasoning 19(3), pp. 263\u2013276, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Mark Stickel. Schubert\u2019s Steamroller Problem: Formulations and Solutions. In Journal of Automated Reasoning 2(1), 1986.","DOI":"10.1007\/BF00246025"},{"key":"10_CR22","first-page":"76","volume":"2","author":"M. Th\u00fcring","year":"1985","unstructured":"Manfred Th\u00fcring, Kurt Wender. \u2020ber kausale Inferenzen beim Lesen. In Sprache und Kognition 2, pp. 76\u201386, 1985.","journal-title":"Sprache und Kognition"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0004-3702(95)00114-X","volume":"85","author":"M. Walker","year":"1996","unstructured":"Marilyn Walker. The Effect of Resource Limits and Task Complexity on Collaborative Planning in Dialogue. In Artificial Intelligence 85, pp. 181\u2013243, 1996.","journal-title":"Artificial Intelligence"},{"key":"10_CR24","unstructured":"Ingrid Zukerman, Richard McConachy. Generating Concise Discourse that Addresses a User\u2019s Inferences. In Proc. of IJCAI-93, pp. 1202\u20131207, Chambery, France, 1993."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T04:56:34Z","timestamp":1556945794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}