共查询到20条相似文献,搜索用时 0 毫秒
1.
Mechanical theorem proving in differential geometry 总被引:1,自引:0,他引:1
Hongbo Li 《中国科学A辑(英文版)》1997,40(4):350-356
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 Chem’s theorems:
“The non-trivial families of isometric surfaces having the same principal curvatures are W-surfaces.” Some other theorems
are also tested by this method. The proofs are generally simpler than those in differential geometry textbooks.
Project supported partially by the National Natural Science Foundation of China. 相似文献
2.
Ordering in mechanical geometry theorem proving 总被引:2,自引:0,他引:2
Hongbo Li 《中国科学A辑(英文版)》1997,40(3):225-233
Ordering in mechanical geometry theorem proving is studied from geometric viewpoint and some new ideas are proposed. For Thebault’s
theorem which is the most difficult theorem that has ever been proved by Wu’s method, a very simple proof using Wu’s method
under a linear order is discovered.
Project supported by the National Natural Science Foundation of China. 相似文献
3.
Let T be a Banach space operator, E(T) be the set of all isolated eigenvalues of T and π(T) be the set of all poles of T. In this work, we show that Browder's theorem for T is equivalent to the localized single-valued extension property at all complex numbers λ in the complement of the Weyl spectrum of T, and we give some characterization of Weyl's theorem for operator satisfying E(T) = π(T). An application is also given. 相似文献
4.
Ning ZHANG~ 《中国科学A辑(英文版)》2007,50(7):941-950
This paper discusses two problems:one is some important theories and algorithms of affine bracket algebra;the other is about their applications in mechanical theorem proving.First we give some efficient algorithms including the boundary expanding algorithm which is a key feature in application.We analyze the characteristics of the boundary operator and this is the base for the implementation of the system.We also give some new theories or methods about the exact division,the representations and structure of affine geometry and so on.In practice,we implement the mechanical auto-proving system in Maple 10 based on the above algorithms and theories.Also we test about more than 100 examples and compare the results with the methods before. 相似文献
5.
XiLIFENG 《高校应用数学学报(英文版)》1997,12(4):483-492
For real-valued functions defined on Cantor triadic ,set. a derivative with corresponding formula of Newton-Leihniz‘s type is given In particular, for the self-simltar functions and alter-nately jumping functions defined in this paper, their derivative and exceptional sets are studied ac-curately by using ergodic theory on Е2 and Duffin-Scbaeffer‘s theorem coneerning metric diophan-tine approximation. In addition, Haar basis of L2(Е2) is constructed and Flaar expansion of stan-drd self-similar function is given. 相似文献
6.
We consider the relation between versions of Ramsey’s Theorem and König’s Infinity Lemma, in the absence of the axiom of choice. 相似文献
7.
基于多项式组主项解耦消元法 ,将几何定理的假设条件 (多项式组 PS)化为主项只含主变元的三角型多项式组 DTS,可得到定理命题成立的不含变元的非退化条件 ,即充分必要或更接近充分必要的非退化条件 .由于多项式主系数不含变元 ,已不存在 DTS多项式之间的约化问题 ,故方法有普遍意义 .文中例为西姆松定理的机器证明 . 相似文献
8.
L. L. Maksimova 《Algebra and Logic》2007,46(5):341-353
The interpolation property in extensions of Johansson’s minimal logic is investigated. The construction of a matched product
of models is proposed, which allows us to prove the interpolation property in a number of known extensions of the minimal
logic. It is shown that, unlike superintuitionistic, positive, and negative logics, a sum of J-logics with the interpolation property CIP may fail to possess CIP, nor even the restricted interpolation property.
Supported by RFBR grant No. 06-01-00358, by INTAS grant No. 04-77-7080, and by the Council for Grants (under RF President)
and State Aid of Fundamental Science Schools, project NSh-4787.2006.1.
__________
Translated from Algebra i Logika, Vol. 46, No. 5, pp. 627–648, September–October, 2007. 相似文献
9.
B. M. Podlevskii 《Computational Mathematics and Mathematical Physics》2008,48(12):2140-2145
An iterative algorithm is examined for finding the eigenvalues of the two-parameter (multiparameter) algebraic eigenvalue problem. This algorithm uses Newton’s method and an efficient numerical procedure for differentiating determinants. Some numerical examples are given. 相似文献
10.
Rudra P. Sarkar 《Proceedings Mathematical Sciences》2002,112(4):579-593
A theorem of Hardy characterizes the Gauss kernel (heat kernel of the Laplacian) on ℝ from estimates on the function and its
Fourier transform. In this article we establisha full group version of the theorem for SL2(ℝ) which can accommodate functions with arbitraryK-types. We also consider the ‘heat equation’ of the Casimir operator, which plays the role of the Laplacian for the group.
We show that despite the structural difference of the Casimir with the Laplacian on ℝn or the Laplace—Beltrami operator on the Riemannian symmetric spaces, it is possible to have a heat kernel. This heat kernel
for the full group can also be characterized by Hardy-like estimates. 相似文献
11.
12.
We propose a new method of summation to any accuracy for a wide class of divergent series, using only a finite number of terms of the series. Translated fromMatematicheskie Zametki, Vol. 68, No. 1, pp. 24–35, July, 2000. 相似文献
13.
14.
15.
Ioannis K. Argyros 《Central European Journal of Mathematics》2007,5(2):205-214
We provide sufficient convergence conditions for the Secant method of approximating a locally unique solution of an operator
equation in a Banach space. The main hypothesis is the gamma condition first introduced in [10] for the study of Newton’s
method. Our sufficient convergence condition reduces to the one obtained in [10] for Newton’s method. A numerical example
is also provided.
相似文献
16.
We re-examine a quadratically convergent method using divided differences of order one in order to approximate a locally unique
solution of an equation in a Banach space setting [4, 5, 7]. Recently in [4, 5, 7], using Lipschitz conditions, and a Newton-Kantorovich
type approach, we provided a local as well as a semilocal convergence analysis for this method which compares favorably to
other methods using two function evaluations such as the Steffensen’s method [1, 3, 13]. Here, we provide an analysis of this
method under the gamma condition [6, 7, 19, 20]. In particular, we also show the quadratic convergence of this method. Numerical
examples further validating the theoretical results are also provided.
相似文献
17.
N. M. Timofeev 《Mathematical Notes》1999,66(4):474-488
Suppose thatg(n) is equal to the number of divisors ofn, counting multiplicity, or the number of divisors ofn, a≠0 is an integer, andN(x,b)=|{n∶n≤x, g(n+a)−g(n)=b orb+1}|. In the paper we prove that sup
b
N(x,b)≤C(a)x)(log log 10
x
)−1/2 and that there exists a constantC(a,μ)>0 such that, given an integerb |b|≤μ(log logx)1/2,x≥x
o, the inequalityN(x,b)≥C(a,μ)x(log logx(−1/2) is valid.
Translated fromMatematicheskie Zametki, Vol. 66, No. 4, pp. 579–595, October, 1999. 相似文献
18.
B. Cordani 《Regular and Chaotic Dynamics》2008,13(1):46-56
The Arnold web and the Arnold diffusion arise when an integrable Hamiltonian system is slightly perturbed: the first concerns
the peculiar topology characterizing the set of the resonance lines in phase space, the latter the extremaly slow motion (if
any) along these lines. While Arnold has proved the possibility of diffusion, it is still unknown if the phenomenon is generic in realistic physical systems. The system we consider is the
Hydrogen atom (or Kepler problem) subject to the combined action of a constant electric and magnetic field, which is known
as Stark-Zeeman problem. We describe the results of numerical experiments: the Arnold web is clearly highlighted and, looking
at the behaviour of the KAM frequencies on orbits of 108 revolutions, evidence for the diffusion existence is reached.
相似文献
19.
E. Yu. Lerner 《Russian Mathematics (Iz VUZ)》2008,52(12):36-40
We prove that prime witnesses in the Miller-Rabin algorithm coincide with those in the Shor algorithm which satisfy the condition of Fermat’s little theorem. We describe the set of natural numbers, whose prime witnesses in the Miller-Rabin algorithm coincide with those in the Shor algorithm. We find all such numbers less than 100,000,000 and experimentally study the rate of increase of the ratio of the quantity of such numbers to the quantity of Carmichael numbers. 相似文献
20.
E. Kopecká 《Mathematical Notes》2007,81(3-4):308-317
Let K ? ?d be a compact convex set which is an intersection of half-spaces defined by at most two coordinates. Let Q be the smallest axes-parallel box containing K. We show that, as the dimension d grows, the ratio diam Q/ diam K can be arbitrarily large. We also give examples of compact sets in Banach spaces which are not contained in any compact contractive set. 相似文献