{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T14:58:58Z","timestamp":1775228338369,"version":"3.50.1"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1995,3,1]],"date-time":"1995-03-01T00:00:00Z","timestamp":794016000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1995,3]]},"DOI":"10.1007\/bf01531326","type":"journal-article","created":{"date-parts":[[2005,4,19]],"date-time":"2005-04-19T00:34:59Z","timestamp":1113870899000},"page":"109-137","source":"Crossref","is-referenced-by-count":20,"title":["Automated production of traditional proofs for theorems in Euclidean geometry I. The Hilbert intersection point theorems"],"prefix":"10.1007","volume":"13","author":[{"given":"Jing-Zhong","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shang-Ching","family":"Chou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiao-Shan","family":"Gao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1090\/conm\/029\/14","volume":"29","author":"S.C. Chou","year":"1984","unstructured":"S.C. Chou, Proving elementary geometry theorems using Wu's algorithm,Automated Theorem Proving: After 25 Years (Amer. Math. Soc.), Contemporary Mathematics 29(1984)243?286.","journal-title":"Contemporary Mathematics"},{"key":"CR2","volume-title":"Mechanical Geometry Theorem Proving","author":"S.C. Chou","year":"1988","unstructured":"S.C. Chou,Mechanical Geometry Theorem Proving (Reidel, Dordrecht, 1988)."},{"key":"CR3","unstructured":"S.C. Chou, X.S. Gao and J.Z. Zhang, Automated production of traditional proofs for theorems in Euclidean geometry: IV, A collection of 400 geometry theorems, WSUCS-92-7 (1992)."},{"key":"CR4","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1145\/96877.96946","volume-title":"Proc. ISSAC-90","author":"S.C. Chou","year":"1990","unstructured":"S.C. Chou and X.S. Gao, Mechanical formula derivation in elementary geometries,Proc. ISSAC-90 (ACM, New York, 1990) pp. 265?270."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"S.C. Chou and X.S. Gao, Proving constructive geometry statements, in:CADE11, ed. D. Kapur, Lecture Notes on Comp. Sci. 607 (Springer, 1992) pp. 20?34.","DOI":"10.1007\/3-540-55602-8_153"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF02328448","volume":"2","author":"S.C. Chou","year":"1986","unstructured":"S.C. Chou and W.F. Schelter, Proving geometry theorems with rewrite rules, J. Autom. Reasoning 2(1986)253?273.","journal-title":"J. Autom. Reasoning"},{"key":"CR7","unstructured":"X.S. Gao and D.M. Wang, Geometry theorems proved mechanically using Wu's method, Part on elementary geometries, MM Preprint No. 2 (1987)."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"H. Gelernter, J.R. Hanson and D.W. Loveland, Empirical explorations of the geometry-theorem proving machine,Proc. West. Joint Computer Conf., 1960, pp. 143?147.","DOI":"10.1145\/1460361.1460381"},{"key":"CR9","volume-title":"Foundations of Geometry","author":"D. Hilbert","year":"1971","unstructured":"D. Hilbert,Foundations of Geometry (Open Court Publ. Comp., Lasalla, IL, 1971)."},{"key":"CR10","first-page":"824","volume":"29","author":"J.W. Hong","year":"1986","unstructured":"J.W. Hong, Can a geometry theorem be proved by an example?, Sci. Sinica 29(1986)824?834.","journal-title":"Sci. Sinica"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"D. Kapur, Geometry theorem proving using Hilbert's nullstellensatz,Proc. SYMSAC '86, Waterloo, 1986, pp. 202?208.","DOI":"10.1145\/32439.32479"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1207\/s15516709cog1404_2","volume":"14","author":"K.R. Koedinger","year":"1990","unstructured":"K.R. Koedinger and J.R. Anderson, Abstract planning and perceptual chunks: Elements of expertise in geometry, Cognitive Sci. 14(1990)511?550.","journal-title":"Cognitive Sci."},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"B. Kutzler and S. Stifter, Automated geometry theorem proving using Buchberger's algorithm,Proc. SYMSAC '86, Waterloo, 1986, pp. 209?214.","DOI":"10.1145\/32439.32480"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J.D. McCharen","year":"1976","unstructured":"J.D. McCharen, R.A. Overbeek and L.A. Wos, Problems and experiments for and with automated theorem-proving programs, IEEE Trans. Comp. C-25(1976)773?782.","journal-title":"IEEE Trans. Comp."},{"key":"CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"A.J. Nevins","year":"1977","unstructured":"A.J. Nevins, Plane geometry theorem proving using forward chaining, Artificial Intelligence 6(1977)1?23.","journal-title":"Artificial Intelligence"},{"key":"CR16","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, Sci. Sinica 21(1978)159?172. Also in:Automated Theorem Proving: After 25 Years (Amer. Math. Soc.), Contemporary Mathematics 29(1984)213?234.","journal-title":"Sci. Sinica"},{"key":"CR17","first-page":"207","volume":"4","author":"Wu Wen-ts\u00fcn","year":"1984","unstructured":"Wu Wen-ts\u00fcn, Basic principles of mechanical theorem proving in elementary geometries, J. Syst. Sci. Math. Sci. 4(1984)207?235. Also in: J. Autom. Reasoning 2(1986)221?252.base.","journal-title":"J. Syst. Sci. Math. Sci."},{"key":"CR18","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/S0252-9602(18)30628-3","volume":"2","author":"Wu Wen-ts\u00fcn","year":"1982","unstructured":"Wu Wen-ts\u00fcn, Toward mechanization of geometry ? some comments on Hilbert's ?Grundlagen der Geometrie?, Acta Math. Sci. 2(1982)125?138.","journal-title":"Acta Math. Sci."},{"key":"CR19","unstructured":"L. Yang, J.Z. Zhang and X.R. Hou, A criterion of dependency between algebraic equations and its application,Proc. 1992 Int. Workshop on Mechanization of Mathematics (Inter. Academic Publ.) pp. 110?134."},{"key":"CR20","unstructured":"J.Z. Zhang,How to Solve Geometry Problems Using Areas (Shanghai Educ. Publ. 1982), in Chinese."},{"key":"CR21","unstructured":"J.Z. Zhang,A New Approach to Plane Geometry (Sichuan Educ. Publ., 1992), in Chinese."},{"key":"CR22","unstructured":"J.Z. Zhang and P.S. Cao,From Education of Mathematics to Mathematics for Education (Sichuan Educ. Publ., 1988), in Chinese."},{"key":"CR23","doi-asserted-by":"crossref","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 and M.K. Deng, The parallel numerical method of mechanical theorem proving, Theor. Comp. Sci. 74(1990)253?271.","journal-title":"Theor. Comp. Sci."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01531326\/fulltext.html","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01531326.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01531326\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01531326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,31]],"date-time":"2024-12-31T19:42:31Z","timestamp":1735674151000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01531326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,3]]},"references-count":23,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1995,3]]}},"alternative-id":["BF01531326"],"URL":"https:\/\/doi.org\/10.1007\/bf01531326","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,3]]}}}