{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:14:45Z","timestamp":1742912085591,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642250699"},{"type":"electronic","value":"9783642250705"}],"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-25070-5_7","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T01:30:55Z","timestamp":1320802255000},"page":"118-131","source":"Crossref","is-referenced-by-count":0,"title":["Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry"],"prefix":"10.1007","author":[{"given":"Dominique","family":"Michelucci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Apel, S., Richter-Gebert, J.: Cancellation patterns in automatic geometric theorem proving. Talk at ADG 2010, Munich, Germany (July 2010)","DOI":"10.1007\/978-3-642-25070-5_1"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00283133","volume":"17","author":"S.C. Chou","year":"1996","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants, ii. theorem proving with full-angles. J. Automated Reasoning\u00a017, 325\u2013347 (1996)","journal-title":"J. Automated Reasoning"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"S.-C. Chou","year":"2000","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: A deductive database approach to automated geometry theorem proving and discovering. J. Autom. Reason.\u00a025, 219\u2013246 (2000)","journal-title":"J. Autom. Reason."},{"key":"7_CR4","volume-title":"Projective Geometry","author":"H. Coxeter","year":"1987","unstructured":"Coxeter, H.: Projective Geometry. Springer, Heidelberg (1987)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Gao, X.-S.: Chapter 10: Search methods revisited. In: Gao, X.-S., Wang, D. (eds.) Mathematics Mechanization and Application, pp. 253\u2013272. Academic Press (2000)","DOI":"10.1016\/B978-012734760-8\/50011-9"},{"key":"7_CR6","unstructured":"Gelernter, H.: Realization of a geometry theorem proving machine. In: IFIP Congress, pp. 273\u2013281 (1959)"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-81952-0_8","volume-title":"Automation of Reasoning 1: Classical Papers on Computational Logic 1957-1966","author":"H. Gelernter","year":"1983","unstructured":"Gelernter, H.: Realization of a geometry-theorem proving machine. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 1: Classical Papers on Computational Logic 1957-1966, pp. 99\u2013122. Springer, Heidelberg (1983)"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-81952-0_10","volume-title":"Automation of Reasoning 1: Classical Papers on Computational Logic 1957-1966","author":"H. Gelernter","year":"1983","unstructured":"Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of the geometry-theorem proving machine. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 1: Classical Papers on Computational Logic 1957-1966, pp. 140\u2013150. Springer, Heidelberg (1983)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Desargues\u2019 theorem in Coq using ranks. In: Shin and Ossowski [16], pp. 1110\u20131115","DOI":"10.1145\/1529282.1529527"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Michelucci, D., Foufou, S.: Interrogating witnesses for geometric constraints solving. In: ACM Conf. Solid and Physical Modelling, San Francisco, pp. 343\u2013348 (2009)","DOI":"10.1145\/1629255.1629301"},{"issue":"5-6","key":"7_CR11","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1142\/S0218195906002130","volume":"16","author":"D. Michelucci","year":"2006","unstructured":"Michelucci, D., Schreck, P.: Incidence constraints: a combinatorial approach. Int. J. Comput. Geometry Appl.\u00a016(5-6), 443\u2013460 (2006)","journal-title":"Int. J. Comput. Geometry Appl."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Michelucci, D., Schreck, P., Thierry, S.E.B., F\u00fcnfzig, C., G\u00e9nevaux, J.-D.: Using the witness method to detect rigid subsystems of geometric constraints in CAD. In: SPM 2010: Proceedings of the ACM Conference on Solid and Physical Modeling, Ha\u00effa, Isra\u00ebl. ACM (September 2010)","DOI":"10.1145\/1839778.1839791"},{"key":"7_CR13","unstructured":"Pouzergues, R.: Les hexamys, web document (2002) (in French)"},{"key":"7_CR14","unstructured":"Richter-Gebert, J.: Meditations on Ceva\u2019s theorem. In: Davis, C., Ellers, E. (eds.) The Coxeter Legacy: Reflections and Projections, pp. 227\u2013254. Fields\u00a0Institute American Mathematical\u00a0Society (2006)"},{"key":"7_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17286-1","volume-title":"Perspectives on Projective Geometry: A Guided Tour Through Real and Complex Geometry","author":"J. Richter-Gebert","year":"2011","unstructured":"Richter-Gebert, J.: Perspectives on Projective Geometry: A Guided Tour Through Real and Complex Geometry. Springer, Heidelberg (2011)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Shin, S.Y., Ossowski, S. (eds.): Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), Honolulu, Hawaii, USA, March 9-12. ACM (2009)","DOI":"10.1145\/1529282"},{"key":"7_CR17","unstructured":"Wilson, S., Fleuriot, J.D.: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In: Proceedings of the European Joint Conferences on Theory and Practice of Software (ETAPS) Satellite Workshop on User Interfaces for Theorem Provers (UITP), Edinburgh, UK (April 2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Geometry"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25070-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T22:33:21Z","timestamp":1741905201000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25070-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642250699","9783642250705"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25070-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}