|
|||||
|
|
| ORDERING IN AUTOMATED THEOREMPROVING OF DIFFERENTIAL GEOMETRY | |
| 引用本文： | 李洪波,程民德. ORDERING IN AUTOMATED THEOREMPROVING OF DIFFERENTIAL GEOMETRY[J]. 应用数学学报(英文版), 1998, 14(4): 358-362. DOI: 10.1007/BF02683818 |
| 作者姓名： | 李洪波 程民德 |
| 作者单位： | LI HONGBO (Institute of Systems Science，the Chinese Academy of Sciences，Beijing 100080，China)CHENG MINTEH (Institute of Mathematics，Peking University，Beijing 100871，China) |
| 摘 要： | 1.BackgroundMom1979,WuWentsunbeganthestudyofautomatedtheoremprovingindifferentialgeometry[1].Inhismethod,thehypotheses,representedbydifferentialpolynomials,aretriangulatedaccordingtoanorderofthevariablesinthepolynomials;theconclusionisprovedbythetriangulatedresultcalledcharacteristicset.Wuusedelement-basedorderingmethodwhichcanbeillustratedbythisexample'LettingxKybetwosmoothfunctionsofthesamevariable,thenxKX'KX"K'Ky'y,Ky"'.ThisorderisthefoundationofWu'seliminationprinciple.However,a… |
| 收稿时间： | 1995-10-24 |
Ordering in automated theorem proving of differential geometry |
|
| Li Hongbo,Cheng Minteh. Ordering in automated theorem proving of differential geometry[J]. Acta Mathematicae Applicatae Sinica, 1998, 14(4): 358-362. DOI: 10.1007/BF02683818 | |
| Authors: | Li Hongbo Cheng Minteh |
| Affiliation: | (1) Institute of Systems Science, the Chinese Academy of Sciences, 100080 Beijing, China;(2) Institute of Mathematics, Peking University, 100871 Beijing, China |
| Abstract: | A new ordering method is proposed for automated theorem proving of differential geometry,by which Cartan's moving frame method can be combined with Wu's elimination principle. |
| Keywords: | Wu's method ordering |
| 本文献已被 CNKI SpringerLink 等数据库收录！ | |