{"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":1771063360966,"version":"3.50.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,10,28]],"date-time":"2016-10-28T00:00:00Z","timestamp":1477612800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1007\/s10817-016-9392-2","type":"journal-article","created":{"date-parts":[[2016,10,28]],"date-time":"2016-10-28T15:12:17Z","timestamp":1477667537000},"page":"181-207","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Finding Proofs in Tarskian Geometry"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9259-1220","authenticated-orcid":false,"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]},{"given":"Larry","family":"Wos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,28]]},"reference":[{"key":"9392_CR1","unstructured":"Beeson, M.: The Tarski formalization project. http:\/\/www.michaelbeeson.com\/research\/FormalTarski\/index.php"},{"key":"9392_CR2","doi-asserted-by":"crossref","unstructured":"Beeson, M., Wos, L.: OTTER proofs in Tarskian geometry. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proceedings of 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Vienna, Austria, July 19\u201322, 2014. Lecture Notes in Computer Science, vol. 8562, pp. 495\u2013510. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_38"},{"key":"9392_CR3","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016)"},{"key":"9392_CR4","doi-asserted-by":"crossref","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot J. (eds.) Automated Deduction in Geometry 2012, vol. 7993, pp. 89\u2013109. Springer-Verlag (2013)","DOI":"10.1007\/978-3-642-40672-0_7"},{"key":"9392_CR5","doi-asserted-by":"publisher","unstructured":"Braun, G., Narboux, J.: A synthetic proof of Pappus\u2019s theorem in Tarski\u2019s geometry. J. Autom. Reason. (2016). doi: 10.1007\/s10817-016-9374-4","DOI":"10.1007\/s10817-016-9374-4"},{"key":"9392_CR6","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","year":"1998","unstructured":"Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Wien (1998)"},{"key":"9392_CR7","doi-asserted-by":"publisher","unstructured":"Durdevic, S.S., Narboux, J., Janicic, P.: Automated generation of machine verifiable and readable proofs: a case study of Tarski\u2019s geometry. Ann. Math. Artif. Intell. 25 (2015). doi: 10.1007\/s10472-014-9443-5 . https:\/\/hal.inria.fr\/hal-01091011","DOI":"10.1007\/s10472-014-9443-5"},{"key":"9392_CR8","unstructured":"Gupta, H.N.: Contributions to the axiomatic foundations of geometry. Ph.D. thesis, University of California, Berkeley (1965)"},{"key":"9392_CR9","unstructured":"Hilbert, D.: Foundations of Geometry (Grundlagen der Geometrie): Open Court, La Salle, Illinois (1960). Second English edition, translated from the tenth German edition by Leo Unger. Original publication date (1899)"},{"issue":"2","key":"9392_CR10","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014). doi: 10.1007\/s10817-014-9303-3","journal-title":"J. Autom. Reason."},{"key":"9392_CR11","volume-title":"Vorlesung \u00fcber Neuere Geometrie","author":"M Pasch","year":"1882","unstructured":"Pasch, M.: Vorlesung \u00fcber Neuere Geometrie. Teubner, Leipzig (1882)"},{"key":"9392_CR12","unstructured":"Pasch, M., Dehn, M.: Vorlesung \u00fcber Neuere Geometrie. In: Teubner, B.G. (ed.) Leipzig (1926). The first edition (1882), which is the one digitized by Google Scholar, does not contain the appendix by Dehn"},{"key":"9392_CR13","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL 2010. The 8th International Workshop on the Implementation of Logics, EasyChair Proceedings in Computing, vol.\u00a02, pp. 1\u201311. EasyChair (2012)","DOI":"10.29007\/36dt"},{"key":"9392_CR14","volume-title":"Automated Development of Fundamental Mathematical Theories","author":"A Quaife","year":"1992","unstructured":"Quaife, A.: Automated Development of Fundamental Mathematical Theories. Springer, Berlin (1992)"},{"key":"9392_CR15","doi-asserted-by":"crossref","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie: Teil I: Ein axiomatischer Aufbau der euklidischen Geometrie, Teil II: Metamathematische Betrachtungen (Hochschultext). Springer (1983). Reprinted 2012 by Ishi Press, with a new foreword by Michael Beeson","DOI":"10.1007\/978-3-642-69418-9"},{"key":"9392_CR16","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Technical Report R-109, second revised edition, reprinted in [6], pp. 24\u201384, Rand Corporation (1951)","DOI":"10.1525\/9780520348097"},{"key":"9392_CR17","doi-asserted-by":"crossref","unstructured":"Tarski, A.: What is elementary geometry? In: Henkin, L., Suppes, P., Tarksi, A. (eds.) The axiomatic method, with special reference to geometry and physics. Proceedings of an International Symposium held at the University of California, Berkeley, Dec. 26, 1957\u2013Jan. 4, 1958, Studies in Logic and the Foundations of Mathematics, pp. 16\u201329. North-Holland, Amsterdam (1959). Available as a 2007 reprint, Brouwer Press, ISBN 1-443-72812-8","DOI":"10.1016\/S0049-237X(09)70017-5"},{"issue":"2","key":"9392_CR18","doi-asserted-by":"crossref","first-page":"175","DOI":"10.2307\/421089","volume":"5","author":"A Tarski","year":"1999","unstructured":"Tarski, A., Givant, S.: Tarski\u2019s system of geometry. Bull. Symb. Log. 5(2), 175\u2013214 (1999)","journal-title":"Bull. Symb. Log."},{"key":"9392_CR19","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1090\/S0002-9947-1904-1500678-X","volume":"5","author":"O Veblen","year":"1904","unstructured":"Veblen, O.: A system of axioms for geometry. Trans. Am. Math. Soc. 5, 343\u2013384 (1904)","journal-title":"Trans. Am. Math. Soc."},{"issue":"3","key":"9392_CR20","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program. J. Autom. Reason. 16(3), 223\u2013239 (1996)","journal-title":"J. Autom. Reason."},{"key":"9392_CR21","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L Wos","year":"1988","unstructured":"Wos, L.: Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs (1988)"},{"key":"9392_CR22","volume-title":"Automated Reasoning and the Discovery of Missing and Elegant Proofs","author":"L Wos","year":"2003","unstructured":"Wos, L.: Automated Reasoning and the Discovery of Missing and Elegant Proofs. Rinton Press, Paramus (2003)"},{"key":"9392_CR23","unstructured":"Wos, L.: The subformula strategy: coping with complex expressions (2008). http:\/\/www.automatedreasoning.net\/docs_and_pdfs\/subformula"},{"key":"9392_CR24","unstructured":"Wos, L.: An amazing approach to plane geometry (2014). http:\/\/www.automatedreasoning.net\/docs_and_pdfs\/an_amazing_approach"},{"key":"9392_CR25","doi-asserted-by":"crossref","DOI":"10.1142\/4132","volume-title":"A Fascinating Country in the World of Computing","author":"L Wos","year":"1999","unstructured":"Wos, L., Pieper, G.W.: A Fascinating Country in the World of Computing. World Scientific, Singapore (1999)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9392-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9392-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9392-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T22:21:34Z","timestamp":1749680494000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9392-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,28]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,1]]}},"alternative-id":["9392"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9392-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10,28]]}}}