Formal Kinematic Analysis of Epicyclic Bevel Gear Trains

Epicyclic Bevel Gear Trains (EBGTs) play a vital role in providing highly efficient solutions for power transmissions between shafts in various engineering applications, such as wind turbines and jet airplane engines. The kinematic analysis of EBGTs involves identifying fundamental cycles, and utilizing screw theory to understand the velocities and relative motion of the system’s components. In this paper, we propose to use higher-order-logic theorem proving for the formal kinematic analysis of EBGTs. In particular, we formalize a directed graph representation of EBGT systems, consisting of links and joints (pairs). Next, we formalize a corresponding cycle matrix form of the EBGT in order to analyze fundamental cycles in the graph. Moreover, we formalize the linear and angular velocities of the joint components in the systems using various notions of screw theory, such as screw and twist. We use the above to formally verify the kinematic equations providing a sound relationship between the relative angular joint velocities. In order to illustrate the utility of our proposed formalization, we formally analyze the Bendix wrist, which is a well-known industrial geared mechanism, by providing a verified solution of its kinematic equations.