{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:01:43Z","timestamp":1760061703523},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642406713"},{"type":"electronic","value":"9783642406720"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40672-0_1","type":"book-chapter","created":{"date-parts":[[2013,9,2]],"date-time":"2013-09-02T07:49:04Z","timestamp":1378108144000},"page":"1-30","source":"Crossref","is-referenced-by-count":6,"title":["Proof and Computation in Geometry"],"prefix":"10.1007","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"700","DOI":"10.1017\/S1755020309990098","volume":"2","author":"J. Avigad","year":"2009","unstructured":"Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid\u2019s Elements. Review of Symbolic Logic\u00a02, 700\u2013768 (2009)","journal-title":"Review of Symbolic Logic"},{"key":"1_CR2","unstructured":"Beeson, M.: \n                  \n                    http:\/\/www.michaelbeeson.com\/research\/FormalTarski\/index.php"},{"key":"1_CR3","unstructured":"Beeson, M.: Foundations of Constructive Geometry (2012), Available on the author\u2019s website, \n                  \n                    www.michaelbeeson.com\/research\/papers\/pubs.html"},{"key":"1_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-30870-3_6","volume-title":"How the World Computes","author":"M. Beeson","year":"2012","unstructured":"Beeson, M.: Logic of ruler and compass constructions. In: Cooper, S.B., Dawar, A., L\u00f6we, B. (eds.) CiE 2012. LNCS, vol.\u00a07318, pp. 46\u201355. Springer, Heidelberg (2012)"},{"key":"1_CR5","unstructured":"Borsuk, K., Szmielew, W.: Foundations of Geometry: Euclidean and Bolyai-Lobachevskian Geometry, Projective Geometry. North-Holland, Amsterdam (1960); translated from Polish by Marquit, E."},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"C.W. Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B, a program for computing with semi-algebraic sets using cads. SIGSAM Bulletin\u00a037, 97\u2013108 (2003)","journal-title":"SIGSAM Bulletin"},{"volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","year":"1998","key":"1_CR7","unstructured":"Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Wien (1998)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. World Scientific (1994)","DOI":"10.1142\/9789812798152"},{"key":"1_CR9","unstructured":"Feferman, S. (ed.): The Collected Works of Julia Robinson. American Mathematical Society (1996)"},{"key":"1_CR10","unstructured":"Fischer, M.J., Rabin, M.O.: Super\u2013exponential complexity of Presburger arithmetic. SIAM-AMS Proceedings\u00a0VII, 27\u201341 (1974); reprinted in [7], pp. 27\u201341"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"198","DOI":"10.4169\/000298910X480063","volume":"117","author":"M.J. Greenberg","year":"2010","unstructured":"Greenberg, M.J.: Old and new results in the foundations of elementary plane euclidean and non-euclidean geometries. American Mathematical Monthly\u00a0117, 198\u2013219 (2010)","journal-title":"American Mathematical Monthly"},{"key":"1_CR12","unstructured":"Gupta, H.N.: Contributions to the Axiomatic Foundations of Geometry. Ph.D. thesis, University of California, Berkeley (1965)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Hartshorne, R.: Geometry: Euclid and Beyond. Springer (2000)","DOI":"10.1007\/978-0-387-22676-7"},{"key":"1_CR14","unstructured":"Hilbert, D.: Foundations of Geometry (Grundlagen der Geometrie). Open Court, La Salle, Illinois (1960), 2nd English edition, translated from the tenth German edition by Unger, L. Original publication date (1899)"},{"key":"1_CR15","unstructured":"Hilbert, D.: David Hilbert\u2019s lectures on the foundations of geometry 1891-1902. Springer, Heidelberg (2004),edited by Hallett, M and Majer, U."},{"key":"1_CR16","first-page":"147","volume":"21","author":"A.B. Kempe","year":"1890","unstructured":"Kempe, A.B.: On the relation between the logical theory of classes and the geometrical theory of points. Proceedings of the London Mathematical Society\u00a021, 147\u2013182 (1890)","journal-title":"Proceedings of the London Mathematical Society"},{"key":"1_CR17","volume-title":"The Legacy of Mario Pieri in Geometry and Arithmetic","author":"E.A. Marchisotto","year":"2007","unstructured":"Marchisotto, E.A., Smith, J.T.: The Legacy of Mario Pieri in Geometry and Arithmetic. Birkhauser, Boston (2007)"},{"issue":"8","key":"1_CR18","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., Wos, L.: Problems and experiments for and with automated theorem-proving programs. IEEE Transactions on Computers\u00a0C-25(8), 773\u2013782 (1976)","journal-title":"IEEE Transactions on Computers"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/BF01449485","volume":"58","author":"J. Mollerup","year":"1904","unstructured":"Mollerup, J.: Die Beweise der ebenen Geometrie ohne Benutzung der Gleichheit und Unbleichheit der Winkel. Mathematische Annalen\u00a058, 479\u2013496 (1904)","journal-title":"Mathematische Annalen"},{"key":"1_CR20","series-title":"LNAI","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":"1_CR21","unstructured":"Pasch, M.: Vorlesung \u00fcber Neuere Geometrie. Teubner, Leipzig (1882)"},{"key":"1_CR22","unstructured":"Pasch, M., Dehn, M.: Vorlesung \u00fcber Neuere Geometrie. B.\u00a0G. Teubner, Leipzig (1926), the 1st edition (1882), which is the one digitized by Scholar, G. does not contain the appendix by Dehn"},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/BF01342979","volume":"143","author":"W. Pejas","year":"1961","unstructured":"Pejas, W.: Die Modelle des Hilbertschen Axiomensystems der absoluten Geometrie. Mathematische Annalen\u00a0143, 212\u2013235 (1961)","journal-title":"Mathematische Annalen"},{"key":"1_CR24","unstructured":"Pieri, M.: La geometry elementare istituita sulle nozioni di \u201cpunto\u201d e \u201csfera\u201d (elementary geometry based on the notions of point and sphere). Memorie di Matematica e di Fisica della Societ\u00e0 Italiana delle Scienze 15, 345\u2013450 (1908), english translation in [7], pp. 160\u2013288"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF00245024","volume":"5","author":"A. Quaife","year":"1989","unstructured":"Quaife, A.: Automated development of Tarski\u2019s geometry. Journal of Automated Reasoning\u00a05, 97\u2013118 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR26","volume-title":"Automated Development of Fundamental Mathematical Theories","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: Automated Development of Fundamental Mathematical Theories. Springer, Heidelberg (1992)"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Renegar, J.: Recent progress on the complexity of the decision problem for the reals. DIMACS Series 6, 287\u2013308 (1991); reprinted in [7], pp. 220\u2013241","DOI":"10.1090\/dimacs\/006\/20"},{"key":"1_CR28","doi-asserted-by":"crossref","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J. Robinson","year":"1949","unstructured":"Robinson, J.: Definability and decision problems in arithmetic. Journal of Symbolic Logic 14, 98\u2013114 (1949); reprinted in [9], pp.7\u201324","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR29","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 Beeson, M."},{"key":"1_CR30","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF02018030","volume":"4","author":"J. Strommer","year":"1973","unstructured":"Strommer, J.: \u00dcber die Kreisaxiome. Periodica Mathematica Hungarica\u00a04, 3\u201316 (1973)","journal-title":"Periodica Mathematica Hungarica"},{"key":"1_CR31","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 Univ. of Calif., Berkeley, December 26, 1957\u2013January 4, 1958. pp. 16\u201329. Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam (1959), available as a 2007 reprint, Brouwer Press, ISBN 1-443-72812-8"},{"issue":"2","key":"1_CR32","doi-asserted-by":"publisher","first-page":"175","DOI":"10.2307\/421089","volume":"5","author":"A. Tarski","year":"1999","unstructured":"Tarski, A., Givant, S.: Tarski\u2019s system of geometry. The Bulletin of Symbolic Logic\u00a05(2), 175\u2013214 (1999)","journal-title":"The Bulletin of Symbolic Logic"},{"key":"1_CR33","doi-asserted-by":"publisher","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. Transactions of the American Mathematical Society\u00a05, 343\u2013384 (1904)","journal-title":"Transactions of the American Mathematical Society"},{"key":"1_CR34","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":"1_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6639-0","volume-title":"Mechanical Theorem Proving in Geometries: Basic Principles","author":"W.T. Wu","year":"1994","unstructured":"Wu, W.T.: Mechanical Theorem Proving in Geometries: Basic Principles. Springer, Wien (1994)"},{"issue":"28","key":"1_CR36","first-page":"269","volume":"2","author":"M. Ziegler","year":"1982","unstructured":"Ziegler, M.: Einige unentscheidbare k\u00f6rpertheorien. Enseignement Math.\u00a02(28), 269\u2013280 (1982)","journal-title":"Enseignement Math."}],"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-40672-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T21:08:40Z","timestamp":1558040920000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40672-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642406713","9783642406720"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40672-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}