Dissertation > Excellent graduate degree dissertation topics show

The Function Differential, Partial Differentiation, Grads, Divergence, and Curl in Mizar

Author: XieBing
Tutor: LiangXiQuan
School: Qingdao University of Science and Technology
Course: Applied Mathematics
Keywords: mathematics mechanization Mizar language system formalized mathematics automated theorem proving
CLC: TP399-C5
Type: Master's thesis
Year: 2009
Downloads: 65
Quote: 1
Read: Download Dissertation


The Mizar system is a computer language system, which is a formalization of mathematical knowledge and information, with the function of proving, verifying and typesetting, possessing of Mizar Mathematical Library.This dissertation introduces mathematics mechanization, describes the history of Mizar system and how to write articles in Mizar language. The article discusses the theory of partial differentiation and higher-order partial derivatives, dissertates the correlative properties as well as grads, divergence, curl in Mizar system, also provides the corresponding proof and calculation methods. The automatic reasoning and proving process, which are related to the above aspects, have been embodied in Mizar Mathematical Library. At the same time, the dissertation has been published in《Formalized Mathematics》(Poland). The main contents are summarized as follows:1. In Mizar language project, the differential coefficient of multivariable function is realized, by dint of this the partial differentiation of real binary functions is defined, their operation together with the relation between differential coefficient and continuity are discussed.2. For the first time the second-order partial differentiation is formalized concisely in Mizar system , the interrelated operation formulas and theorems are also given.3. The correlative theorems are extended in 3-dimensional euclidian space, the definition of grads, divergence, curl as well as theorems and formulas are formalized in Mizar system for the first time.

Related Dissertations

  1. Solutions of Nonlinear Partial Differential Equations by Homotopy Analysis Method,O241.82
  2. Study on Mathematical Software Virtualization in Cloud Environment,TP393.09
  3. Solving Nonlinear Partial Differential Equation and Integrable System,O175.29
  4. Darboux Transformations and Exact Solutions of (2+1) Dimensional Soliton Equations,O175.29
  5. The Existence and Mechanical Algorithm for Elementary Integration of Transcendental Functions,O1-0
  6. Computer Proving of Several Theorem in BCI-Algebra Ideals,TP391.7
  7. Solving Nonlinear Black-Scholes Equation,F224
  8. Nonlinear Waves, Symbolic Integration and Its Application,O241.8
  9. A class of nonlinear wave equations group classification,O245
  10. Some Problems of Nonlinear Dynamic on the Rotor System with Multi-Faults,TH113
  11. The Scale of the Solution Spaces of DEs,O175
  12. Spline function space singularity some triangulation and interpolation posedness,O174.42
  13. Some Problems in Nonlinear Partial Differential Equations’ Exact Solutions,O241.8
  14. AC = BD model and its exact solution of partial differential equations in the application,O241.8
  15. Set theory equation theorem proving systems research and development,TP181
  16. The Application of AC=BD Theory to Solving Differential Equations Mechanically,O241.8
  17. Some Problems in Fractional Differential Equations and Nonlinear Evolution Equations,O241.8
  18. A Constructive Method for Solving Exact Solutions of Some Nonlinear Evolution Equations,O175.29
  19. Symbolic Computation of solitary wave solutions of nonlinear coupled scalar field equations,O411.1
  20. AC = BD Backlund transformation and partial differential equations completeness,O241.8

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer applications > In other aspects of the application
© 2012 www.DissertationTopic.Net  Mobile