Mathematics mechanization and applications after thirty years

The aim of mathematics mechanization is to develop symbolic algorithms for manipulating mathematical objects, proving and discovering theorems in a mechanical way. This paper gives a brief review of the major advances in the field over the past thirty years. The characteristic set method for symbolic solution of algebraic, differential, and difference equation systems are first introduced. Methods for automated proving and discovering geometry theorems are then reviewed. Finally, applications in computer-aided geometric design, computer vision, intelligent computeraided design, and robotics are surveyed. Keywords mathematics mechanization, characteristic set method, automated theorem proving, automated theorem discovering, symbolic equation solving, computer aided geometric design, computer vision, intelligent computeraided design, robotics

• Type: Journal
• Year: 2007
• Where: FCSC
• Authors: Wenjun Wu, Xiaoshan Gao
• Keywords: Difference Equation Systems, FCSC 2007, Geometric Design, Mathematics Mechanization