{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,3]],"date-time":"2026-02-03T15:16:03Z","timestamp":1770131763143,"version":"3.49.0"},"reference-count":67,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,11,16]],"date-time":"2010-11-16T00:00:00Z","timestamp":1289865600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10817-010-9209-7","type":"journal-article","created":{"date-parts":[[2010,11,15]],"date-time":"2010-11-15T06:57:41Z","timestamp":1289804261000},"page":"489-532","source":"Crossref","is-referenced-by-count":46,"title":["The Area Method"],"prefix":"10.1007","volume":"48","author":[{"given":"Predrag","family":"Jani\u010di\u0107","sequence":"first","affiliation":[]},{"given":"Julien","family":"Narboux","sequence":"additional","affiliation":[]},{"given":"Pedro","family":"Quaresma","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,11,16]]},"reference":[{"key":"9209_CR1","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9209_CR2","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B Buchberger","year":"2006","unstructured":"Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: towards computer-aided mathematical theory exploration. Journal of Applied Logic 4, 470\u2013504 (2006)","journal-title":"Journal of Applied Logic"},{"key":"9209_CR3","doi-asserted-by":"crossref","unstructured":"Chou, S., Gao, X., Zhang, J.: An introduction to geometry expert. In: McRobbie, M.A., Slaney, J.K. (eds.) Proc. CADE-13. Lecture Notes in Computer Science, vol. 1104, pp. 235\u2013239. Springer (1996)","DOI":"10.1007\/3-540-61511-3_86"},{"key":"9209_CR4","unstructured":"Chou, S.C.: Proving and Discovering Geometry Theorems using Wu\u2019s Method. Ph.D. thesis, The University of Texas, Austin (1985)"},{"key":"9209_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-009-4037-6","volume-title":"Mechanical Geometry Theorem Proving","author":"SC Chou","year":"1987","unstructured":"Chou, S.C.: Mechanical Geometry Theorem Proving. Reidel, Dordrecht (1987)"},{"key":"9209_CR6","volume-title":"Mechanical Geometry Theorem Proving","author":"SC Chou","year":"1988","unstructured":"Chou, S.C.: Mechanical Geometry Theorem Proving. Reidel, Dordrecht (1988)"},{"key":"9209_CR7","doi-asserted-by":"crossref","first-page":"707","DOI":"10.1016\/B978-044450813-3\/50013-8","volume-title":"Handbook of Automated Reasoning","author":"SC Chou","year":"2001","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 and MIT Press (2001)"},{"key":"9209_CR8","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated production of traditional proofs for constructive geometry theorems. In: Vardi, M. (ed.) Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science LICS, pp. 48\u201356. IEEE Computer Society Press (1993)","DOI":"10.1109\/LICS.1993.287601"},{"key":"9209_CR9","doi-asserted-by":"crossref","DOI":"10.1142\/9789812798152","volume-title":"Machine Proofs in Geometry","author":"SC Chou","year":"1994","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)"},{"key":"9209_CR10","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/BF00881858","volume":"14","author":"SC Chou","year":"1995","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated production of traditional proofs in solid geometry. J. Autom. Reason. 14, 257\u2013291 (1995)","journal-title":"J. Autom. Reason."},{"key":"9209_CR11","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00283133","volume":"17","author":"SC Chou","year":"1996","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation. J. Autom. Reason. 17, 325\u2013347 (1996)","journal-title":"Multiple and shortest proof generation. J. Autom. Reason."},{"key":"9209_CR12","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF00283134","volume":"17","author":"SC Chou","year":"1996","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants, II. theorem proving with full-angles. J. Autom. Reason. 17, 349\u2013370 (1996)","journal-title":"J. Autom. Reason."},{"key":"9209_CR13","doi-asserted-by":"crossref","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, 219\u2013246 (2000)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9209_CR14","doi-asserted-by":"crossref","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)","journal-title":"J. Autom. Reason."},{"key":"9209_CR15","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, 20\u201323 May 1975. Lecture Notes In Computer Science, vol.\u00a033, pp. 134\u2013183. Springer (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"9209_CR16","doi-asserted-by":"crossref","unstructured":"Dehlinger, C., Dufourd, J.F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert\u2019s elementary geometry. In: Richter-Gebert, D.W.J. (ed.) Proceedings of Automated Deduction in Geometry (ADG00). Lecture Notes in Computer Science, vol. 2061, pp. 306\u2013324 (2000)","DOI":"10.1007\/3-540-45410-1_17"},{"key":"9209_CR17","unstructured":"Duprat, J.: The Euclid\u2019s plane: formalization and implementation in Coq. In: Proceedings of ADG\u201910 (2010)"},{"key":"9209_CR18","first-page":"11","volume":"8","author":"EW Elcock","year":"1977","unstructured":"Elcock, E.W.: Representation of knowledge in geometry machine. Mach. Intell. 8, 11\u201329 (1977)","journal-title":"Mach. Intell."},{"key":"9209_CR19","doi-asserted-by":"crossref","unstructured":"Gao, X.S., Lin, Q.: MMP\/Geometer\u2014a software package for automated geometric reasoning. In: Winkler, F. (ed.) Proceedings of Automated Deduction in Geometry (ADG02). Lecture Notes in Computer Science, vol. 2930, pp. 44\u201366. Springer (2004)","DOI":"10.1007\/978-3-540-24616-9_4"},{"key":"9209_CR20","first-page":"134","volume-title":"Computers & Thought","author":"H Gelernter","year":"1995","unstructured":"Gelernter, H.: Realization of a geometry-theorem proving machine. In: Computers & Thought, pp. 134\u2013152. MIT Press, Cambridge (1995)"},{"key":"9209_CR21","unstructured":"Geuvers, H., et al.: The \u201cFundamental Theorem of Algebra\u201d project. http:\/\/www.cs.ru.nl\/~freek\/fta\/ (2008)"},{"key":"9209_CR22","unstructured":"Gonthier, G., Werner, B.: A Computer Checked Proof of the Four Colour Theorem (2004)"},{"issue":"6","key":"9209_CR23","doi-asserted-by":"crossref","first-page":"445","DOI":"10.3758\/BF03198261","volume":"7","author":"J Greeno","year":"1979","unstructured":"Greeno, J., Magone, M.E., Chaiklin, S.: Theory of constructions and set in problem solving. Mem. Cogn. 7(6), 445\u2013461 (1979)","journal-title":"Mem. Cogn."},{"key":"9209_CR24","doi-asserted-by":"crossref","unstructured":"Guilhot, F.: Formalisation en Coq d\u2019un cours de g\u00e9om\u00e9trie pour le lyc\u00e9e. In: Journ\u00e9es Francophones des Langages Applicatifs (2004)","DOI":"10.3166\/tsi.24.1113-1138"},{"key":"9209_CR25","volume-title":"Mathematics, Algorithms, Proofs, Dagstuhl Seminar Proceedings, vol. 05021","author":"TC Hales","year":"2006","unstructured":"Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.F. (eds.) Mathematics, Algorithms, Proofs, Dagstuhl Seminar Proceedings, vol. 05021. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany (2006)"},{"key":"9209_CR26","volume-title":"The Thirteen Books of Euclid\u2019s Elements","author":"TL Heath","year":"1956","unstructured":"Heath, T.L.: The Thirteen Books of Euclid\u2019s Elements, 2nd edn. Dover, New York (1956)","edition":"2"},{"key":"9209_CR27","unstructured":"Hilbert, D.: In: Barnays, P. (ed.) Foundations of Geometry, 10th rev. edn. Open Court, La Salle (1977)"},{"key":"9209_CR28","unstructured":"Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq Proof Assistant\u2014A Tutorial, version 8.0 (2004). http:\/\/coq.inria.fr"},{"key":"9209_CR29","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P.: GCLC\u2014a tool for constructive Euclidean geometry and more than that. In: Takayama, N., Iglesias, A., Gutierrez, J. (eds.) Proceedings of International Congress of Mathematical Software (ICMS 2006). Lecture Notes in Artificial Intelligence, vol. 4151. Springer (2006)","DOI":"10.1007\/11832225_6"},{"key":"9209_CR30","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P., Quaresma, P.: Automatic verification of regular constructions in dynamic geometry systems. In: Botana, F., Recio, T. (eds.) Proceedings of Automated Deduction in Geometry (ADG06). Lecture Notes in Artificial Intelligence, vol. 4869, pp. 39\u201351. Springer, Pontevedra (2007)","DOI":"10.1007\/978-3-540-77356-6_3"},{"key":"9209_CR31","unstructured":"Jani\u010di\u0107, P.: One Method for Automathed Theorem Proving in Geometry. Master\u2019s thesis, Faculty of Mathematics, University of Belgrade. In Serbian (1996)"},{"issue":"1\u20132","key":"9209_CR32","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10817-009-9135-8","volume":"44","author":"P Jani\u010di\u0107","year":"2010","unstructured":"Jani\u010di\u0107, P.: Geometry constructions language. J. Autom. Reason. 44(1\u20132), 3\u201324 (2010)","journal-title":"J. Autom. Reason."},{"key":"9209_CR33","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P., Quaresma, P.: System description: GCLCprover + GeoThms. In: Ulrich, F., Natarajan, S. (eds.) Automated Reasoning. Lecture Notes in Artificial Intelligence, vol. 4130, pp. 145\u2013150. Springer (2006)","DOI":"10.1007\/11814771_13"},{"key":"9209_CR34","unstructured":"Kahn, G.: Constructive Geometry According to Jan von Plato. Coq Contribution (1995). Coq V5.10"},{"key":"9209_CR35","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1145\/32439.32479","volume-title":"SYMSAC \u201986: Proceedings of the Fifth ACM Symposium on Symbolic and Algebraic Computation","author":"D Kapur","year":"1986","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert\u2019s nullstellensatz. In: SYMSAC \u201986: Proceedings of the Fifth ACM Symposium on Symbolic and Algebraic Computation, pp. 202\u2013208. ACM Press, New York (1986)"},{"issue":"4","key":"9209_CR36","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1016\/S0747-7171(86)80007-4","volume":"2","author":"D Kapur","year":"1986","unstructured":"Kapur, D.: Using Gr\u00f6bner bases to reason about geometry problems. J. Symb. Comput. 2(4), 399\u2013408 (1986)","journal-title":"J. Symb. Comput."},{"key":"9209_CR37","unstructured":"Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Workshop on Mathematical User Interfaces (2004)"},{"key":"9209_CR38","first-page":"42","volume-title":"33rd Symposium Principles of Programming Languages","author":"X Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"9209_CR39","first-page":"205","volume-title":"Mathematics Mechanization and Applications","author":"H Li","year":"2000","unstructured":"Li, H.: Clifford algebra approaches to mechanical geometry theorem proving. In: Gao, X.S., Wang, D. (eds.) Mathematics Mechanization and Applications, pp. 205\u2013299. Academic, San Diego (2000)"},{"key":"9209_CR40","doi-asserted-by":"crossref","first-page":"1110","DOI":"10.1145\/1529282.1529527","volume-title":"SAC","author":"N Magaud","year":"2009","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Desargues\u2019 theorem in Coq using ranks. In: Shin, S.Y., Ossowski, S. (eds.) SAC, pp. 1110\u20131115. ACM Press, New York (2009)"},{"key":"9209_CR41","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing projective plane geometry in Coq. In: Sturm, T. (ed.) Proceedings of Automated Deduction in Geometry (ADG08). Lecture Notes inArtifical Intelligence, vol. 6301. Springer"},{"key":"9209_CR42","doi-asserted-by":"crossref","unstructured":"Meikle, L., Fleuriot, J.: Formalizing Hilbert\u2019s Grundlagen in Isabelle\/Isar. In: Basin, D.A., Wolff, B. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 2758, pp. 319\u2013334. Springer (2003)","DOI":"10.1007\/10930755_21"},{"key":"9209_CR43","doi-asserted-by":"crossref","unstructured":"Narboux, J.: A decision procedure for geometry in Coq. In: Konrad, S., Annett, B., Ganesh, G. (eds.) Proceedings of TPHOLs\u20192004. Lecture Notes in Computer Science, vol. 3223. Springer (2004)","DOI":"10.1007\/978-3-540-30142-4_17"},{"key":"9209_CR44","unstructured":"Narboux, J.: Formalisation et Automatisation du Raisonnement G\u00e9om\u00e9trique en Coq. Ph.D. thesis, Universit\u00e9 Paris Sud (2006)"},{"issue":"2","key":"9209_CR45","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10817-007-9071-4","volume":"39","author":"J Narboux","year":"2007","unstructured":"Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reason. 39(2), 161\u2013180 (2007)","journal-title":"J. Autom. Reason."},{"key":"9209_CR46","doi-asserted-by":"crossref","unstructured":"Narboux, J.: Mechanical theorem proving in Tarski\u2019s geometry. In: Proceedings of Automatic Deduction in Geometry 06. Lecture Notes in Artificial Intelligence, vol. 4869, pp. 139\u2013156. Springer (2007)","DOI":"10.1007\/978-3-540-77356-6_9"},{"key":"9209_CR47","unstructured":"Narboux, J.: Formalization of the Area Method. Coq User Contribution (2009). http:\/\/dpt-info.u-strasbg.fr\/~narboux\/area_method.html"},{"issue":"1","key":"9209_CR48","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"A Nevis","year":"1975","unstructured":"Nevis, A.: Plane geometry theorem proving using forward chaining. Artif. Intell. 6(1), 1\u201323 (1975)","journal-title":"Artif. Intell."},{"key":"9209_CR49","unstructured":"Predovi\u0107, G.: Automated Geometry Theorem Proving Based on Wu\u2019s and Buchberger\u2019s Methods. Master\u2019s thesis, Faculty of Mathematics, University of Belgrade. Supervisor: Predrag Jani\u010di\u0107. In Serbian (2008)"},{"key":"9209_CR50","unstructured":"Quaresma, P., Jani\u010di\u0107, P.: Framework for Constructive Geometry (Based on the Area Method). Tech. Rep. 2006\/001, Centre for Informatics and Systems of the University of Coimbra (2006)"},{"key":"9209_CR51","doi-asserted-by":"crossref","unstructured":"Quaresma, P., Jani\u010di\u0107, P.: Geothms\u2014a web system for Euclidean constructive geometry. In: Autexier, S., Benzm\u00fcller, C. (eds.) UITP 2006, vol. 174, pp. 21\u201333 (2006)","DOI":"10.1016\/j.entcs.2006.09.020"},{"key":"9209_CR52","unstructured":"Quaresma, P., Jani\u010di\u0107, P.: Geothms\u2014Geometry Framework. Tech. Rep. 2006\/002, Centre for Informatics and Systems of the University of Coimbra (2006)"},{"key":"9209_CR53","doi-asserted-by":"crossref","unstructured":"Quaresma, P., Jani\u010di\u0107, P.: Integrating dynamic geometry software, deduction systems, and theorem repositories. In: Borwein, J.M., Farmer, W.M. (eds.) Mathematical Knowledge Management. Lecture Notes in Artificial Intelligence, vol. 4108, pp. 280\u2013294. Springer (2006)","DOI":"10.1007\/11812289_22"},{"key":"9209_CR54","unstructured":"Quaresma, P., Jani\u010di\u0107, P.: The Area Method\u2014Properties and Their Proofs. Tech. Rep. 2009\/006, Centre for Informatics and Systems of the University of Coimbra (2009)"},{"key":"9209_CR55","unstructured":"Quaresma, P., Pereira, A.: Visualiza\u00e7\u00e3o de constru\u00e7\u00f5es geom\u00e9tricas. Gaz. Mat. 151 (2006)"},{"key":"9209_CR56","unstructured":"Robu, J.: Geometry Theorem Proving in the Frame of the Theorema Project. Ph.D. thesis, Johannes Kepler Universit\u00e4t, Linz (2002)"},{"key":"9209_CR57","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)","DOI":"10.1525\/9780520348097"},{"key":"9209_CR58","first-page":"16","volume-title":"The Axiomatic Method, with Special Reference to Geometry and Physics","author":"A Tarski","year":"1959","unstructured":"Tarski, A.: What is elementary geometry? In: Henkin, P.S.L., Tarski, A. (eds.) The Axiomatic Method, with Special Reference to Geometry and Physics, pp. 16\u201329. North-Holland, Amsterdam (1959)"},{"key":"9209_CR59","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual, version 8.2. TypiCal Project (2009). http:\/\/coq.inria.fr"},{"key":"9209_CR60","doi-asserted-by":"crossref","unstructured":"von Plato, J.: The axioms of constructive geometry. In: Annals of Pure and Applied Logic, vol.\u00a076, pp. 169\u2013200 (1995)","DOI":"10.1016\/0168-0072(95)00005-2"},{"key":"9209_CR61","doi-asserted-by":"crossref","unstructured":"von Plato, J.: Formalization of Hilbert\u2019s geometry of incidence and parallelism. In: Synthese, vol. 110, pp. 127\u2013141. Springer (1997)","DOI":"10.1023\/A:1004959405270"},{"key":"9209_CR62","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-7091-6604-8_8","volume-title":"Automated Practical Reasoning","author":"D Wang","year":"1995","unstructured":"Wang, D.: Reasoning about geometric problems using an elimination method. In: Pfalzgraf, J., Wang, D. (eds.) Automated Practical Reasoning, pp. 147\u2013185. Springer, New York (1995)"},{"key":"9209_CR63","doi-asserted-by":"crossref","unstructured":"Wu, W.T.: On the decision problem and the mechanization of theorem proving in elementary geometry. In: Automated Theorem Proving: After 25 Years, vol.\u00a029, pp. 213\u2013234. American Mathematical Society (1984)","DOI":"10.1090\/conm\/029\/12"},{"key":"9209_CR64","series-title":"Lecture Notes in Artificial Intelligence","first-page":"171","volume-title":"Proceedings of Automated Deduction in Geometry (ADG98)","author":"L Yang","year":"1998","unstructured":"Yang, L., Gao, X., Chou, S., Zhang, Z.: Automated proving and discovering of theorems in non-euclidean geometries. In: Proceedings of Automated Deduction in Geometry (ADG98). Lecture Notes in Artificial Intelligence, vol. 1360, pp. 171\u2013188. Springer, Berlin (1998)"},{"issue":"3","key":"9209_CR65","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10817-009-9162-5","volume":"45","author":"Z Ye","year":"2010","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane geometry. Part 1. Basic features and the manual input method. J. Autom. Reason. 45(3), 213\u2013241 (2010)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9209_CR66","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/s10817-009-9163-4","volume":"45","author":"Z Ye","year":"2010","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane geometry. Part 2. Automated generation of visually dynamic presentations with the full-angle method and the deductive database method. J. Autom. Reason. 45(3), 243\u2013266 (2010)","journal-title":"J. Autom. Reason."},{"key":"9209_CR67","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BF01531326","volume":"13","author":"JZ Zhang","year":"1995","unstructured":"Zhang, J.Z., Chou, S.C., Gao, X.S.: Automated production of traditional proofs for theorems in Euclidean geometry. Ann. Math. Artif. Intell. 13, 109\u2013137 (1995)","journal-title":"Ann. Math. Artif. Intell."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9209-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9209-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9209-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T21:06:53Z","timestamp":1740690413000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9209-7"}},"subtitle":["A Recapitulation"],"short-title":[],"issued":{"date-parts":[[2010,11,16]]},"references-count":67,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["9209"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9209-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,11,16]]}}}