×

zbMATH — the first resource for mathematics

A review and prospect of readable machine proofs for geometry theorems. (English) Zbl 1291.68351
Summary: After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T05 Learning and adaptive systems in artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] D. Hilbert, Foundations of Geometry, Open Court Publishing Company, La Salla, Illinois, 1971. · Zbl 0228.50002
[2] W. T. Wu, Mathematics Mechanization, Science Press, Beijing, 2003.
[3] A. Tarski, A Decision Method for Elementary Algebra and Geometry, The RAND Corporation Press, Santa Monica, 1948. · Zbl 0035.00602
[4] A. Seidenberg, A new decision method of elementary algebra, Annals of Mathematics, 1954, 60: 365–371. · Zbl 0056.01804 · doi:10.2307/1969640
[5] G. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Lecture Notes Computer Sciences 33, Springer-Verlag, Berlin, Heidelberg, 1975. · Zbl 0318.02051
[6] D. Arnon, Geometric reasoning with logic and algebra, Artificial Intelligence, 1988, 37: 37–60. · Zbl 0705.68086 · doi:10.1016/0004-3702(88)90049-5
[7] W. T. Wu, On the decision problem and the mechanization of theorem proving in elementary geometry, Journal of Systems Science and Mathematical Science, 1978, 21(16): 157–179 (in Chinese).
[8] W. T. Wu, Basic Principles of Mechanical Theorem Proving in Geometries, Science Press, Beijing, 1984 (in Chinese).
[9] J. Ritt, Differential Algebra, American Mathematical Society, New York, 1950. · Zbl 0037.18402
[10] S. C. Chou, An introduction to Wu’s method for mechanical theorem proving in geometry, Journal of Automated Reasoning, 1988, 4: 237–267. · Zbl 0715.03005 · doi:10.1007/BF00244942
[11] S. C. Chou, Proving Elementary Geometry Theorems Using Wu’s Algorithm, Automated Theorem Proving: After 25 Years (ed. by W. Bledsoe and D. Loveland), AMS Contemporary Mathematics Series, 1984, 29: 243–286.
[12] S. C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht, Netherlands, 1988.
[13] B. Kutzler and S. Stifter, On the application of Buchberger’s algorithm to automated geometry theorem proving, Journal of Symbolic Computation, 1986, 2: 389–397. · Zbl 0629.68086 · doi:10.1016/S0747-7171(86)80006-2
[14] B. Buchberger, G. Collins, and B. Kutzler, Algebraic methods for geometric reasoning, Annual Review of Computer Sciences, 1995, 3(19): 85–119. · doi:10.1146/annurev.cs.03.060188.000505
[15] D. Kapur, T. Saxena, and L. Yang, Algebraic and geometric reasoning with dixon resultants, Proceedings of International Symposium on Symbolic and Algebraic Computation (Oxford, 1994), ACM Press, New York, 1994 99–107. · Zbl 0964.68536
[16] J. Z. Zhang, L. Yang, and X. R. Hou, The sub-resultant method for automated theorem proving, Journal of Systems Science and Mathematical Sciences, 1995, 15(1): 10–15. (in Chinese). · Zbl 0839.68090
[17] D. M. Wang, Elimination procedures for mechanical theorem proving in geometry, Annals of Mathematics and Artificial Intelligence, 1995, 13: 1–24. · Zbl 0855.68090 · doi:10.1007/BF01531321
[18] J. W. Hong, Can geometry be proved by an example? Scientia Sinica, 1986, 29: 824–834. · Zbl 0606.68084
[19] J. Z. Zhang and L. Yang, Principles of parallel numerical method and single-instance method of mechanical theorem proving, Mathematics in Practice and Theory, 1989, 1: 34–43.
[20] J. Z. Zhang, L. Yang, and M. Deng, The parallel numerical method of mechanical theorem proving, Theoretical Computer Science, 1990, 74: 253–271. · Zbl 0701.68087 · doi:10.1016/0304-3975(90)90077-U
[21] H. Gelernter and N. Rochester, Intelligent behavior in problem-solving machines, IBM Journal, 1958: 336–345.
[22] H. Gelernter, Realization of a Geometry Theorem Machine, Computers and Thought (ed. by E. Feigenbaum and J. Feldman), McGraw-Hill, New York, 1963. · Zbl 0158.16208
[23] H. Gelernter, J. Hansen, and D. Loveland, Empirical Explorations of the Geometry Theorem Proving Machine, Computers and Thought (ed. by E. Feigenbaum and J. Feldman), McGraw-Hill, New York, 1963.
[24] S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated Production of Traditional Proofs for Theorems in Euclidean Geometry, IV, A Collection of 400 Geometry Theorems, TR-92-7, Department of Computer Science, WSU, 1992.
[25] S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated production of traditional proofs for constructive geometry theorems, Proceedings of Eighth IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1993.
[26] J. Z. Zhang, X. S. Gao, and S. C. Chou, The geometric information search system by forward reasoning, Chinese Journal of Computers, 1996, 19(10): 721–727 (in Chinese).
[27] S. C. Chou, X. S. Gao, and J. Z. Zhang, A deductive database approach to automated geometry theorem proving and discovering, Journal of Automated Reasoning, 2000, 25(3): 219–246. · Zbl 0961.68121 · doi:10.1023/A:1006171315513
[28] H. Goldstein, Elementary Geometry Theorem Proving, AIM-280, MIT, Cambridge, Massachusetts, 1973.
[29] J. Anderson, C. Boyle, A. Corbett, and M. Lewis, The geometry tutor, Proceedings of IJCAI’85, Los Angles, 1985.
[30] P. Gilmore, An examination of the geometry theorem proving machine, Artificial Intelligence, 1970, 1(2): 171–187. · Zbl 0205.31602 · doi:10.1016/0004-3702(70)90005-6
[31] A. Nevins, Plane geometry theorem proving using forward chaining, Artificial Intelligence, 1975, 6(1): 1–23. · Zbl 0301.68086 · doi:10.1016/0004-3702(75)90013-2
[32] S. Ullman, Model-Driven Geometry Theorem Prover, AIM-321, MIT, Cambridge, Massachusetts, 1975.
[33] H. Coelho and L. Pereira, Automated reasoning in geometry theorem proving with prolog, Journal of Automated Reasoning, 1986, 2(4): 329–390. · Zbl 0642.68161 · doi:10.1007/BF00248249
[34] T. Evans, A Heuristic Program to Solve Geometry Analogy Problems, Semantic Information Processing (ed. by M. Minsky), MIT Press, Cambridge, 1969.
[35] J. Anderson, Tuning of Search of the Problem Space for Geometry Proofs, Proceeding of IJCAI’81, Vancouver, 1981.
[36] Y. Zheng, S. C. Chou, and X. S. Gao, Visually dynamic presentation of proofs in plane geometry – part 2. Automated generation of visually dynamic presentation with the Full-Angle method and the deductive database method, Journal of Automated Reasoning, 2010, 45(3): 243–266 · Zbl 1211.68373 · doi:10.1007/s10817-009-9163-4
[37] X. S. Gao, J. Z. Zhang, and S. C. Chou, Geometry Expert, Nine Chapters Publishing, TaiPei, Taiwan, 1998 (in Chinese).
[38] J. G. Jiang and J. Z. Zhang, The automated geometry reasoning network based on equivalent class reasoning, Patttern Recognition and Artificial Intelligence, 2006, 19(5): 617–622 (in Chinese).
[39] J. G. Jiang and J. Z. Zhang, The automated geometry reasoning system based on RETE algorithm, Journal of Sichuan University: Engineering Science Edition, 2006, 38(3): 135–139 (in Chinese).
[40] J. G. Jiang, J. Z. Zhang, and X. J. Wang, Readable proving for a class of geometric theorems of polynomial equality type, Chinese Journal of Computers, 2008, 31(2): 207–213 (in Chinese). · doi:10.3724/SP.J.1016.2008.00207
[41] R. Welham R, Geometry Problem Solving, D.A.I. Research Report No.14, 1976.
[42] R. Wong, Construction Heuristics for Geometry and a Vector Algebra Representation of Geometry, Technical Memorandum 28, Project MAC, MIT, Cambridge, Massachusetts, 1973.
[43] R. Reiter, A semantically guided deductive system for automatic theorem proving, IEEE Transactions on Computers, 1977, C-25(4): 328–334. · Zbl 0324.68052 · doi:10.1109/TC.1976.1674613
[44] A. Robinson, Proving a theorem (as done by Man, Logician, or Machine), Automation of Reasoning (ed. by J. Siekmann and G. Wrightson), Springer-Verlag, Berlin, Heidelberg, 1983.
[45] W. Elcock, Representation of knowledge in geometry machine, Machine Intelligence (ed. by W. Elcock and D. Michie), John Wiley and Sons, 1977, 8: 11–29.
[46] G. Greeno, M. Magone, and S. Chaiklin, Theory of constructions and set in problem solving, Memory and Cognition, 1979, 7(6): 445–461. · doi:10.3758/BF03198261
[47] N. Matsuda and K. Van Lehn, GRAMY: A geometry theorem prover capable of construction, Journal of Automated Reasoning, 2004. 32(1): 3–33. · Zbl 02081543 · doi:10.1023/B:JARS.0000021960.39761.b7
[48] J. McCharen, R. Overbeek, and L. Wos, Problems and experiments for and with automated theorem-proving programs, IEEE Transactions on Computers, 1976, C-25: 773–782. · Zbl 0329.68075 · doi:10.1109/TC.1976.1674696
[49] A. Quaife, Automated Development of Tarski’s geometry, Journal of Automated Reasoning, 1989, 5: 97–118. · Zbl 0683.68082 · doi:10.1007/BF00245024
[50] L. Meikle and J. Fleuriot, Formalizing Hilbert’s grundlagen in Isabelle/Isar, Theorem Proving in Higher Order Logics, 2003: 319–334. · Zbl 1279.68291
[51] P. Scott, Mechanizing Hilbert’s Foundations of Geometry in Isabelle, Master Thesis, School of Informatics, University of Edinburgh, 2008.
[52] C. Dehlinger, J. Dufourd, and P. Schreck, Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry, Automated Deduction in Geometry (2000), LNAI 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001. · Zbl 0985.68078
[53] J. Narboux, A decision procedure for geometry in Coq, Proceedings of TPHOLs’ 2004, LNCS 3223 (ed. by S. Konrad, B. Annett, and G. Genesh), 2004. · Zbl 1099.68734
[54] J. Z. Zhang, S. C. Chou, and X. S. Gao, Automated production of traditional proofs for theorems in Euclidean geometry, I: The Hilbert intersection point theorems, Annals of Mathematics and Artificial Intelligence, 1995, 13: 109–137. · Zbl 0855.68095 · doi:10.1007/BF01531326
[55] J. Narboux, A graphical user interface for formal proofs in geometry, Journal of Automated Reasoning, 2007, 39: 161–180. · Zbl 1131.68094 · doi:10.1007/s10817-007-9071-4
[56] R. Caferra, N. Peltier, and F. Puitg, Emphasizing human techniques in automated geometry theorem proving: A practical realization, Automated Deduction in Geometry (2000), LNAI 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001. · Zbl 0985.68058
[57] S. Fèvre, Integration of reasoning and algebraic calculus in geometry, Automated Deduction in Geometry (1996), Lecture Notes in Artificial Intelligence 1360, Springer-Verlag, Berlin, Heidelberg, 1998.
[58] S. F‘evre and D. M. Wang, Combining algebraic computing and term-rewriting for geometry theorem proving. Proceedings of AISC’98, Pittsburgh, USA, 1998. · Zbl 0914.03014
[59] G. Défourneaux, C. Bourely, and N. Peltier, Semantic generalizations for proving and disproving conjectures by analogy, Journal of Automated Reasoning, 1998, 20(1–2): 27–45. · Zbl 0893.68134 · doi:10.1023/A:1005944606876
[60] S. C. Chou, X. S. Gao, and J. Z. Zhang, Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems, World Scientific, Singapore, 1994. · Zbl 0941.68503
[61] J. Z. Zhang, Points Elimination Methods for Geometric Problem Solving, Mathematics Mechanization and Applications (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000.
[62] P. Janičić, J. Narboux, and P. Quaresma, The area method: A recapitulation, Journal of Automated Reasoning, 2012, 48(4): 489–532 · Zbl 1242.68281 · doi:10.1007/s10817-010-9209-7
[63] J. Z. Zhang, How to Solve Geometry Problems Using Areas, Shanghai Educational Publishing Inc., Shanghai, 1982 (in Chinese).
[64] J. Z. Zhang and P. Cao, From Education of Mathematics to Mathematics for Education, Sichun Educational Publishing Inc., Chengdu, 1988 (in Chinese).
[65] J. Z. Zhang, A New Approach to Plane Geometry, Sichuan Educational Publishing Inc., Chengdu, 1992 (in Chinese).
[66] S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated generation of readable proofs with geometric invariants, I: Multiple and shortest proofs generation, Journal of Automated Reasoning, 1996, 17(3): 325–347. · Zbl 0865.68109 · doi:10.1007/BF00283133
[67] S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated generation of readable proofs with geometric invariants, II: Theorem proving with full-angles, Journal of Automated Reasoning, 1996, 17(3): 349–370. · Zbl 0865.68110 · doi:10.1007/BF00283134
[68] S. C. Chou, X. S. Gao, and J. Z. Zhang, A Collection of 110 Geometry Theorems and Their Machine Proofs Based on Full-Angles, TR-94-4, Department of Computer Science, WSU, 1994.
[69] Y. Zou and J. Z. Zhang, Automated generation of readable proofs for constructive geometry statements with the mass point method, Automated Deduction in Geometry (2010), Lecture Notes in Artificial Intelligence 6877, Springer-Verlag, Berlin Heidelberg, 2011. · Zbl 1350.68246
[70] S. C. Chou, X. S. Gao, and J. Z. Zhang, Mechanical geometry theorem proving by vector calculation, Proceedings of International Symposium on Symbolic and Algebraic Computation (Kiev, Ukraine, July 6–8, 1993), ACM Press, New York, 1993. · Zbl 0968.03520
[71] S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated production of traditional proofs in solid geometry, Journal of Automated Reasoning, 1995, 14: 257–291. · Zbl 0824.03005 · doi:10.1007/BF00881858
[72] L. Yang, X. S. Gao, S. C. Chou, and J. Z. Zhang, Automated production of readable proofs for theorems in non-euclidean geometries, Automated Deduction in Geometry, Lecture Notes Computer Sciences 1360, Springer-Verlag, Berlin, Heidelberg, 1997.
[73] H. B. Li, Clifford algebra approaches to mechanical geometry theorem proving, Mathematics Mechanization (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000.
[74] B. Sturmfels, Computational algebraic geometry of projective configurations, Journal of Symbolic Computation, 1993, 11: 595–618. · Zbl 0766.14043 · doi:10.1016/S0747-7171(08)80121-6
[75] J. Righter-Gebert, Mechanical theorem proving in projective geometry, Annals of Mathematics and Artificial Intelligence, 1995, 13: 139–172. · Zbl 0855.68096 · doi:10.1007/BF01531327
[76] H. B. Li, New Explorations in Automated Theorem Proving in Geometries, Ph.D. Thesis, Peking University, China, 1994.
[77] H. B. Li, Some applications of clifford algebra to geometries, Automated Deduction in Geometry (1989), Lecture Notes in Artificial Intelligence 1669, Springer-Verlag, Berlin, Heidelberg, 1998.
[78] D. M. Wang, Clifford algebraic calculus for geometric reasoning with application to computer vision, Automated Deduction in Geometry (1996), Lecture Notes in Artificial Intelligence 1360, Springer-Verlag, Berlin, Heidelberg, 1998.
[79] H. B. Li and H. Shi, On Erdös’ ten-point problem, Acta Mathematica Sinica, New Series, 1997, 13(2): 221–230. · Zbl 0885.52016
[80] S. Fèvre and D. M. Wang, Proving geometric theorems using clifford algebra and rewrite rules, Lecture Notes in Artificial Intelligence 1421 (ed. by D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 1997.
[81] H. Q. Yang, S. G. Zhang, and G. C. Feng, A Clifford algebraic method for geometric reasoning, Automated Deduction in Geometry (Beijing, 1998), Lecture Notes in Artificial Intelligence 1669 (ed. by X. S. Gao, D. M. Wang, and L. Yang), Springer-Verlag, Berlin, Heidelberg, 1999.
[82] H. B. Li, Vectorial equation-solving for mechanical geometry theorem proving, Journal of Automated Reasoning, 2000, 25: 83–121. · Zbl 0959.03008 · doi:10.1023/A:1006182023017
[83] H. B. Li and M. Cheng, Clifford algebraic reduction method for automated theorem proving in differential geometries, Journal of Automated Reasoning, 1998, 21: 1–21. · Zbl 0914.03015 · doi:10.1023/A:1005819428156
[84] H. B. Li, Mechanical theorem proving in differential geometry, Mathematics Mechanization (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000.
[85] A. Dolzmann, T. Sturm, and V. Weispfenning, A new approach for automatic theorem proving in real geometry, Journal of Automated Reasoning, 1998, 21(3): 357–380. · Zbl 0914.03013 · doi:10.1023/A:1006031329384
[86] W. T. Wu, On problems involving inequalities, MM-Res, Preprints, MMRC, 1992, 7: 103–138.
[87] W. T. Wu, On a finiteness theorem about problems involving inequalities, Journal of Systems Science and Mathematical Sciences, 1994, 7(2): 193–200. · Zbl 0811.65047
[88] D. M. Wang, Polynomial Equations Solving and Mechanical Geometric Theorem Proving, Ph.D. Thesis, Institute of Systems Science, Chinese Academy of Sciences, Beijing, 1993.
[89] L. Yang, Recent advances in automated theorem proving on inequalities, Journal of Computer Science and Technology, 1999, 14(5): 434–446. · Zbl 0944.68169 · doi:10.1007/BF02948785
[90] L. Yang, X. R. Hou, and B. C. Xia, A complete algorithm for automated discovering of a class of inequality-type theorems, Science in China (Series F), 2001, 44(1): 33–49. · Zbl 1125.68406 · doi:10.1007/BF02713938
[91] L. Yang and J. Z. Zhang, A practical program of automated proving for a class of geometric inequalities, Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001. · Zbl 0985.68556
[92] O. Bottema, et al, Geometric Inequalities, Wolters-Noordhoff Publishing, Groningen, Netherlands, 1969. · Zbl 0174.52401
[93] L. Yang, Solving harder problems with lesser mathematics, Proceedings of the 10th Asian Technology Conference in Mathematics, ATCM Inc., Blacksburg, 2005.
[94] L. Yang, Difference substitution and automated inequality proving, Journal of Guangzhou University: Natural Science Edition, 2006, 5(2): 1–7 (in Chinese).
[95] L. Yang and Y. Yao, Difference substitution matrices and decision on nonnegativity of polynomials, Journal of Systems Science and Mathematical Sciences, 2009, 29(9): 1169–1177 (in Chinese). · Zbl 1212.68257
[96] Y. Yao, Infinite product convergence of column stochastic mean matrix and machine decision for positive semi-definite forms, Science China Mathematics (Series A), 2010, 53(3): 251–264 (in Chinese). · Zbl 1188.53008 · doi:10.1007/s11425-010-0004-z
[97] S. H. Xia, Automated Production of Readable Proof for a Class of Inequality-type Theorems, Ph.D, Thesis, Chinese Academy of Sciences, Beijing, 2002.
[98] S. Chen and J. Z. Zhang, Automated production of elementary and readable proof of inequality, Journal of Sichuan University: Engineering Science Education, 2003, 35(4): 86–93 (in Chinese).
[99] S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated geometry theorem proving and geometry education, Proceedings of Asian Technology Conference in Mathematics, Association of Mathematics Educators, Singapore, 1995.
[100] C. Z. Li and J. Z. Zhang, Readable machine solving in geometry and ICAI software MSG, Automated Deduction in Geometry (1998), Lecture Notes in Artificial Intelligence 1669, Springer-Verlag, Berlin, Heidelberg, 1998.
[101] S. C. Chou, X. S. Gao, and J. Z. Zhang, An introduction to geometry expert, Proceedings of CADE-13, Lecture Notes in Artifficial Intelligence (ed. by M. McRobbie and J. Slaney), Springer-Verlag, Berlin, Heidelberg, 1996.
[102] Y. Zheng, S. C. Chou, and X. S. Gao, An introduction to java geometry expert-(extended abstract), Automated Deduction in Geometry – 7th International Workshop (2008), LNCS 6301 (ed. by T. Sturm and C. Zengler), Springer, 2011. · Zbl 1302.68247
[103] Y. Zheng, S. C. Chou, and X. S. Gao, Visually dynamic presentation of proofs in plane geometry – part 1. Basic features and the manual input method, Journal of Automated Reasoning, 2010, 45(3): 213–241. · Zbl 1211.68372 · doi:10.1007/s10817-009-9162-5
[104] X. S. Gao, Q. Lin, MMP/Geometer-A software package for automated geometry reasoning, Automated Deduction in Geometry (Hagenberg Castle, Austria, 2002) (ed. by F. Winkler), Springer-Verlag, Berlin, Heidelberg, 2004: 44–66.
[105] C. Z. Li and J. Z. Zhang, Super Sketchpad, Beijing Normal University Press, Beijing, 2004 (in Chinese).
[106] S. Wilson and J. Fleuriot, Geometry explorer: combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs, Proceedings of the 12th Workshop on Automated Reasoning (ARW), Edinburgh, UK, 2005.
[107] P. Janicic and P. Quaresma, System description: GCLCprover + GeoThms, International Joint Conference on Automated Reasoning (IJCAR-2006), Lecture Notes in Artificial Intelligence 4130 (ed. by U. Furbach and N. Shankar), Springer-Verlag, Berlin, Heidelberg, 2006.
[108] H. Zheng and J. Z. Zhang, Reasoning of algorithm of geometry automatic reasoning platform with sustainable development by user, Journal of Computer Applications, 2011, 31(8): 2101–2107 (in Chinese).
[109] H. Zheng, The sustainable geometry automated reasoning platform, Journal of System Science and Mathematical Sciences, 2011, 31(12): 1622–1632 (in Chinese). · Zbl 1265.68213
[110] A. Samuel, Some studies in machine learning using the game of checkers, IBM Journal of Research and Development, 1959, 3(3): 210–229. · doi:10.1147/rd.33.0210
[111] A. Samuel, Some studies in machine learning using the game of checkers II – Recent progress, IBM Journal of Research and Development, 1967, 11(6): 601–617. · doi:10.1147/rd.116.0601
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.