Mechanical theorem proving in differential geometry - Local theory of surfaces

被引：3

作者：

Li, HB

机构：

[1] Chinese Academy of Sciences,Institute of Systems Science

来源：

SCIENCE IN CHINA SERIES A-MATHEMATICS PHYSICS ASTRONOMY | 1997年 / 40卷 / 04期

关键词：

Wu's method; differential forms; Chern's theorem;

D O I：

10.1007/BF02911434

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

An automated reasoning method, based on Wu's method and calculus of differential forms, is proposed for mechanical theorem proving in local theory of space surfaces in differential geometry. The method has been used to simplify one of Chern's theorems: ''The non-trivial families of isometric surfaces having the same principal curvatures are W-surfaces.'' It Some other theorems are also tested by this method. The proofs are generally simpler than those in differential geometry textbooks.

引用

下载

页码：350 / 356

页数：7

共 50 条

[31] A reification of a strategy for geometry theorem proving
Matsuda, N
VanLehn, K
INTELLIGENT TUTORING SYSTEMS, PROCEEDINGS, 2000, 1839 : 660 - 660
[32] Visual reasoning in geometry theorem proving
1617, Morgan Kaufmann Publ Inc, San Mateo, CA, USA (02):
[33] ON ANALOGUES OF BACKLUND THEOREM IN AFFINE DIFFERENTIAL GEOMETRY OF SURFACES
Robaszewska, Maria
JOURNAL OF GEOMETRY AND SYMMETRY IN PHYSICS, 2019, 54 : 79 - 110
[34] AUTOMATED REASONING IN DIFFERENTIAL GEOMETRY AND MECHANICS USING THE CHARACTERISTIC SET METHOD .2. MECHANICAL THEOREM-PROVING
CHOU, SC
GAO, XS
JOURNAL OF AUTOMATED REASONING, 1993, 10 (02) : 173 - 189
[35] Mechanical theorem proving of differential geometries and some of its applications in mechanics
1600, (07):
[36] ON THE LOCAL EMBEDDING PROBLEMS IN THE DIFFERENTIAL GEOMETRY OF SURFACES
WINTNER, A
AMERICAN JOURNAL OF MATHEMATICS, 1955, 77 (04) : 845 - 852
[37] Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving
Ning Zhang
Hong-bo Li
Science in China Series A: Mathematics, 2007, 50 : 941 - 950
[38] Mechanical theorem proving in the surfaces using the characteristic set method and Wronskian determinant
FENG RuYong1 & YU JianPing2 1 Key Lab of Mathematics Mechanization
Science China Mathematics, 2008, (10) : 1763 - 1774
[39] Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving
Ning ZHANG~(1+) Hong-bo LI~2 1 China Institute for Actuarial Science (CIAS)
2 Academy of Mathematics and Systems Science
Science China Mathematics, 2007, (07) : 941 - 950
[40] Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving
Zhang, Ning
Li, Hong-bo
SCIENCE IN CHINA SERIES A-MATHEMATICS, 2007, 50 (07): : 941 - 950

← 1 2 3 4 5 →