{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T13:53:45Z","timestamp":1756994025341},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1986,9,1]],"date-time":"1986-09-01T00:00:00Z","timestamp":525916800000},"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":[[1986,9]]},"DOI":"10.1007\/bf02328448","type":"journal-article","created":{"date-parts":[[2006,3,14]],"date-time":"2006-03-14T12:24:33Z","timestamp":1142339073000},"page":"253-273","source":"Crossref","is-referenced-by-count":42,"title":["Proving geometry theorems with rewrite rules"],"prefix":"10.1007","volume":"2","author":[{"given":"Shang-Ching","family":"Chou","sequence":"first","affiliation":[]},{"given":"William F.","family":"Schelter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF02328448_CR1","unstructured":"M. Artin and W. Schelter, Graded Algebras of Global Dimension 3, Preprint (1985)."},{"key":"BF02328448_CR2","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/BF01844169","volume":"4","author":"B. Buchberger","year":"1970","unstructured":"B.Buchberger, \u201cAn Algorithm Criterion for the Solvability of a System of Algebraic Equations\u2019 (German),Aequationes Math.4 (1970), 374\u2013383.","journal-title":"Aequationes Math"},{"key":"BF02328448_CR3","doi-asserted-by":"crossref","unstructured":"B. Buchberger, \u201cGr\u00f6bner Bases: An Algorithmic Method in Polynomial Ideal Theory\u201d, Chapter 6 inRecent Trends in Multidimensional Systems Theory, N.K. Bose (ed.) D. Reidel Publ. Comp. 1985.","DOI":"10.1007\/978-94-009-5225-6_6"},{"key":"BF02328448_CR4","doi-asserted-by":"crossref","unstructured":"S.C. Chou, \u201cProving Elementary Geometry Theorems Using Wu's Algorithm\u201d, inAutomated Theorem Proving: After 25 years, Ed. By W.W. Bledsoe and D. Loveland, AMS Contemporary Mathematics Series29 (1984), 243\u2013286.","DOI":"10.1090\/conm\/029\/14"},{"key":"BF02328448_CR5","unstructured":"S.C. Chou, \u201cProving and Discovering Theorems in Elementary Geometries Using Wu's Method\u201d, PhD Thesis, Department of Mathematics, University of Texas, Austin (1985)."},{"key":"BF02328448_CR6","volume-title":"Foundations of Geometry","author":"D. Hilbert","year":"1971","unstructured":"D.Hilbert,Foundations of Geometry, Open Court Publishing Company, La Salla, Illinois, 1971."},{"key":"BF02328448_CR7","unstructured":"Dallas Lankford et al., \u201cDickson's Lemma, Hilbert's Basis Theorem, and Applications to Completion in Commutative Noetherian Rings\u201d, preprint, Department of Mathematics and Statistics, Louisiana Tech University."},{"key":"BF02328448_CR8","doi-asserted-by":"crossref","DOI":"10.1090\/coll\/033","volume-title":"Differential Algebra","author":"R. F. Ritt","year":"1950","unstructured":"R. F.Ritt,Differential Algebra, AMS Colloquium Publications, New York, 1950."},{"key":"BF02328448_CR9","first-page":"157","volume":"21","author":"Wu Wen-ts\u00fcn","year":"1978","unstructured":"WuWen-ts\u00fcn, \u201cOn the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry\u201d,Scientia Sinica 21 (1978) 157\u2013179.","journal-title":"Scientia Sinica"},{"issue":"3","key":"BF02328448_CR10","first-page":"207","volume":"4","author":"Wu Wen-ts\u00fcn","year":"1984","unstructured":"WuWen-ts\u00fcn, \u201cBasic Principles of Mechanical Theorem Proving in Geometries\u201d,J. of Sys. Sci. and Math. Sci. 4 (3) (1984), 207\u2013235.","journal-title":"J. of Sys. Sci. and Math. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02328448.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02328448\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02328448","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T14:07:36Z","timestamp":1558015656000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02328448"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986,9]]},"references-count":10,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1986,9]]}},"alternative-id":["BF02328448"],"URL":"https:\/\/doi.org\/10.1007\/bf02328448","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1986,9]]}}}