{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T10:02:40Z","timestamp":1771063360840,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425984","type":"print"},{"value":"9783540454106","type":"electronic"}],"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_17","type":"book-chapter","created":{"date-parts":[[2007,11,5]],"date-time":"2007-11-05T12:16:33Z","timestamp":1194264993000},"page":"306-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Higher-Order Intuitionistic Formalization and Proofs in Hilbert\u2019s Elementary Geometry"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Dehlinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Dufourd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Schreck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,9,11]]},"reference":[{"key":"17_CR1","unstructured":"Balbiani, P., Dugat, V., Fari\u00f1as del Cerro, L., Lopez, A.: El\u00e9ments de G\u00e9om\u00e9trie M\u00e9canique. Herm\u00e8es (1994)."},{"key":"17_CR2","unstructured":"Barras, B. et al.: The Coq Proof Assistant Reference Manual (Version 6.3.1). INRIA (1999), \n                  http:\/\/pauillac.inria.fr\/coq\/doc\/main.html"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Chou, S.-C.: Mechanical Geometry Theorem Proving. D. Reidel (1988).","DOI":"10.1007\/978-94-009-4037-6"},{"key":"17_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/3-540-15983-5_13","volume-title":"EUROCAL\u2019 85","author":"T. Coquand","year":"1985","unstructured":"Coquand, T., Huet, G.: Constructions: A higher order proof system for mechanizing mathematics. EUROCAL\u2019 85, Linz, LNCS 203, Springer-Verlag (1985), 151\u2013184."},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. P. Martin-L\u00f6f and G. Mints, editors, COLOG-88, LNCS 417, Springer-Verlag (1990), 50\u201366."},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0004-3702(97)00070-2","volume":"99","author":"J.-F. Dufourd","year":"1998","unstructured":"Dufourd, J.-F., Mathis, P., Schreck, P.: Geometric construction by assembling solved subfigures. Artificial Intelligence 99 (1998), 73\u2013119.","journal-title":"Artificial Intelligence"},{"key":"17_CR7","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0925-7721(00)00004-3","volume":"16","author":"J.-F. Dufourd","year":"2000","unstructured":"Dufourd, J.-F., Puitg, F.: Functional specification and prototyping with combinatorial maps. Computational Geometry-Theory and Applications 16 (2000), 129\u2013156.","journal-title":"Computational Geometry-Theory and Applications"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Essert-Villard, C., Schreck, P., Dufourd, J.-F.: Sketch-based pruning of a solution space within a formal geometric constraint solver. Submitted (2000).","DOI":"10.1016\/S0004-3702(00)00061-8"},{"key":"17_CR9","unstructured":"Gelernter, H.: Realization of a geometry theorem proving machine. Computers and Thought, Mac Graw Hill (1963), 134\u2013163."},{"key":"17_CR10","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (1989)."},{"key":"17_CR11","unstructured":"Heyting, A.: Intuitionism-An Introduction. North Holland (1956)."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Heyting, A.: Axioms for intuitionistic plane affine geometry. Proceedings of an International Symposium on the Axiomatic Method with Special Reference to Geometry and Physics (1959), 160\u2013173.","DOI":"10.1016\/S0049-237X(09)70026-6"},{"key":"17_CR13","unstructured":"Hilbert, D.: Fondations de la G\u00e9om\u00e9trie-Edition critique pr\u00e9par\u00e9e par P. Rossier, CNRS, Dunod (1971)."},{"key":"17_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-55611-7","volume-title":"Axioms and Hulls","author":"D.E. Knuth","year":"1992","unstructured":"Knuth, D.E.: Axioms and Hulls. LNCS 606, Springer-Verlag (1992)."},{"key":"17_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda-Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive Definition in the System Coq-Rules and Properties. Typed Lambda-Calculi and Applications, LNCS 664, Springer-Verlag (1993)."},{"key":"17_CR16","unstructured":"Toussaint, G.: A new look at Euclid\u2019s second proposition. Technical Report No SOCS 90.21 (1990)."},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0168-0072(95)00005-2","volume":"76","author":"J. Plato von","year":"1995","unstructured":"von Plato, J.: The axioms of constructive geometry. Annals of Pure and Applied Logic 76 (1995), 169\u2013200.","journal-title":"Annals of Pure and Applied Logic"},{"key":"17_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/3-540-61780-9_76","volume-title":"Organization and development of a constructive axiomatization","author":"J. Plato von","year":"1996","unstructured":"von Plato, J.: Organization and development of a constructive axiomatization. LNCS 1158, Springer-Verlag (1996), 288\u2013296."},{"issue":"4","key":"17_CR19","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1016\/S0019-3577(98)80034-7","volume":"9","author":"J. Plato von","year":"1998","unstructured":"von Plato, J.: A constructive theory of ordered affine geometry. Indagationes Mathematicae N.S. 9(4) (1998), 549\u2013562.","journal-title":"Indagationes Mathematicae N.S."},{"key":"17_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-48257-1_3","volume-title":"Current Trends in Applied Formal Methods","author":"F. Puitg","year":"1998","unstructured":"Puitg, F., Dufourd J.-F.: Formal program development in geometric modelling. Current Trends in Applied Formal Methods, Boppard, LNCS 1641, Springer-Verlag (1998), 62\u201376."},{"key":"17_CR21","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":"Puitg, F., Dufourd J.-F.: Formal specifications and theorem proving breakthroughs in geometric modelling. Theorem Proving in Higher Order Logics, Canberra, LNCS 1479, Springer-Verlag (1998), 401\u2013427."},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Puitg, F., Dufourd J.-F.: Formalizing mathematics in higher logic: A case study in geometric modelling. Theoretical Computer Science 234 (M. Nivat, ed.), Elsevier Science (2000), 1\u201357.","DOI":"10.1016\/S0304-3975(98)00228-X"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Wu, W.-T.: Mechanical Theorem Proving in Geometries. Springer-Verlag (1994).","DOI":"10.1007\/978-3-7091-6639-0"}],"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_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T14:54:06Z","timestamp":1558277646000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45410-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425984","9783540454106"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45410-1_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"11 September 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}