Automated Reasoning in Mechanics Using Ritt-wu''s Method
Shang Chou, Xiao Feng Gao · 1989
Methods of automated reasoning in mechanics have been presented and implemented on computers. The paper consists of two parts. In part I, a mechanical method developed by W.T. Wu on the basis of the work of J. F. Ritt has been used to prove theorems in mechanics. In particular, a mechanical study of the complete logical relationship between Kepler''s laws and Newton''s gravitational laws has been given. Wu''s work on the same topic has been extended in several ways. Many other examples from mechanics are also given. In part II, a method of mechanical derivation of formulas from a set of differential polynomials has been presented. The method has been used successfully to some problems in mechanics. In particular, a mechanical derivation of Newton''s gravitational laws from Kepler''s laws has been given without knowing Newton''s Laws in advance.