Clifford Algebraic Reduction Method for Automated Theorem Proving in Differential Geometry
Tóm tắt
In this paper a new method is proposed for mechanically proving theorems in the local theory of space curves. The method is based on Ritt-Wu’s well-ordering principle of ordinary differential polynomials, Clifford algebraic representation of Euclidean space and equation set solving in Clifford algebra formalism. It has been tested by various theorems and seems to be efficient.
Tài liệu tham khảo
Wen-tsun Wu: On the mechanization of theorem proving in elementary and differential geometry, Scientia Sinica, Math. Supplement (I), 1979 (in Chinese).
Wen-tsun Wu: A Constructive Theory of Differential Algebraic Geometry, Lect. Notes in Math., 1255, Springer-Verlag, 1987.
Wen-tsun Wu: A mechanization method of geometry and its applications II. Curve pairs of Bertrand type, Chinese Science Bulletin 32(9) (1987).
Wen-tsun Wu: Mechanical theorem proving of differential geometries and some of its applications in mechanics, J. Automated Reasoning 7(2) (1991), 171–191.
Chou, S. C. and Gao, X. S.: Automated reasoning in differential geometry and mechanics using the characteristic set method - I, II, J. Automated Reasoning 10(2) (1993), 161–172.
Ferro, G. C. and Gallo, G.: A Procedure to Prove Statements in Differential Geometries, J. Automated Reasoning 6(2) (1990), 203–209.
Li, Z. M.: Mechanical Theorem-Proving of the Local Theory of the Surfaces, MM Research Preprints 6, 1991, MMRC, Institute of Systems Science, Academia Sinica, Beijing.
Wang, D. M.: A method for proving theorems in differential geometry and mechanics, J. Universal Computer Science 1(9) (1995).
Hestenes, D. and Sobczyk, G.: Clifford Algebra to Geometric Calculus, D. Reidel, Dordrecht/Boston, 1984.
Li Hongbo, and Cheng Minteh: Ordering in automated theorem proving of differential geometry, Chinese J. Appl. Math. (to appear).
Chen Weihuan: Preliminaries of Differential Geometry, Peking Univ. Pr., 1990 (in Chinese).