{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T23:35:31Z","timestamp":1783726531077,"version":"3.55.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2000,10]]},"DOI":"10.1023\/a:1006171315513","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:53:09Z","timestamp":1040518389000},"page":"219-246","source":"Crossref","is-referenced-by-count":67,"title":["A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering"],"prefix":"10.1007","volume":"25","author":[{"given":"Shang-Ching","family":"Chou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiao-Shan","family":"Gao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jing-Zhong","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"192795_CR1","doi-asserted-by":"crossref","unstructured":"Bancilhon, F. and Ramakrishnan, R.: An amateur's introduction to recursive query processing strategies, in C. Zanioilo (ed.), Proc. of ACM SIGMOD Conference, 1986, pp. 16-52.","DOI":"10.1145\/16856.16859"},{"issue":"2","key":"192795_CR2","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0004-3702(88)90001-X","volume":"36","author":"W. Buntine","year":"1988","unstructured":"Buntine, W.: Generalized subsumption and its application to induction and redundancy, Artif. Intell.\n36(2) (1988), 149-179.","journal-title":"Artif. Intell."},{"key":"192795_CR3","volume-title":"Mechanical Geometry Theorem Proving","author":"S. C. Chou","year":"1988","unstructured":"Chou, S. C.: Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht, Netherlands, 1988."},{"key":"192795_CR4","first-page":"265","volume-title":"Proc. ISSAC-90","author":"S. C. Chou","year":"1990","unstructured":"Chou, S. C. and Gao, X. S.: Mechanical formula derivation in elementary geometries, in Proc. ISSAC-90, ACM, New York, 1990, pp. 265-270."},{"key":"192795_CR5","doi-asserted-by":"crossref","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z.: Machine Proofs in Geometry, World Scientific, 1994.","DOI":"10.1142\/9789812798152"},{"issue":"3","key":"192795_CR6","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00283133","volume":"17","author":"S. C. Chou","year":"1996","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z.: Automated generation of readable proofs with geometric invariants, I: Multiple and shortest proof generation, J. Automated Reasoning\n17(3) (1996), 325-347.","journal-title":"J. Automated Reasoning"},{"issue":"3","key":"192795_CR7","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF00283134","volume":"17","author":"S. C. Chou","year":"1996","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z.: Automated generation of readable proofs with geometric invariants, II: Proving theorems with full-angles, WSUCS-94-3, CS Dept, Wichita State University, March 1994, J. Automated Reasoning\n17(3) (1996), 349-370.","journal-title":"J. Automated Reasoning"},{"key":"192795_CR8","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. Automated Reasoning\n2 (1986), 329-390.","journal-title":"J. Automated Reasoning"},{"key":"192795_CR9","unstructured":"Bulmer, M. and Fearnley-Sander, D.: The kinds of truth of geometry theorems, Preprint."},{"issue":"2","key":"192795_CR10","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1145\/356924.356929","volume":"16","author":"H. Gallaire","year":"1984","unstructured":"Gallaire, H., Minker, J. and Nicola, J. M.: Logic and databases: A deductive approach, ACM Comput. Surveys\n16(2) (1984), 153-185.","journal-title":"ACM Comput. Surveys"},{"key":"192795_CR11","doi-asserted-by":"crossref","unstructured":"Gerlentner, 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-147.","DOI":"10.1145\/1460361.1460381"},{"key":"192795_CR12","unstructured":"Havel, T.: The use of distance as coordinates in computer-aided proofs of theorems in Euclidean geometry, IMA Preprint, No. 389, University of Minnesota, 1988."},{"key":"192795_CR13","unstructured":"Helm, R.: On the elimination of redundant derivations during execution, in Proc. of 1990 North American Conference on Logic Programming, The MIT Press, 1990, pp. 551-568."},{"key":"192795_CR14","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert's nullstellensatz, in Proc. SYMSAC'86, Waterloo, 1986, pp. 202-208.","DOI":"10.1145\/32439.32479"},{"key":"192795_CR15","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\n14 (1990), 511-550.","journal-title":"Cognitive Science"},{"issue":"1","key":"192795_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005819428156","volume":"21","author":"L. Hong-Bo","year":"1998","unstructured":"Hong-Bo, Li and Minteh, Cheng: Clifford algebraic reduction method for automated theorem proving in differential geometry, J. Automated Reasoning\n21(1) (1998), 1-21.","journal-title":"J. Automated Reasoning"},{"key":"192795_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"A. J. Nevins","year":"1975","unstructured":"Nevins, A. J.: Plane geometry theorem proving using forward chaining, Artif. Intell.\n6 (1975), 1-23. 18._ Recio, T. and Velex-Melon, M. P.: Automatic discovery of theorems in elementary geometry, Preprint, 1997.","journal-title":"Artif. Intell."},{"issue":"4","key":"192795_CR18","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1109\/TC.1976.1674613","volume":"C-25","author":"R. Reiter","year":"1976","unstructured":"Reiter, R.: A semantically guided deductive system for automatic theorem proving, IEEE Trans. on Computers\nC-25(4) (1976), 328-334.","journal-title":"IEEE Trans. on Computers"},{"key":"192795_CR19","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-1-4684-3384-5_3","volume-title":"Logic and Data Bases","author":"R. Reiter","year":"1978","unstructured":"Reiter, R.: On the closed world data bases, in H. Gallaire and J. Minker (eds), Logic and Data Bases, Plenum Press, New York, 1978, pp. 55-76."},{"key":"192795_CR20","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-78.","DOI":"10.1007\/978-3-642-81952-0_5"},{"key":"192795_CR21","doi-asserted-by":"crossref","unstructured":"Sagiv, Y.: Optimizing datalog programs, in J. Minker (ed.), Foundations of Deductive Databases and Logic Programming, Morgan Kauffmann, 1988, pp. 659-698.","DOI":"10.1016\/B978-0-934613-40-8.50021-X"},{"key":"192795_CR22","doi-asserted-by":"crossref","unstructured":"Wang, D. M.: Reasoning about geometric problems using an elimination method, in J. Pfalzgraf and D. M. Wang (eds), Automated Practical Reasoning, Springer-Verlag, 1995, pp. 148-185.","DOI":"10.1007\/978-3-7091-6604-8_8"},{"key":"192795_CR23","unstructured":"White, N. L. and Mcmillan, T.: Cayley factorization, in Proc. ISSAC'88, ACM Press, 1988, pp. 4-8."},{"key":"192795_CR24","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"Wos, L.: Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey, 1988."},{"key":"192795_CR25","volume-title":"Basic Principles of Mechanical Theorem Proving in Geometries, Volume I: Part of Elementary Geometries","author":"W. Wen-ts\u00fcn","year":"1984","unstructured":"Wu Wen-ts\u00fcn: Basic Principles of Mechanical Theorem Proving in Geometries, Volume I: Part of Elementary Geometries, Science Press, Beijing (in Chinese), 1984. English version, Springer-Verlag, 1993."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006171315513.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006171315513\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006171315513.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:40:28Z","timestamp":1749123628000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006171315513"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,10]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,10]]}},"alternative-id":["192795"],"URL":"https:\/\/doi.org\/10.1023\/a:1006171315513","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,10]]}}}