{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T16:08:08Z","timestamp":1764173288644,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540642978"},{"type":"electronic","value":"9783540697176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0022725","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T08:02:06Z","timestamp":1132387326000},"page":"171-188","source":"Crossref","is-referenced-by-count":6,"title":["Automated production of readable proofs for theorems in non-Euclidean geometries"],"prefix":"10.1007","author":[{"given":"Lu","family":"Yang","sequence":"first","affiliation":[]},{"given":"Xiao-Shan","family":"Gao","sequence":"additional","affiliation":[]},{"given":"Shang-Ching","family":"Chou","sequence":"additional","affiliation":[]},{"given":"Jing-Zhong","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"8_CR1","volume-title":"Mechanical Geometry Theorem Proving","author":"S. C. Chou","year":"1988","unstructured":"S. C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht, Netherlands, 1988."},{"key":"8_CR2","doi-asserted-by":"crossref","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry","author":"S. C. Chou","year":"1994","unstructured":"S. C. Chou, X. S. Gao, & J. Z. Zhang, Machine Proofs in Geometry, World Scientific Pub., Singapore, 1994."},{"key":"8_CR3","first-page":"136","volume-title":"Computer Mathematics","author":"S. C. Chou","year":"1993","unstructured":"S. C. Chou & X. S. Gao, Mechanical Theorem Proving in Riemann Geometry, Computer Mathematics, W. T. Wu ed., World Scientific Pub., Singapore, pp. 136\u2013157, 1993."},{"unstructured":"S. C. Chou, X. S. Gao, L. Yang, & J. Z. Zhang, Automated Production of Readable Proofs for Theorems in non-Euclidean Geometries, TR-WSU-94-9, 1994.","key":"8_CR4"},{"unstructured":"S. C. Chou, X. S. Gao, L. Yang, & J. Z. Zhang, A Collection of 90 Automatically Proved Geometry Theorems in non-Euclidean Geometries, TR-WSU-94-10, 1994.","key":"8_CR5"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H. Coelho","year":"1987","unstructured":"H. Coelho & L. M. Pereira, Automated Reasoning in Geometry with Prolog, J. of Automated Reasoning, 2, 329\u2013390, 1987.","journal-title":"J. of Automated Reasoning"},{"unstructured":"H. S. M. Coxeter, Non-Euclidean Geometry, Univ. of Toronto Press, 1968.","key":"8_CR7"},{"key":"8_CR8","first-page":"403","volume":"6","author":"X. S. Gao","year":"1990","unstructured":"X. S. Gao, Transcendental Functions and Mechanical Theorem Proving in Elementary Geometries, J. of Automated Reasoning, 6, 403\u2013417, 1990.","journal-title":"J. of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"H. Gelernter, J. R. Hanson, & D. W. Loveland, Empirical Explorations of the Geometry-theorem Proving Machine, Proc. West. Joint Computer Conf., pp. 143\u2013147, 1960.","key":"8_CR9","DOI":"10.1145\/1460361.1460381"},{"unstructured":"M. J. Greenberg, Euclidean Geometry and non-Euclidean Geometry, Development and History, Freeman, 1980.","key":"8_CR10"},{"unstructured":"B. Gr\u00fcnbaum & G. C. Shephard, From Mennelaus to Computer Assisted Proofs in Geometry, Preprint, Washington State University, 1993.","key":"8_CR11"},{"key":"8_CR12","doi-asserted-by":"crossref","first-page":"579","DOI":"10.1016\/S0747-7171(08)80120-4","volume":"11","author":"T. Havel","year":"1991","unstructured":"T. Havel, Some Examples of the Use of Distances as Coordinates for Euclidean Geometry, J. of Symbolic Computation, 11, 579\u2013594, 1991.","journal-title":"J. of Symbolic Computation"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1016\/0364-0213(90)90008-K","volume":"14","author":"K. R. Koedinger","year":"1990","unstructured":"K. R. Koedinger & J. R. Anderson, Abstract Planning and Perceptual Chunks: Elements of Expertise in Geometry, Cognitive Science, 14, 511\u2013550, 1990.","journal-title":"Cognitive Science"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"A. J. Nevins","year":"1976","unstructured":"A. J. Nevins, Plane Geometry Theorem Proving Using Forward Chaining, Artificial Intelligence, 6, 1\u201323, 1976.","journal-title":"Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"D. Kapur, Geometry Theorem Proving Using Hilbert's Nullstellensatz, Proc. of SYMSAC'86, Waterloo, pp. 202\u2013208, 1986.","key":"8_CR15","DOI":"10.1145\/32439.32479"},{"doi-asserted-by":"crossref","unstructured":"B. Kutzler & S. Stifter, A Geometry Theorem Prover Based on Buchberger's Algorithm, Proc. CADS-7, Oxford, ed. J. H. Siekmann, LNCS, no. 230, pp. 693\u2013694, 1987.","key":"8_CR16","DOI":"10.1007\/3-540-16780-3_141"},{"key":"8_CR17","first-page":"301","volume-title":"Geometry Theorem Proving in Vector Spaces by Means of Gr\u00f6bner Bases","author":"S. Stifter","year":"1993","unstructured":"S. Stifter, Geometry Theorem Proving in Vector Spaces by Means of Gr\u00f6bner Bases, Proc. of ISSAC-98, Kiev, ACM Press, pp. 301\u2013310,1993."},{"unstructured":"T. E. Stokes, On the Algebraic and Algorithmic Properties of Some Generalized Algebras, Ph.D thesis, University of Tasmania, 1990.","key":"8_CR18"},{"key":"8_CR19","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"A. Tarski, A Decision Method for Elementary Algebra and Geometry, Univ. of California Press, Berkeley, 1951."},{"unstructured":"D. M. Wang, On Wu's Method for Proving Constructive Geometry Theorems, Proc. IJCAI'89, Detroit, pp. 419\u2013424, 1989.","key":"8_CR20"},{"key":"8_CR21","first-page":"1","volume":"13","author":"D. M. Wang","year":"1995","unstructured":"D. M. Wang, Elimination Procedures for Mechanical Theorem Proving in Geometry, Ann. of Math. and AI, 13, 1\u201324, 1995.","journal-title":"Ann. of Math. and AI"},{"key":"8_CR22","first-page":"159","volume":"21","author":"W. T. Wu","year":"1978","unstructured":"W. T. Wu, On the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry, Scientia Sinica 21, 159\u2013172, 1978, Also in Automated Theorem Proving: After 25 years, A.M.S., Contemporary Mathematics, 29, pp. 213-234, 1984.","journal-title":"Scientia Sinica"},{"key":"8_CR23","volume-title":"Volume 1: Part of Elementary Geometries","author":"W. T. Wu","year":"1984","unstructured":"W. T. Wu, Basic Principles of Mechanical Theorem Proving in Geometries, Volume 1: Part of Elementary Geometries, Science Press, Beijing (in Chinese), 1984. English Edition, Springer-Verlag, 1994."},{"unstructured":"L. Yang, Computer-Aided Proving for New Theorems of non-Euclidean Geometry, Research Report, No.4, Mathematics Research Section, Australian National University, 1989.","key":"8_CR24"},{"key":"8_CR25","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(90)90077-U","volume":"74","author":"J. Z. Zhang","year":"1990","unstructured":"J. Z. Zhang, L. Yang, & M. Deng, The Parallel Numerical Method of Mechanical Theorem Proving, Theoretical Computer Science, 74, 253\u2013271, 1990.","journal-title":"Theoretical Computer Science"},{"issue":"A","key":"8_CR26","first-page":"547","volume":"37","author":"J. Z. Zhang","year":"1994","unstructured":"J. Z. Zhang, L. Yang, & X. Hou, A Criterion for Dependency of Algebraic Equations, with Applications to Automated Theorem Proving, Science in China Ser.A, 37, 547\u2013554,1994.","journal-title":"Science in China"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Geometry"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022725","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T19:02:55Z","timestamp":1736103775000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022725"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540642978","9783540697176"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0022725","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}