In this paper, we generalize the method of mechanical theorem proving in curves to prove theorems about surfaces in differential geometry with a mechanical procedure. We improve the classical result on Wronskian deter...In this paper, we generalize the method of mechanical theorem proving in curves to prove theorems about surfaces in differential geometry with a mechanical procedure. We improve the classical result on Wronskian determinant, which can be used to decide whether the elements in a partial differential field are linearly dependent over its constant field. Based on Wronskian determinant, we can describe the geometry statements in the surfaces by an algebraic language and then prove them by the characteristic set method.展开更多
Let F be an irreducible differential polynomial over k(t)with k being an algebraically closed field of characteristic zero.The authors prove that F=0 has rational general solutions if and only if the differential alge...Let F be an irreducible differential polynomial over k(t)with k being an algebraically closed field of characteristic zero.The authors prove that F=0 has rational general solutions if and only if the differential algebraic function field over k(t)associated to F is generated over k(t)by constants,i.e.,the variety defined by F descends to a variety over k.As a consequence,the authors prove that if F is of first order and has movable singularities then F has only finitely many rational solutions.展开更多
基金the National Key Basic Research Project of China (Grant No.2004CB318000)
文摘In this paper, we generalize the method of mechanical theorem proving in curves to prove theorems about surfaces in differential geometry with a mechanical procedure. We improve the classical result on Wronskian determinant, which can be used to decide whether the elements in a partial differential field are linearly dependent over its constant field. Based on Wronskian determinant, we can describe the geometry statements in the surfaces by an algebraic language and then prove them by the characteristic set method.
基金the National Natural Science Foundation of China under Grants Nos.11771433and 11688101Beijing Natural Science Foundation under Grants No.Z190004。
文摘Let F be an irreducible differential polynomial over k(t)with k being an algebraically closed field of characteristic zero.The authors prove that F=0 has rational general solutions if and only if the differential algebraic function field over k(t)associated to F is generated over k(t)by constants,i.e.,the variety defined by F descends to a variety over k.As a consequence,the authors prove that if F is of first order and has movable singularities then F has only finitely many rational solutions.
