{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T11:32:55Z","timestamp":1648985575625},"reference-count":24,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1999,5,1]],"date-time":"1999-05-01T00:00:00Z","timestamp":925516800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information Sciences"],"published-print":{"date-parts":[[1999,5]]},"DOI":"10.1016\/s0020-0255(98)10094-4","type":"journal-article","created":{"date-parts":[[2003,4,25]],"date-time":"2003-04-25T01:23:41Z","timestamp":1051233821000},"page":"3-23","source":"Crossref","is-referenced-by-count":3,"title":["Presenting inequations in mathematical proofs"],"prefix":"10.1016","volume":"116","author":[{"given":"Detlef","family":"Fehrer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Horacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0020-0255(98)10094-4_bib1","series-title":"Automated Deduction \u2014 CADE-14, Proceedings of the 14th International Conference on Automated Deduction","first-page":"252","article-title":"\u03a9MEGA: Towards a Mathematical Assistant","author":"Benzm\u00fcller","year":"1997"},{"key":"10.1016\/S0020-0255(98)10094-4_bib2","article-title":"Analysis and representation of equational proofs generated by a distributed completion based proof system","author":"Denzinger","year":"1994"},{"key":"10.1016\/S0020-0255(98)10094-4_bib3","first-page":"959","article-title":"Exploiting the addressee's inferential capabilities in presenting mathematical proofs","volume":"vol. 2","author":"Fehrer","year":"1997"},{"key":"10.1016\/S0020-0255(98)10094-4_bib4","first-page":"39","article-title":"Untersuchungen \u00fcber das logische Schlie\u03b2en I. Mathematische Zeitschrift","author":"Gentzen","year":"1935"},{"key":"10.1016\/S0020-0255(98)10094-4_bib5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1008297401272","article-title":"A model for adapting explanations to the user's likely inferences","volume":"7","author":"Horacek","year":"1997","journal-title":"User Modeling and User-Adapted Interaction"},{"key":"10.1016\/S0020-0255(98)10094-4_bib6","series-title":"AAAI-98\/IAAI-98 Fifteenth National Conference on Artificial Intelligence and Tenth Conference on Innovative Applications of Artificial Intelligence","first-page":"814","article-title":"Generating Inference-Rich Discourse Through Revisions of RST-Trees","author":"Horacek","year":"1998"},{"key":"10.1016\/S0020-0255(98)10094-4_bib7","series-title":"Proceedings of 16th Annual Conference of the Cognitive Science Society","first-page":"427","article-title":"Proverb: A system explaining machine-found proofs","author":"Huang","year":"1994"},{"key":"10.1016\/S0020-0255(98)10094-4_bib8","series-title":"Automated Deduction \u2014 CADE-12, Proceedings of the 12th International Conference on Automated Deduction","first-page":"788","article-title":"Reconstructing proofs at the assertion level","author":"Huang","year":"1994"},{"key":"10.1016\/S0020-0255(98)10094-4_bib9","article-title":"Human oriented proof presentation: a reconstructive approach","author":"Huang","year":"1996","journal-title":"No. 112 in DISKI. Infix"},{"key":"10.1016\/S0020-0255(98)10094-4_bib10","series-title":"Proceedings of PRICAI-96","first-page":"399","article-title":"Translating machine-generated resolution proofs into ND-proofs at the assertion level","volume":"1114","author":"Huang","year":"1996"},{"key":"10.1016\/S0020-0255(98)10094-4_bib11","series-title":"Proceedings of the 8th International Natural Language Generation Workshop","article-title":"Paraphrasing and aggregating argumentative texts using text structure","author":"Huang","year":"1996"},{"key":"10.1016\/S0020-0255(98)10094-4_bib12","series-title":"Proceedings of the 13th CADE","article-title":"Presenting machine-found proofs","author":"Huang","year":"1996"},{"key":"10.1016\/S0020-0255(98)10094-4_bib13","series-title":"Automated Deduction \u2014 CADE-12, Proceedings of the 12th International Conference on Automated Deduction","first-page":"788","article-title":"\u03a9-MKRP, a proof development environment","author":"Huang","year":"1994"},{"key":"10.1016\/S0020-0255(98)10094-4_bib14","unstructured":"X. Huang, A. Meier, Natural deduction proofs can be as short as resolution proofs, SEKI report, to appear."},{"key":"10.1016\/S0020-0255(98)10094-4_bib15","article-title":"Transformation and Structuring of Computer Generated proofs","author":"Lingenfelder","year":"1990"},{"key":"10.1016\/S0020-0255(98)10094-4_bib16","article-title":"Presentation of proofs in an equational calculus","author":"Lingenfelder","year":"1990"},{"key":"10.1016\/S0020-0255(98)10094-4_bib17","series-title":"Vorlesungen \u00fcber Analysis","author":"L\u00fcneburg","year":"1981"},{"key":"10.1016\/S0020-0255(98)10094-4_bib18","author":"McCune","year":"1994"},{"key":"10.1016\/S0020-0255(98)10094-4_bib19","series-title":"Proceedings of the 10th International Conference on Automated Deduction","first-page":"351","article-title":"Toward mechanical methods for streamlining proofs","author":"Pierce","year":"1990"},{"key":"10.1016\/S0020-0255(98)10094-4_bib20","first-page":"135","article-title":"Paramodulation and theorem proving in first order theories with equality","volume":"vol. 4","author":"Robinson","year":"1969"},{"key":"10.1016\/S0020-0255(98)10094-4_bib21","first-page":"227","article-title":"Automated deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"Int. J. of Comp. Math."},{"key":"10.1016\/S0020-0255(98)10094-4_bib22","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","article-title":"Refutation graphs","volume":"7","author":"Shostak","year":"1976","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0020-0255(98)10094-4_bib23","first-page":"76","article-title":"\u00dcber kausale Inferenzen beim Lesen","volume":"2","author":"Th\u00fcring","year":"1985","journal-title":"Sprache und Kognition"},{"key":"10.1016\/S0020-0255(98)10094-4_bib24","series-title":"Proceedings of IJCAI-93","first-page":"1202","article-title":"Generating concise discourse that adresses a user's inferences","author":"Zukerman","year":"1993"}],"container-title":["Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0020025598100944?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0020025598100944?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T22:21:52Z","timestamp":1556058112000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0020025598100944"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,5]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,5]]}},"alternative-id":["S0020025598100944"],"URL":"https:\/\/doi.org\/10.1016\/s0020-0255(98)10094-4","relation":{},"ISSN":["0020-0255"],"issn-type":[{"value":"0020-0255","type":"print"}],"subject":[],"published":{"date-parts":[[1999,5]]}}}