{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T22:56:05Z","timestamp":1769813765213,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642250699","type":"print"},{"value":"9783642250705","type":"electronic"}],"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_12","type":"book-chapter","created":{"date-parts":[[2011,11,8]],"date-time":"2011-11-08T20:30:55Z","timestamp":1320784255000},"page":"201-220","source":"Crossref","is-referenced-by-count":21,"title":["A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs"],"prefix":"10.1007","author":[{"given":"Sana","family":"Stojanovi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vesna","family":"Pavlovi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Predrag","family":"Jani\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid\u2019s Elements. The Review of Symbolic Logic (2009)","DOI":"10.1017\/S1755020309990098"},{"key":"12_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/11591191_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Bezem","year":"2005","unstructured":"Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 246\u2013260. Springer, Heidelberg (2005)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Bezem, M., Hendriks, D.: On the Mechanization of the Proof of Hessenberg\u2019s Theorem in Coherent Logic. Journal of Automated Reasoning\u00a040(1) (2008)","DOI":"10.1007\/s10817-007-9086-x"},{"key":"12_CR4","volume-title":"Foundations of Geometry","author":"K. Borsuk","year":"1960","unstructured":"Borsuk, K., Szmielew, W.: Foundations of Geometry. Norht-Holland Publishing Company, Amsterdam (1960)"},{"key":"12_CR5","unstructured":"Buchberger, B.: An Algorithm for finding a basis for the residue class ring of a zero-dimensional polynomial ideal. PhD thesis. University of Innsbruck (1965)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Buchberger, B., et al.: Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic (2006)","DOI":"10.1016\/j.jal.2005.10.006"},{"key":"12_CR7","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 (1988)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Chou, S.-C., Gao, X.-S.: Automated reasoning in geometry. In: Handbook of Automated Reasoning. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50013-8"},{"key":"12_CR9","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":"12_CR10","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated production of traditional proofs for constructive geometry theorems. In: IEEE Symposium on Logic in Computer Science LICS. IEEE Computer Society Press (1993)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants, II. theorem proving with full-angles. Journal of Automated Reasoning\u00a017 (1996)","DOI":"10.1007\/BF00283134"},{"key":"12_CR12","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering. Journal Automated Reasoning\u00a025(3) (2000)"},{"key":"12_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/3-540-45410-1_17","volume-title":"Automated Deduction in Geometry","author":"C. Dehlinger","year":"2001","unstructured":"Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in hilbert\u2019s elementary geometry. In: Richter-Gebert, J., Wang, D. (eds.) ADG 2000. LNCS (LNAI), vol.\u00a02061, pp. 306\u2013323. Springer, Heidelberg (2001)"},{"key":"12_CR14","unstructured":"Duprat, J.: Une axiomatique de la g\u00e9om\u00e9trie plane en coq. In: Actes des JFLA 2008, INRIA (2008)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-75292-9_14","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"J. Fisher","year":"2007","unstructured":"Fisher, J., Bezem, M.: Skolem Machines and Geometric Logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol.\u00a04711, pp. 201\u2013215. Springer, Heidelberg (2007)"},{"key":"12_CR16","unstructured":"Gelernter, H., Hanson, J.R., Loveland, D.W.: Empirical explorations of the geometry-theorem proving machine. In: Computers and Thought. MIT Press (1995)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Guilhot, F.: Formalisation en coq d\u2019un cours de g\u00e9om\u00e9trie pour le lyc\u00e9e. Journ\u00e9es Francophones des Langages Applicatifs (2004)","DOI":"10.3166\/tsi.24.1113-1138"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: Hol light: A Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"12_CR19","volume-title":"The Thirteen Books of Euclid\u2019s Elements","author":"T.L. Heath","year":"1956","unstructured":"Heath, T.L.: The Thirteen Books of Euclid\u2019s Elements. Dover Publications, New-York (1956)"},{"key":"12_CR20","unstructured":"Hilbert, D.: Grundlagen der Geometrie, Leipzig (1899)"},{"key":"12_CR21","unstructured":"Jani\u010di\u0107, P., Kordi\u0107, S.: EUCLID \u2014 the geometry theorem prover. FILOMAT\u00a09(3) (1995)"},{"key":"12_CR22","unstructured":"Kahn, G.: Constructive geometry according to Jan von Plato. Coq contribution. Coq V5.10 (1995)"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Using Gr\u00f6bner bases to reason about geometry problems. Journal of Symbolic Computation\u00a02(4) (1986)","DOI":"10.1016\/S0747-7171(86)80007-4"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-21046-4_7","volume-title":"Automated Deduction in Geometry","author":"N. Magaud","year":"2011","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Projective Plane Geometry in Coq. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol.\u00a06301, pp. 141\u2013162. Springer, Heidelberg (2011)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Desargues\u2019 theorem in Coq using ranks. In: ACM Symposium on Applied Computing. ACM (2009)","DOI":"10.1145\/1529282.1529527"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/10930755_21","volume-title":"Theorem Proving in Higher Order Logics","author":"L.I. Meikle","year":"2003","unstructured":"Meikle, L.I., Fleuriot, J.D.: Formalizing Hilbert\u2019s Grundlagen in Isabelle\/Isar. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 319\u2013334. Springer, Heidelberg (2003)"},{"key":"12_CR27","unstructured":"Narboux, J.: Formalisation et automatisation du raisonnement g\u00e9om\u00e9trique en Coq. PhD thesis. Universit\u00e9 Paris Sud (2006)"},{"key":"12_CR28","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-77356-6_9","volume-title":"Automated Deduction in Geometry","author":"J. Narboux","year":"2007","unstructured":"Narboux, J.: Mechanical theorem proving in tarski\u2019s geometry. In: Botana, F., Recio, T. (eds.) ADG 2006. LNCS (LNAI), vol.\u00a04869, pp. 139\u2013156. Springer, Heidelberg (2007)"},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"von Plato, J.: The axioms of constructive geometry. Annals of Pure and Applied Logic\u00a076 (1995)","DOI":"10.1016\/0168-0072(95)00005-2"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"von Plato, J.: Formalization of Hilbert\u2019s geometry of incidence and parallelism. Synthese\u00a0110 (1997)","DOI":"10.1023\/A:1004959405270"},{"key":"12_CR32","unstructured":"Polonsky, A.: Proofs, Types, and Lambda Calculus. PhD thesis. University of Bergen (2011)"},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"Quaife, A.: Automated development of Tarski\u2019s geometry. Journal of Automated Reasoning\u00a05(1) (1989)","DOI":"10.1007\/BF00245024"},{"key":"12_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69418-9","volume-title":"Metamathematische Methoden in der Geometrie","author":"W. Schwabhuser","year":"1983","unstructured":"Schwabhuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983)"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4) (2009)","DOI":"10.1007\/s10817-009-9143-8"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. Journal of ACM 22(2) (1975)","DOI":"10.1145\/321879.321884"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"Tarski, A.: What is elementary geometry? In: The Axiomatic Method, with Special Reference to Geometry and Physics. North-Holland (1959)","DOI":"10.1016\/S0049-237X(09)70017-5"},{"key":"12_CR38","unstructured":"The Coq development team. The Coq proof assistant reference manual, Version 8.2. TypiCal Project (2009)"},{"key":"12_CR39","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11542384_4","volume-title":"The Seventeen Provers of the World","author":"A. Trybulec","year":"2006","unstructured":"Trybulec, A.: Mizar. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600, pp. 20\u201323. Springer, Heidelberg (2006)"},{"key":"12_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M.T. Wenzel","year":"1999","unstructured":"Wenzel, M.T.: Isar - a Generic Interpretative Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013183. Springer, Heidelberg (1999)"},{"key":"12_CR41","unstructured":"Wu, W.-T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica\u00a021 (1978)"}],"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\/978-3-642-25070-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:30:17Z","timestamp":1558297817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25070-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642250699","9783642250705"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25070-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}