{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,3]],"date-time":"2026-02-03T17:34:26Z","timestamp":1770140066872,"version":"3.49.0"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T00:00:00Z","timestamp":1684886400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T00:00:00Z","timestamp":1684886400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005727","name":"Universidade de Coimbra","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005727","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2023,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The Geometry Automated-Theorem-Provers (GATP) based on the deductive database method use a data-based search strategy to improve the efficiency of forward chaining. An implementation of such a method is expected to be able to efficiently prove a large set of geometric conjectures, producing readable proofs. The number of conjectures a given implementation can prove will depend on the set of inference rules chosen, the deductive database method is not a decision procedure. Using an approach based in an <jats:italic>SQL<\/jats:italic> database library and using an in-memory database, the implementation described in this paper tries to achieve the following goals. Efficiency in the management of the inference rules, the set of already known facts and the new facts discovered, by the use of the efficient data manipulation techniques of the <jats:italic>SQL<\/jats:italic> library. Flexibility, by transforming the inference rules in <jats:italic>SQL<\/jats:italic> data manipulation language queries, will open the possibility of meta-development of GATP based on a provided set of rules. Natural language and visual renderings, possible by the use of a synthetic forward chaining method. Implemented as an open source library, that will open its use by third-party programs, e.g. the dynamic geometry systems.<\/jats:p>","DOI":"10.1007\/s10472-023-09839-0","type":"journal-article","created":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T12:02:18Z","timestamp":1684929738000},"page":"851-863","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Towards a geometry deductive database prover"],"prefix":"10.1007","volume":"91","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1629-7924","authenticated-orcid":false,"given":"Nuno","family":"Baeta","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7728-4935","authenticated-orcid":false,"given":"Pedro","family":"Quaresma","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,5,24]]},"reference":[{"key":"9839_CR1","doi-asserted-by":"publisher","first-page":"129","DOI":"10.4204\/EPTCS.352.14","volume":"352","author":"N Baeta","year":"2021","unstructured":"Baeta, N., Quaresma, P.: Open geometry prover community project. Electron. Proc. Theor. Comput. Sci. 352, 129\u2013138 (2021). https:\/\/doi.org\/10.4204\/EPTCS.352.14","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"9839_CR2","doi-asserted-by":"publisher","unstructured":"Baeta, N., Quaresma, P., Kov\u00e1cs, Z.: Towards a geometry automated provers competition. In: Proceedings 8th International Workshop on Theorem proving components for Educational software. Electronic Proceedings in Theoretical Computer Science. https:\/\/doi.org\/10.4204\/EPTCS.313.6, (ThEdu\u201919), Natal, Brazil, 25th August 2019, vol. 313, pp 93\u2013100 (2020)","DOI":"10.4204\/EPTCS.313.6"},{"key":"9839_CR3","doi-asserted-by":"publisher","unstructured":"Chou, S.C., Gao, X.S.: Automated reasoning in geometry. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp 707\u2013749. Elsevier Science Publishers B.V (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50013-8","DOI":"10.1016\/B978-044450813-3\/50013-8"},{"issue":"3","key":"9839_CR4","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"SC 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. 25(3), 219\u2013246 (2000). https:\/\/doi.org\/10.1023\/A:1006171315513","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9839_CR5","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H Coelho","year":"1986","unstructured":"Coelho, H., Pereira, L.M.: Automated reasoning in geometry theorem proving with Prolog. J. Autom. Reason. 2(4), 329\u2013390 (1986). https:\/\/doi.org\/10.1007\/BF00248249","journal-title":"J. Autom. Reason."},{"key":"9839_CR6","unstructured":"Font, L.: G\u00e9n\u00e9ration automatique de preuves pour un logiciel tuteur en g\u00e9om\u00e9trie. phdthesis Polytechnique Montr\u00e9al. https:\/\/publications.polymtl.ca\/9090\/(2021)"},{"key":"9839_CR7","doi-asserted-by":"publisher","unstructured":"Font, L., Richard, P.R., Gagnon, M.: Improving qed-tutrix by automating the generation of proofs. In: Quaresma, P., Neuper, W. (eds.) Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017. Electronic Proceedings in Theoretical Computer Science, vol. 267, pp 38\u201358. Open Publishing Association (2018). https:\/\/doi.org\/10.4204\/EPTCS.267.3","DOI":"10.4204\/EPTCS.267.3"},{"key":"9839_CR8","doi-asserted-by":"publisher","unstructured":"Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of the geometry theorem machine. In: Papers presented at the May 3-5, 1960, Western Joint IRE-AIEE-ACM computer conference. IRE-AIEE-ACM \u201960 (Western), pp 143\u2013149. ACM, New York (1960). https:\/\/doi.org\/10.1145\/1460361.1460381","DOI":"10.1145\/1460361.1460381"},{"key":"9839_CR9","doi-asserted-by":"publisher","unstructured":"Hanna, G., Reid, D., de Villiers, M. (eds.): Proof Technology in Mathematics Research and Teaching. Springer. https:\/\/doi.org\/10.1007\/978-3-030-28483-1 (2019)","DOI":"10.1007\/978-3-030-28483-1"},{"key":"9839_CR10","unstructured":"Hohenwarter, M.: GeoGebra - a software system for dynamic geometry and algebra in the plane. Master\u2019s thesis, University of Salzburg, Austria (2002)"},{"issue":"1","key":"9839_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"A Nevins","year":"1975","unstructured":"Nevins, A.: Plane geometry theorem proving using forward chaining. Artif. Intell. 6(1), 1\u201323 (1975). http:\/\/hdl.handle.net\/1721.1\/6218","journal-title":"Artif. Intell."},{"key":"9839_CR12","doi-asserted-by":"publisher","unstructured":"Quaresma, P.: Evolution of Automated Deduction and Dynamic Constructions in Geometry, Mathematics Education in the Digital Era, chap. 1, vol. 17, pp 3\u201322. Springer, New York (2022). https:\/\/doi.org\/10.1007\/978-3-030-86909-0","DOI":"10.1007\/978-3-030-86909-0"},{"key":"9839_CR13","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-030-28483-1_11","volume-title":"Proof Technology in Mathematics Research and Teaching, chap. Computer-generated geometry proofs in a learning context","author":"P Quaresma","year":"2019","unstructured":"Quaresma, P., Santos, V.: Proof Technology in Mathematics Research and Teaching, chap. Computer-generated geometry proofs in a learning context, pp 237\u2013253. Springer, New York (2019). https:\/\/doi.org\/10.1007\/978-3-030-28483-1_11"},{"key":"9839_CR14","doi-asserted-by":"publisher","unstructured":"Quaresma, P., Santos, V.: Four geometry problems to introduce automated deduction in secondary schools. In: Proceedings 10th International Workshop on Theorem Proving Components for Educational Software. Electronic Proceedings in Theoretical Computer Science, vol. 354, pp 27\u201342. Open Publishing Association (2022). https:\/\/doi.org\/10.4204\/eptcs.354.3","DOI":"10.4204\/eptcs.354.3"},{"issue":"1","key":"9839_CR15","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s10639-017-9597-y","volume":"23","author":"P Quaresma","year":"2018","unstructured":"Quaresma, P., Santos, V., Mari\u0107, M.: WGL, a web laboratory for geometry. Educ. Inf. Technol. 23(1), 237\u2013252 (2018). https:\/\/doi.org\/10.1007\/s10639-017-9597-y","journal-title":"Educ. Inf. Technol."},{"issue":"1","key":"9839_CR16","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1080\/10494820.2016.1258715","volume":"26","author":"V Santos","year":"2018","unstructured":"Santos, V., Quaresma, P., Mari\u0107, M., Campos, H.: Web geometry laboratory: case studies in Portugal and Serbia. Interact. Learn. Environ. 26(1), 3\u201321 (2018). https:\/\/doi.org\/10.1080\/10494820.2016.1258715","journal-title":"Interact. Learn. Environ."},{"key":"9839_CR17","doi-asserted-by":"publisher","unstructured":"Stojanovi\u0107, S., Pavlovi\u0107, V., Jani\u0107i\u0107, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6877, pp 201\u2013220. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-25070-5_12","DOI":"10.1007\/978-3-642-25070-5_12"},{"issue":"4","key":"9839_CR18","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","journal-title":"J. Autom. Reason."},{"key":"9839_CR19","doi-asserted-by":"crossref","unstructured":"Teles, J., Santos, V., Quaresma, P.: A rule based theorem prover: an introduction to proofs in secondary schools. Electronic Proceedings in Theoretical Computer Science, accepted for publication (2023)","DOI":"10.4204\/EPTCS.375.3"},{"key":"9839_CR20","doi-asserted-by":"publisher","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: An introduction to Java geometry expert. In: Sturm, T., Zengler, C. (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6301, pp 189\u2013195. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-21046-4_10","DOI":"10.1007\/978-3-642-21046-4_10"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-023-09839-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-023-09839-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-023-09839-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,15]],"date-time":"2023-11-15T11:08:05Z","timestamp":1700046485000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-023-09839-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,24]]},"references-count":20,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["9839"],"URL":"https:\/\/doi.org\/10.1007\/s10472-023-09839-0","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,24]]},"assertion":[{"value":"8 February 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 May 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"All authors declare that they have no conflicts of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interests"}}]}}