{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,3]],"date-time":"2026-02-03T15:35:12Z","timestamp":1770132912488,"version":"3.49.0"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1996,12,1]],"date-time":"1996-12-01T00:00:00Z","timestamp":849398400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1996,12]]},"DOI":"10.1007\/bf00283133","type":"journal-article","created":{"date-parts":[[2004,9,19]],"date-time":"2004-09-19T11:33:20Z","timestamp":1095593600000},"page":"325-347","source":"Crossref","is-referenced-by-count":48,"title":["Automated generation of readable proofs with geometric invariants"],"prefix":"10.1007","volume":"17","author":[{"given":"Shang-Ching","family":"Chou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiao-Shan","family":"Gao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jing-Zhong","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF00283133_CR1","unstructured":"Anderson, J. R., Boyle, C. F., Corbett, A., and Lewis, M.: The geometry tutor, in Proc. of the IJCAI, Los Angeles, U.S.A., 1985 pp. 1\u20137."},{"key":"BF00283133_CR2","volume-title":"Mechanical Geometry Theorem Proving","author":"S. C. Chou","year":"1988","unstructured":"Chou, S. C.: Mechanical Geometry Theorem Proving, D. Reidel Publ. Co., Dordrecht, The Netherlands, 1988."},{"key":"BF00283133_CR3","doi-asserted-by":"crossref","unstructured":"Chou, S. C., Gao, X. S., and Zhang, J. Z.: The Machine Proofs in Geometry, World Scientific, 1994.","DOI":"10.1142\/2196"},{"key":"BF00283133_CR4","doi-asserted-by":"crossref","unstructured":"Chou, S. C., Gao, X. S., and Zhang, J. Z.: Automated production of traditional proofs for constructive geometry theorems, in Proc. of Eighth IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1993, pp. 48\u201356.","DOI":"10.1109\/LICS.1993.287601"},{"key":"BF00283133_CR5","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H. Coelho","year":"1986","unstructured":"Coelho, H. and Pereira, L. M.: Automated reasoning in geometry theorem proving with prolog, J. of Automated Reasoning 2 (1986), 329\u2013390.","journal-title":"J. of Automated Reasoning"},{"key":"BF00283133_CR6","unstructured":"Gelertner, H.: Realization of a geometry-theorem proving machine, in E. A. Feigenbaum and J. Feldman, (eds), Computers and Thought, McGraw-Hill, pp. 134\u2013152."},{"key":"BF00283133_CR7","doi-asserted-by":"crossref","unstructured":"Gelertner, H., Hanson, J. R., and Loveland, D. W.: Empirical explorations of the geometry-theorem proving machine, in Proc. West. Joint Computer Conf., 1960, pp. 143\u2013147.","DOI":"10.1145\/1460361.1460381"},{"key":"BF00283133_CR8","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert's Nullstellensatz, in Proc. of SYMSAC'86, Waterloo, 1986, pp. 202\u2013208.","DOI":"10.1145\/32439.32479"},{"key":"BF00283133_CR9","doi-asserted-by":"crossref","unstructured":"Gilmore, P. C.: An examination of the geometry theorem proving machine, Artificial Intelligence 1, 171\u2013187.","DOI":"10.1016\/0004-3702(70)90005-6"},{"key":"BF00283133_CR10","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1207\/s15516709cog1404_2","volume":"14","author":"K. R. Koedinger","year":"1990","unstructured":"Koedinger, K. R. and Anderson, J. R.: Abstract planning and perceptual chunks: Elements of expertise in geometry, Cognitive Science 14 (1990), 511\u2013550.","journal-title":"Cognitive Science"},{"key":"BF00283133_CR11","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. E. Korf","year":"1985","unstructured":"Korf, R. E.: Depth-first interactive-deepening: An optimal admissible tree search, Artificial Intelligence 27 (1985), 97\u2013109.","journal-title":"Artificial Intelligence"},{"key":"BF00283133_CR12","doi-asserted-by":"crossref","unstructured":"Nevins, A. J.: Plane geometry theorem proving using forward chaining, Artificial Intelligence 6, 1\u201323.","DOI":"10.1016\/0004-3702(75)90013-2"},{"key":"BF00283133_CR13","doi-asserted-by":"crossref","unstructured":"Robinson, A.: Proving a theorem (as done by man, logician, or machine), in J. Siekmann and G. Wrightson (eds), Automation of Reasoning, Springer-Verlag, 1983, pp. 74\u201378.","DOI":"10.1007\/978-3-642-81952-0_5"},{"issue":"4","key":"BF00283133_CR14","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. Stickel","year":"1985","unstructured":"Stickel, M.: A prolog technology theorem prover: Implementation by an extended prolog compiler, J. of Automated Reasoning 4(4) (1985), 353\u2013380.","journal-title":"J. of Automated Reasoning"},{"key":"BF00283133_CR15","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/320856.320867","volume":"4","author":"H. Wang","year":"1957","unstructured":"Wang, H.: A variant to turing's theory of computing machines, J. of ACM 4 (1957), 63\u201392.","journal-title":"J. of ACM"},{"key":"BF00283133_CR16","unstructured":"Warren, D. S., Pereira, F., and Debray, S. K.: The SB-Prolog System, Version 3.0, Department of Computer Science, Univ. of Arizona."},{"key":"BF00283133_CR17","first-page":"159","volume":"21","author":"Wu Wen-ts\u00fcn","year":"1978","unstructured":"Wu Wen-ts\u00fcn: On the decision problem and the mechanization of theorem in elementary geometry, Scientia Sinica 21 (1978), 159\u2013172; Also in Automated Theorem Proving: After 25 Years, A.M.S., Contemporary Mathematics 29 (1984), 213\u2013234.","journal-title":"Scientia Sinica"},{"key":"BF00283133_CR18","volume-title":"Basic Principles of Mechanical Theorem Proving in Geometries","author":"Wu Wen-ts\u00fcn","year":"1984","unstructured":"Wu Wen-ts\u00fcn: Basic Principles of Mechanical Theorem Proving in Geometries, Vol. I: Part of Elementary Geometries, Science Press, Beijing, 1984 (in Chinese)."},{"key":"BF00283133_CR19","unstructured":"Zhang, J. Z and Cao, P. S.: From Education of Mathematics to Mathematics for Education, Sichuan Educational Publishing Inc., 1988 (in Chinese)."},{"key":"BF00283133_CR20","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BF01531326","volume":"13","author":"J. Z. Zhang","year":"1995","unstructured":"Zhang, J. Z., Chou, S. C., and Gao, X. S., Automated production of traditional proofs for theorems in Euclidean geometry, I. The Hilbert intersection point theorems, Annals of Mathematics and Artificial Intelligence 13 (1995), 109\u2013137.","journal-title":"Annals of Mathematics and Artificial Intelligence"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00283133.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00283133\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00283133","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,18]],"date-time":"2024-12-18T17:39:23Z","timestamp":1734543563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00283133"}},"subtitle":["I. Multiple and shortest proof generation"],"short-title":[],"issued":{"date-parts":[[1996,12]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1996,12]]}},"alternative-id":["BF00283133"],"URL":"https:\/\/doi.org\/10.1007\/bf00283133","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,12]]}}}