{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,3]],"date-time":"2026-01-03T14:43:05Z","timestamp":1767451385341,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642253782"},{"type":"electronic","value":"9783642253799"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-25379-9_8","type":"book-chapter","created":{"date-parts":[[2011,11,13]],"date-time":"2011-11-13T20:33:47Z","timestamp":1321216427000},"page":"71-86","source":"Crossref","is-referenced-by-count":12,"title":["Formalization of Wu\u2019s Simple Method in Coq"],"prefix":"10.1007","author":[{"given":"Jean-David","family":"G\u00e9nevaux","sequence":"first","affiliation":[]},{"given":"Julien","family":"Narboux","sequence":"additional","affiliation":[]},{"given":"Pascal","family":"Schreck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"LNCS","first-page":"357","volume-title":"CPP 2011","author":"M. Boespflug","year":"2011","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full Reduction at Full Throttle. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 357\u2013372. Springer, Heidelberg (2011)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-52885-7_89","volume-title":"10th International Conference on Automated Deduction","author":"S.-C. Chou","year":"1990","unstructured":"Chou, S.-C., Gao, X.-S.: Ritt-Wu\u2019s Decomposition Algorithm and Geometry Theorem Proving. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 207\u2013220. Springer, Heidelberg (1990)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/3-540-55602-8_153","volume-title":"Automated Deduction - CADE-11","author":"S.-C. Chou","year":"1992","unstructured":"Chou, S.-C., Gao, X.-S.: A Class of Geometry Statements of Constructive Type and Geometry Theorem Proving. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 20\u201334. Springer, Heidelberg (1992)"},{"key":"8_CR4","doi-asserted-by":"publisher","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry","author":"S.-C. Chou","year":"1994","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Chou, S.-C.: Mechanical Geometry Theorem Proving. D.\u00a0Reidel Publishing Company (1988)","DOI":"10.1007\/978-94-009-4037-6"},{"key":"8_CR6","unstructured":"Coq development team. The Coq proof assistant reference manual, Version 8.3. LogiCal Project (2010)"},{"key":"8_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-73086-6_3","volume-title":"Towards Mechanized Mathematical Assistants","author":"A. Chaieb","year":"2007","unstructured":"Chaieb, A., Wenzel, M.: Context Aware Calculation and Deduction. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 27\u201339. Springer, Heidelberg (2007)"},{"key":"8_CR8","series-title":"LNAI","first-page":"51","volume-title":"ADG 2010","author":"L. Fuchs","year":"2011","unstructured":"Fuchs, L., Th\u00e9ry, L.: A Formalization of Grassmann-Cayley Algebra in Coq and its Application to Theorems Proving in Projective Geometry. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS (LNAI), vol.\u00a06877, pp. 51\u201367. Springer, Heidelberg (2011)"},{"key":"8_CR9","unstructured":"Gao, X.-S.: Geometry expert, software package (2000)"},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0010-4485(97)00052-3","volume":"30","author":"X.-S. Gao","year":"1998","unstructured":"Gao, X.-S., Chou, S.-C.: Solving geometric constraint systems. I. A global propagation approach. Computer Aided Design\u00a030(1), 47\u201354 (1998)","journal-title":"Computer Aided Design"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/S0010-4485(97)00055-9","volume":"30","author":"X.-S. Gao","year":"1998","unstructured":"Gao, X.-S., Chou, S.-C.: Solving geometric constraint systems. II. A symbolic approach and decision of Rc-constructibility. Computer Aided Design\u00a030(2), 115\u2013122 (1998)","journal-title":"Computer Aided Design"},{"key":"8_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24616-9_4","volume-title":"Automated Deduction in Geometry","author":"X.-S. Gao","year":"2004","unstructured":"Gao, X.-S., Lin, Q.: MMP\/Geometer \u2013 A Software Package for Automated Geometric Reasoning. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol.\u00a02930, pp. 44\u201366. Springer, Heidelberg (2004)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving Equalities in a Commutative Ring Done Right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 98\u2013113. Springer, Heidelberg (2005)"},{"key":"8_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-21046-4_3","volume-title":"Automated Deduction in Geometry","author":"B. Gr\u00e9goire","year":"2011","unstructured":"Gr\u00e9goire, B., Pottier, L., Th\u00e9ry, L.: Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS (LNAI), vol.\u00a06301, pp. 42\u201359. Springer, Heidelberg (2011)"},{"key":"8_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-73595-3_5","volume-title":"Automated Deduction \u2013 CADE-21","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Automating Elementary Number-Theoretic Proofs Using Gr\u00f6bner Bases. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 51\u201366. Springer, Heidelberg (2007)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-03359-9_3","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2009","unstructured":"Harrison, J.: Without Loss of Generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 43\u201359. Springer, Heidelberg (2009)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P., Narboux, J., Quaresma, P.: The Area Method: a Recapitulation. Journal of Automated Reasoning (2010)","DOI":"10.1007\/s10817-010-9209-7"},{"key":"8_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/11814771_13","volume-title":"Automated Reasoning","author":"P. Jani\u010di\u0107","year":"2006","unstructured":"Jani\u010di\u0107, P., Quaresma, P.: System Description: GCLCprover + Geothms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 145\u2013150. Springer, Heidelberg (2006)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry Theorem Proving using Hilbert\u2019s Nullstellensatz. In: SYMSAC 1986: Proceedings of the fifth ACM Symposium on Symbolic and Algebraic Computation, New York, NY, USA, pp. 202\u2013208. ACM Press (1986)","DOI":"10.1145\/32439.32479"},{"key":"8_CR20","unstructured":"Mahboubi, A.: Contributions \u00e0 la certification des calculs dans R: th\u00e9orie, preuves, programmation. PhD thesis, Universit\u00e9 de Nice Sophia-Antipolis (November 2006)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-30142-4_17","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Narboux","year":"2004","unstructured":"Narboux, J.: A Decision Procedure for Geometry in Coq. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 225\u2013240. Springer, Heidelberg (2004)"},{"issue":"2","key":"8_CR22","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-007-9071-4","volume":"39","author":"J. Narboux","year":"2007","unstructured":"Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reasoning\u00a039(2), 161\u2013180 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-21898-9_32","volume-title":"Computational Science and Its Applications - ICCSA 2011","author":"T.-M. Pham","year":"2011","unstructured":"Pham, T.-M., Bertot, Y., Narboux, J.: A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. In: Murgante, B., Gervasi, O., Iglesias, A., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2011, Part IV. LNCS, vol.\u00a06785, pp. 368\u2013383. Springer, Heidelberg (2011)"},{"key":"8_CR24","unstructured":"Pham, T.M.: An Additional Tool About the Orientation for Theorem Proving in the Coq Proof Assitant. In: Proceedings of Automated Deduction in Geometry, ADG 2010 (2010)"},{"key":"8_CR25","unstructured":"Pottier, L.: Connecting Gr\u00f6bner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Knowledge Exchange: Automated Provers and Proof Assistants. CEUR Workshop Proceedings, Doha, Qatar p. 418 (2008)"},{"key":"8_CR26","unstructured":"Robu, J.: Geometry Theorem Proving in the Frame of the Theorema Project. PhD thesis, Johannes Kepler Universitt, Linz (September 2002)"},{"key":"8_CR27","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01231031","volume":"36","author":"D. Wang","year":"1989","unstructured":"Wang, D.: A new theorem discovered by computer prover. Journal of Geometry\u00a036, 173\u2013182 (1989), doi:10.1007\/BF01231031","journal-title":"Journal of Geometry"},{"key":"8_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6202-6","volume-title":"Elimination Method","author":"D. Wang","year":"2001","unstructured":"Wang, D.: Elimination Method. Springer, Heidelberg (2001)"},{"key":"8_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-540-24616-9_12","volume-title":"Automated Deduction in Geometry","author":"D. Wang","year":"2004","unstructured":"Wang, D.: GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol.\u00a02930, pp. 194\u2013215. Springer, Heidelberg (2004)"},{"key":"8_CR30","doi-asserted-by":"publisher","DOI":"10.1142\/p318","volume-title":"Elimination Practice","author":"D. Wang","year":"2004","unstructured":"Wang, D.: Elimination Practice. Springer, Heidelberg (2004)"},{"key":"8_CR31","first-page":"157","volume":"21","author":"W.-T. Wu","year":"1978","unstructured":"Wu, W.-T.: On the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry. Scientia Sinica\u00a021, 157\u2013179 (1978)","journal-title":"Scientia Sinica"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-21046-4_10","volume-title":"Automated Deduction in Geometry","author":"Z. Ye","year":"2011","unstructured":"Ye, Z., Chou, S.-C., Gao, X.-S.: An Introduction to Java Geometry Expert. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol.\u00a06301, pp. 189\u2013195. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25379-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T09:39:02Z","timestamp":1560937142000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25379-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253782","9783642253799"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25379-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}