Wu’s method and its application to perspective viewing. (English) Zbl 0664.68102
Wu developed a method to prove automatically geometric theorems. Hundreds of, - at times non trivial, - theorems in plane geometry have been proven, by using certain implementations of the method. It rests upon an algebraic approach, namely the translation of both hypotheses and conjectures into polynomial equations. The authors describe the method and give as applications proving properties of perspective viewing, relevant to image understanding, and handling nonlinear inequalities.
Reviewer: G.Molenberghs
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 51-04 | Software, source code, etc. for problems pertaining to geometry |
References:
| [1] | Arnon, D. S.; Collins, G. E.; McCallum, S., Cylindrical algebraic decomposition I: The basic algorithm; II: An adjacency algorithm for the plane, SIAM J. Comput., 13, 878-889 (1984) · Zbl 0562.14001 |
| [2] | Chou, S.-C., Proving elementary geometry theorems using Wu’s algorithm, (Bledsoe, W. W.; Loveland, D. W., Theorem Proving: After 25 Years. Theorem Proving: After 25 Years, Contemporary Mathematics, 29 (1984)), 243-286 · Zbl 0578.68079 |
| [3] | Chou, S.-C., Proving and discovering theorems in elementary geometry using Wu’s method, (Ph.D. Thesis (1985), Department of Mathematics, University of Texas: Department of Mathematics, University of Texas Austin, TX) |
| [4] | Chou, S.-C.; Schelter, W. F., Proving geometry theorems with rewrite rules, J. Autom. Reasoning, 2, 3, 253-273 (1986) · Zbl 0642.68162 |
| [5] | Coelho, H.; Pereira, L. M., Automated reasoning in geometry theorem proving with PROLOG, J. Autom. Reasoning, 2, 4, 329-390 (1986) · Zbl 0642.68161 |
| [6] | Duda, R. O.; Hart, P., (Pattern Classification and Scene Analysis (1973), Wiley: Wiley New York), 379-404, Chapter 10 · Zbl 0277.68056 |
| [7] | Kapur, D.; Musser, D. R.; Mundy, J. L.; Narendran, P., Reasoning about three dimensional space, (Proceedings IEEE International Conference on Robotics and Automation. Proceedings IEEE International Conference on Robotics and Automation, St. Louis, MO (1985)), 405-410 |
| [8] | Kapur, D., Geometry theorem proving using Hilbert’s Nullstellensatz, (Proceedings 1986 Symposium on Symbolic and Algebraic Computation (SYMSAC 86). Proceedings 1986 Symposium on Symbolic and Algebraic Computation (SYMSAC 86), Waterloo, Ont. (1986)), 202-208, (an expanded version is in this volume) |
| [9] | Knuth, D. E., (Seminumerical Algorithms: The Art of Computer Programming, 2 (1980), Addison-Wesley: Addison-Wesley Reading, MA), 407-408 |
| [10] | Ko, H. P.; Hussain, M. A., A study of Wu’s method—A method to prove certain theorems in elementary geometry, (Congr. Numer., 48 (1985)), 225-242 · Zbl 0634.03010 |
| [11] | Ko, H. P.; Hussain, M. A., ALGE-prover: An algebraic geometry theorem proving software, (Tech. Rept. 85CRD139 (1985), General Electric Corporate Research and Development: General Electric Corporate Research and Development Schenectady, NY) |
| [12] | Ko, H. P., Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle, Artificial Intelligence, 37 (1989), this volume |
| [13] | Kutzler, B.; Stifter, S., Automated geometry theorem proving using Buchberger’s algorithm, (Proceedings 1986 Symposium on Symbolic and Algebraic Computation (SYMSAC 86). Proceedings 1986 Symposium on Symbolic and Algebraic Computation (SYMSAC 86), Waterloo, Ont. (1986)), 209-214 · Zbl 0629.68086 |
| [14] | Mundy, J. L., Image understanding research at General Electric, (Proceedings Image Understanding Workshop. Proceedings Image Understanding Workshop, Miami Beach, FL (1985)), 83-88 |
| [15] | Shafer, S.; Kanade, T.; Kender, J., Gradient space under orthography and perspective, Comput. Vision Graph. Image Process., 24 (1983) · Zbl 0585.68086 |
| [16] | Swain, M. J.; Mundy, J. L., Experiments in using a geometry theorem prover to prove and develop theorems in computer vision, (Proceedings IEEE Conference on Robotics and Automation. Proceedings IEEE Conference on Robotics and Automation, San Francisco, CA (1986)), 280-285 |
| [17] | Tarski, A., (A Decision Method for Elementary Algebra and Geometry (1948), University of California Press: University of California Press Berkeley, CA), 1951 · Zbl 0044.25102 |
| [18] | (Bledsoe, W. W.; Loveland, D. W., Theorem Proving: After 25 Years. Theorem Proving: After 25 Years, Contemporary Mathematics, 29 (1984)), 213-234 · Zbl 0545.00023 |
| [19] | Wu, W., Some recent advances in mechanical theorem proving of geometries, (Bledsoe, W. W.; Loveland, D. W., Theorem Proving: After 25 Years. Theorem Proving: After 25 Years, Contemporary Mathematics, 29 (1984)), 235-241 · Zbl 0578.68077 |
| [20] | J. Autom. Reasoning, 2, 221-252 (1986) · Zbl 0642.68163 |
| [21] | Wu, W., On reducibility problem in mechanical theorem proving of elementary geometries (1986), Institute of Systems Science, Academia Sinica: Institute of Systems Science, Academia Sinica China, Unpublished Manuscript |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
