{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:56:18Z","timestamp":1725494178664},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425984"},{"type":"electronic","value":"9783540454106"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45410-1_16","type":"book-chapter","created":{"date-parts":[[2007,11,5]],"date-time":"2007-11-05T12:16:33Z","timestamp":1194264993000},"page":"268-305","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization"],"prefix":"10.1007","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Puitg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,9,11]]},"reference":[{"key":"16_CR1","first-page":"197","volume-title":"Le concept de preuve \u00e0 la lumi\u00e8re de l\u2019intelligence artificielle","author":"N. Balacheff","year":"1999","unstructured":"N. Balacheff. Apprendre la preuve. In J. Sallantin and J.-J. Szczeniarz (eds.), Le concept de preuve \u00e0 la lumi\u00e8re de l\u2019intelligence artificielle, pages 197\u2013236. PUF, Paris, 1999."},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"W. W. Bledsoe. Non-resolution theorem proving. Artificial Intelligence, 9:1\u201335, 1977.","journal-title":"Artificial Intelligence"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"C. Bourely, G. D\u00e9fourneaux, and N. Peltier. Building proofs or counterexamples by analogy in a resolution framework. In Proceedings of JELIA 96, LNAI 1126, pages 34\u201349. Springer, 1996.","DOI":"10.1007\/3-540-61630-6_3"},{"issue":"2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1006\/jsco.1995.1013","volume":"19","author":"R. Caferra","year":"1995","unstructured":"R. Caferra and M. Herment. A generic graphic framework for combining inference tools and editing proofs and formulae. Journal of Symbolic Computation, 19(2):217\u2013243, 1995.","journal-title":"Journal of Symbolic Computation"},{"key":"16_CR5","series-title":"Lect Notes Comput Sci","first-page":"2","volume-title":"Fundamentals of Artificial Intelligence Research","author":"R. Caferra","year":"1991","unstructured":"R. Caferra, M. Herment, and N. Zabel. User-oriented theorem proving with the ATINF graphic proof editor. In Fundamentals of Artificial Intelligence Research, LNCS 535, pages 2\u201310. Springer, 1991."},{"key":"16_CR6","unstructured":"R. Caferra and N. Peltier. Extending semantic resolution via automated model building: Applications. In Proceeding of IJCAI\u201995, pages 328\u2013334. Morgan Kaufman, 1995."},{"key":"16_CR7","unstructured":"R. Caferra and N. Peltier. Disinference rules, model building and abduction. Logic at Work. Essays dedicated to the memory of Helena Rasiowa (Part 5: Logic in Computer Science, Chap. 20). Physica-Verlag, 1998."},{"issue":"3","key":"16_CR8","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"S.-C. Chou","year":"2000","unstructured":"S.-C. Chou, X.-S. Gao, and J.-Z. Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25(3):219\u2013246, 2000.","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"S.-C. Chou. Mechanical Geometry Theorem Proving. Mathematics and its Applications. D. Reidel, 1988.","DOI":"10.1007\/978-94-009-4037-6"},{"issue":"4","key":"16_CR10","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H. Coelho","year":"1986","unstructured":"H. Coelho and L. Moniz Pereira. Automated reasoning in geometry theorem proving with Prolog. Journal of Automated Reasoning, 2(4):329\u2013390, 1986.","journal-title":"Journal of Automated Reasoning"},{"issue":"1-2","key":"16_CR11","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1023\/A:1005944606876","volume":"20","author":"G. D\u00e9fourneaux","year":"1998","unstructured":"G. D\u00e9fourneaux, C. Bourely, and N. Peltier. Semantic generalizations for proving and disproving conjectures by analogy. Journal of Automated Reasoning, 20(1-2):27\u201345, 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR12","unstructured":"G. D\u00e9fourneaux and N. Peltier. Analogy and abduction in automated reasoning. In M. E. Pollack (ed.), Proceedings of IJCAI\u201997, pages 216\u2013225. Morgan Kaufmann, 1997."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"G. D\u00e9fourneaux and N. Peltier. Partial matching for analogy discovery in proofs and counter-examples. In W. McCune (ed.), Proceedings of CADE-14, LNAI 1249, pages 431\u2013445. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_43"},{"issue":"1","key":"16_CR14","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1093\/jigpal\/6.1.17","volume":"6","author":"C. Ferm\u00fcller","year":"1998","unstructured":"C. Ferm\u00fcller and A. Leitsch. Decision procedures and model building in equational clause logic. Journal of the IGPL, 6(1):17\u201341, 1998.","journal-title":"Journal of the IGPL"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"H. Gelernter, J. Hansen, and D. Loveland. Empirical explorations of the geometry theorem-proving machine. In J. Siekmann and G. Wrightson (eds.), Automation of Reasoning, vol. 1, pages 140\u2013150. Springer, 1983. Originally published in 1960.","DOI":"10.1007\/978-3-642-81952-0_10"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"H. Hong, D. Wang, and F. Winkler. Algebraic Approaches to Geometric Reasoning. Special issue of the Annals of Mathematics and Artificial Intelligence 13 (1\u20132). Baltzer, Amsterdam, 1995.","DOI":"10.1007\/BF01531320"},{"issue":"3","key":"16_CR17","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch. Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. Journal of the ACM, 38(3):559\u2013587, 1991.","journal-title":"Journal of the ACM"},{"key":"16_CR18","unstructured":"D. Kapur and J. E. Mundy. Geometric Reasoning. MIT Press, 1989."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"A. Leitsch. The Resolution Calculus. Texts in Theoretical Computer Science. Springer, 1997.","DOI":"10.1007\/978-3-642-60605-2"},{"key":"16_CR20","first-page":"475","volume-title":"Artificial Intelligence and Education","author":"V. Luengo","year":"1999","unstructured":"V. Luengo. A semi-empirical agent for learning mathematical proof. In S. P. Lajoie and M. Vivet (eds.), Artificial Intelligence and Education, pages 475\u2013482. IOS Press, Amsterdam, 1999."},{"key":"16_CR21","volume-title":"Th\u00e8se de doctorat","author":"V. Luengo","year":"1997","unstructured":"V. Luengo. Cabri-Euclide: Un micromonde de preuve int\u00e9grant la r\u00e9futation. Th\u00e8se de doctorat, I.N.P.G., France, Septembre 1997."},{"key":"16_CR22","unstructured":"N. Peltier. Combining resolution and enumeration for finite model building. In P. Baumgartner and H. Zhang (eds.), FTP\u201900 (Third International Workshop on First-Order Theorem Proving), St-Andrews, Scotland, pages 170\u2013181. Technical Report, Universit\u00e4t Koblenz-Landau, July 2000."},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"N. Peltier. On the decidability of the PVD class with equality. Technical report, LEIBNIZ Laboratory, 2000. To appear in the Logic Journal of the IGPL.","DOI":"10.1093\/jigpal\/9.4.569"},{"issue":"3","key":"16_CR24","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D. A. Plaisted","year":"2000","unstructured":"D. A. Plaisted and Y. Zhu. Ordered semantic hyperlinking. Journal of Automated Reasoning, 25(3):167\u2013217, 2000.","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR25","unstructured":"G. Polya. How to Solve It: A New Aspect of Mathematical Method (second edition). Princeton University Press, 1973."},{"key":"16_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BFb0055149","volume-title":"Theorem Proving in Higher-Order Logics","author":"F. Puitg","year":"1998","unstructured":"F. Puitg and J.-F. Dufourd. Formal specifications and theorem proving breakthroughs in geometric modelling. In Theorem Proving in Higher-Order Logics, LNCS 1479, pages 401\u2013422. Springer, 1998."},{"key":"16_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(98)00228-X","volume":"234","author":"F. Puitg","year":"2000","unstructured":"F. Puitg and J.-F. Dufourd. Formalizing mathematics in higher-order logic: A case study in geometric modelling. Theoretical Computer Science, 234:1\u201357, 2000.","journal-title":"Theoretical Computer Science"},{"key":"16_CR28","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF00245024","volume":"5","author":"A. Quaife","year":"1989","unstructured":"A. Quaife. Automated development of Tarski\u2019s geometry. Journal of Automated Reasoning, 5:97\u2013118, 1989.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"16_CR29","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1023\/A:1006135322108","volume":"23","author":"T. Recio","year":"1999","unstructured":"T. Recio and M. V\u00e9lez. Automatic discovery of theorems in elementary geometry. Journal of Automated Reasoning, 23(1):63\u201382, 1999.","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"16_CR30","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1109\/TC.1976.1674613","volume":"C-25","author":"R. Reiter","year":"1976","unstructured":"R. Reiter. A semantically guided deductive system for automatic theorem proving. IEEE Transactions on Computers, C-25(4):328\u2013334, 1976.","journal-title":"IEEE Transactions on Computers"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"J. Richter-Gebert and U. Kortenkamp. The Interactive Geometry Software Cinderella. Springer, 2000.","DOI":"10.1007\/978-3-642-58318-6"},{"key":"16_CR32","volume-title":"Th\u00e8se d\u2019\u00e9tat","author":"M. Rusinowitch","year":"1987","unstructured":"M. Rusinowitch. D\u00e9monstration automatique par des techniques de r\u00e9\u00e9criture. Th\u00e8se d\u2019\u00e9tat, Universit\u00e9 Nancy 1, France, 1987. Also available as textbook, Inter Editions, Paris, 1989."},{"issue":"4","key":"16_CR33","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J. R. Slagle","year":"1967","unstructured":"J. R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687\u2013697, 1967.","journal-title":"Journal of the ACM"},{"key":"16_CR34","first-page":"109","volume":"1","author":"J. Slaney","year":"1993","unstructured":"J. Slaney. scott: A model-guided theorem prover. In Proceedings IJCAI-93, vol. 1, pages 109\u2013114. Morgan Kaufmann, 1993.","journal-title":"Proceedings IJCAI-93"},{"key":"16_CR35","unstructured":"L. Wos. Automated Reasoning: 33 Basic Research Problems. Prentice Hall, 1988."},{"key":"16_CR36","unstructured":"L. Wos, R. Overbeek, E. Lush, and J. Boyle. Automated Reasoning: Introduction and Applications (second edition). McGraw-Hill, 1992."},{"key":"16_CR37","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. Robinson, and D. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM, 12:536\u2013541, 1965.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Geometry"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45410-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T16:24:46Z","timestamp":1684081486000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45410-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425984","9783540454106"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-45410-1_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"11 September 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}