Bassel Kaddar
email: bassel.kaddar@irccyn.ec-nantes.fr

Yannick Aoustin
email: yannick.aoustin@irccyn.ec-nantes.fr

Christine Chevallereau
email: christine.chevallereau@irccyn.ec-nantes.fr

Arm swing effects on walking bipedal gaits composed of impact, single and double support phases

Keywords: Biped robots, dynamic model, optimal motion, arm swing

In human walking, it is often assumed that the arms have a passive movement which reduces the energy consumption of walking. The issue addressed in this work is the influence of the arms on the walking of a humanoid robot. The study has two objectives: to verify the effect of arms on a sthenic criterion during walking, and to determine whether the optimal movement of the arms is passive or not.

Firstly, we defined optimal cyclic gaits for a biped robot moving in 2D. These gaits are composed of single support phases with a supporting flat foot, double support phases with rotation of the feet and an impact. Different evolutions of arms are studied: bound arms, arms having an active motion and passive arms.

The comparison of our results for different walking speeds show the importance of an active movement of the arms. The part of the sthenic criterion supplied in the joints of arms allows reducing the global sthenic criterion especially for high walking speeds.

A passive movement of the arms will have large amplitude when the natural frequency of the arms coincides with the frequency of the walking gait. Adding springs at the shoulders allows to adjust the natural frequency of the arms to that of walking gait. However, the sthenic criterion with the active arms with or without spring remains less than with the passive arms.

Introduction

Several approaches of upper body motion generation are used to improve the walking of the robot [START_REF] Xing | Arm/trunk motion generation for humanoid robot[END_REF][START_REF] Kajita | Resolved momentum control: humanoid motion planning based on the linear and angular momentum[END_REF][START_REF] Shafii | An optimized gait generator based on fourier series towards fast and robust biped locomotion involving arms swing[END_REF]. Xing and Su generated the movements of the arms during walking by compensating the yaw moment of the robot during the motion [START_REF] Xing | Arm/trunk motion generation for humanoid robot[END_REF]. This upper body motion can stabilize the foot spin for the walking robot. Approaches of generation of the motion of upper limbs from a given reference angular momentum around the center of mass (CoM) have been proposed by Kajita et al. [START_REF] Kajita | Resolved momentum control: humanoid motion planning based on the linear and angular momentum[END_REF]. Shafii et al. [START_REF] Shafii | An optimized gait generator based on fourier series towards fast and robust biped locomotion involving arms swing[END_REF] generated optimal trajectories of a biped robot by using series of Fourier. They found that their model of control is more efficient and produces faster and more stable walk if they consider the influence of the arms of the robot. The study of S. Collins et al. [START_REF] Collins | Dynamic arm swing in human walking[END_REF] allowed to reveal the dynamics of the arms during the walking of a 3D passive biped robot without torso in simulation, but also their utility in the movement. From numerical tests, periodic movements were found through a gradient method. Several modes of arm swing were developed.

• Normal: where each arm oscillates in phase with the leg on the opposite side.

• Bound: the arms are mechanically constrained against rotation. They always remain aligned with the torso.

• Anti-normal: each arm oscillates in phase with the leg on the same side.

• Parallel: during one step both arms swing together. The period of the arm swinging is the stride period.

Thus it has been shown with the numerical tests of S. Collins et al. that passive gaits with arm phasing anti-normal induced a much greater reaction moment from the ground. However these interesting results are obtained with a 3D biped robot the geometrical structure is little far from that of an anthropomorphic bipedal robot with knees and a torso. Few studies and results are available to describe the effects of arms on bipedal walking gaits. The effect of the arms on the energy consumption during a ballistic walk was explored by Aoustin and Formalskii [START_REF] Aoustin | 3D walking biped: optimal swing of the arms[END_REF], who considered cyclic ballistic walking gaits with instantaneous double support phases and impulsive torques in 3D. Torques needed for walking are only applied at the moment of impact. The numerical results show that for a given period of the walking gait step and a length of the step, there is an optimum amplitude of arm swing for which a cost functional is minimum. They also proved that, for any amplitude of arm motion, the energy consumed is less for arms in normal mode than in anti-normal mode. At the instant of the instantaneous double support phase, they numerically proved that the jump of the angular momentum with respect to the vertical axe crossing the stance foot is less for the normal gait than for the anti-normal gait.

In this paper a sthenic criterion is considered. For a robot this criterion represents the energy dissipated by Joule effects in the electrical motors [START_REF] Chevallereau | Bipedal Robots[END_REF]. This criterion leads to the minimization of the maximal torque required and thus allows to choose less powerful actuators. We studied in a previous work, the effect of arm swing on the sthenic criterion during walking of the bipedal planar robot with a flat foot [START_REF] Kaddar | Arms swing effects on a walking planar biped[END_REF] and the effect of passive motion of the arms [START_REF] Kaddar | On passive motion of the arms for a walking planar biped[END_REF]. However, according to our knowledge, it has not been yet shown whether the effect of active or passive movements of the arms can reduce the energy consumption for bipedal walking gaits including double support phases. In this work, we will study the effects of the arms on the sthenic criterion of a planar biped during a walking gait, which is composed of single support phases with flat contact of the stance foot and double support phases with rotation of both feet.

Studies of human walking can provide useful information to improve the humanoid robots. The swinging of the arms is not a purely incidental accompaniment of a forward movement but is an integral part of the dynamics of progression, as shown in [START_REF] Elftman | The function of the arms during walking[END_REF]. It has been shown that the oscillation of the arm reduces the energy costs during human walking [START_REF] Ortega | Effects of aging and arm swing on the metabolic cost of stability in human walking[END_REF][START_REF] Umberger | Effects of suppressing arm swing on kinematics, kinetics, and energetics of human walking[END_REF][START_REF] Collins | Dynamic arm swing in human walking[END_REF]. It is suggested that the high metabolic costs of walking without swinging the arms are either due to the greater momentum around vertical axis that needs to be counteracted [START_REF] Collins | Dynamic arm swing in human walking[END_REF][START_REF] Popovic | Angular momentum regulation during human walking: biomechanics and control[END_REF], either because the oscillations of the arms limit the vertical oscillations of the center of mass [START_REF] Hinrichs | Upper extremity function during treadmill walking[END_REF][START_REF] Umberger | Effects of suppressing arm swing on kinematics, kinetics, and energetics of human walking[END_REF]. Furthermore, several authors argued that the arm swing during human locomotion enhances gait stability [START_REF] Hinrichs | Upper extremity function during treadmill walking[END_REF][START_REF] Ortega | Effects of aging and arm swing on the metabolic cost of stability in human walking[END_REF][START_REF] Bruijn | The effects of arm swing on human gait stability[END_REF]. Collins et al. [START_REF] Collins | Dynamic arm swing in human walking[END_REF] have shown that to swing the arms in anti-normal mode requires the greatest metabolic energy.

The nature of movement of arms is not yet fully understood. Besides, biomechanics do not agree on the passivity of this movement [START_REF] Collins | Dynamic arm swing in human walking[END_REF][START_REF] Pontzer | Control and function of arm swing in human walking and running[END_REF][START_REF] Ballesteros | The pattern of muscular activity during the arm swing of natural walking[END_REF][START_REF] Jackson | A mathematical model of arm swing during human locomotion[END_REF]. For example, Pontzer and al. [START_REF] Pontzer | Control and function of arm swing in human walking and running[END_REF], from the analysis of human walking and running, hypothesize of a passive oscillation of arms. F. Ballesteros et al. [START_REF] Ballesteros | The pattern of muscular activity during the arm swing of natural walking[END_REF], using electrodes to measure muscular activity, show that the motion of the arms is accompanied by the activity of the deltoid muscle, particularly during retraction.

Jackson et al. [START_REF] Jackson | A mathematical model of arm swing during human locomotion[END_REF] make the assumption that the movement of arms is not completely passive. Several experimental measurements on humans show that normal arm swinging requires a minimal shoulder torque, while to hold the arms requires more torque in the shoulder [START_REF] Collins | Dynamic arm swing in human walking[END_REF]. In this work, optimal trajectories are defined for the biped, when the arms are bound to the torso, with a passive motion of arms, and with actuated arms. The sthenic criteria respectively obtained while walking for these three modes are compared.

Cyclic walking gaits are defined with double support phases. Our study has two main goals: the first is to check the effect of the arms on the sthenic criterion during walking. The second is to check the nature of the activation of arms for the optimal gaits and whether the optimal walking requires active or passive movement of the arms.

In order to reach our objective three modes of arm motion are studied:

1. Bound arm mode where the arms are attached to the trunk. Since they are attached the torque useful to keep the desired constant relative position with the torso is not taken into account in the criterion. It is assumed that an external mechanical system is used to maintain the arm held as in the experiments done by S. Collins et al. [START_REF] Collins | Dynamic arm swing in human walking[END_REF]. A simplified model consists to consider only a torso such that its mass and inertia include mass and inertia of the arms.Thus they are an additional charge on the torso.

2.

Active arm swing where the arms are actuated and swing freely in amplitude about the torso.

3.

Passive arm swing where the arms are unactuated and swing freely in amplitude about the torso.

The paper is structured as follows:

The studied robot is presented in Sect 2. The study takes place in the sagittal plane. We use a kinematic structures of biped robot with arms. Starting from this structure, we define a dynamic model of biped for different phases of the walking gait.

In section 3, trajectories of cyclic motion for fully actuated biped are defined. We also define the method to generate passive motion of the arms. Then, the optimization strategy is explained. The results of trajectory optimization for one step in the different cases of the arm motions are shown and arm swing effects are discussed in Sect 4. Section 5 presents our conclusion and perspectives.

The biped modeling in 2D

This section is devoted to the development of the model of the biped robot, its generalized coordinates, the different geometrical structures with active or bound arms, and its model. This model will be used for the generation of optimal movements presented in Sect 3.

Presentation of the biped

As most of the movements are in the sagittal plan during walking, our study is based on a 2D biped, see Fig. 1. Its physical parameters are derived from the humanoid robot HYDROÏD (HYDraulic andROÏD). It is a 3D biped, which was built through the cooperation of several french laboratories and an industrial partner, supported by the French national agency of research, ANR, see [START_REF] Alfayad | Robot humanoïde hydroïd : Actionnement, structure cinématique et stratégie de contrôle[END_REF]. It is equipped with hydraulic actuators. The size of HYDROÏD is 1.40 m, its mass is 45 kg. It has 30 degrees of freedom. Its locomotor system has 16 degrees of freedom (three for each hip, one for each knee, three for each ankle and one for the toe of each foot). It is designed to have geometrical and dynamical parameters close to those of the model of Hanavan established to characterize the human body. To determine the behavior of the biped during different phases, we are going to define the dynamic model of the biped robot for each phase of the studied walking gait. From HYDROÏD we keep only the joints that produce movements in the sagittal plane. The mechanical system is a nine-link bipedal robot composed of two identical legs, two identical one-link arms and a torso. Each leg consists of a femur, a tibia, and a rigid foot. Each arm is composed of one link only. The trunk and the head form a single body too. Table 1 gathers the physical parameters of the biped. From [START_REF] Tilley | The measure of man and woman, human factors in design[END_REF], we can observe that the geometrical parameters are close to the dimensions of an occidental subject, who is 15 years old.

Definition of studied cyclic gait

The cyclic walking gait is composed of single support phases, double support phases and impacts as shown in Fig. 3. Let us consider the current step starting with a double support phase where the front foot (foot 1) and the rear foot (foot 2) are in contact with the ground respectively with the heel and the toe. Both feet rotate until there is an impact on the ground of the toe of the front foot (toe impact). At this instant the rear foot takes off. The single support phase starts on the stance foot 1. This phase is ended with the impactless landing of the heel of foot 2, i.e. the velocity of the heel is equal to zero at the landing.

Modeling

The generalized coordinates are described with the vector

x = [x h y h q p1 q p2 q 1 • • • q n-1 ] ⊤ = [x h y h q ⊤ ] ⊤ ,
where n = 6 or 8 depending on the biped with free or bound arms.

Γ = [Γ 1 Γ 2 • • • Γ n ]
⊤ is the joint torque vector. The dynamic model of the biped robot is:

Dẍ + N(x, ẋ) + Q = BΓ + J ⊤ 1 r 1 + J ⊤ 2 r 2 (1)
with the constraint equations to define the contact between the stance foot i and the ground:

J i ẍ + Ji ẋ = 0 for i = 1 to 2. (2)
Here D(x) ∈ R (n+3)×(n+3) is a positive definitive inertia matrix, N(x, ẋ) ∈ R n+3 contains the Coriolis and centrifugal forces, Q(x) ∈ R n+3 is the vector of gravity forces, and B ∈ R (n+3)×(n) is the actuation matrix which is constant. For the studied walking gaits the contact with the ground of the biped's feet can be with the whole sole, the heel of the toe. Vector r i = [r ix , r iy ] ⊤ (respectively r i = [r ix , r iy , m z ] ⊤ with a contact of the whole sole) defines the effort (respectively the force and moment with a contact of the whole sole) of the ground reaction acting on foot i and J i is the Jacobian matrix of foot i, i = 1, 2.

In double support, the bipedal robot is in contact with the ground on the heel of the front leg as well as on the toe of the rear foot such that the contact between each foot and the ground is punctual, see Fig 4 . For a given movement of the biped, there are n + 4 unknown variables, i.e. n torques and 4 components of the ground reactions, which are solutions of the inverse dynamic model ( 1), composed of n + 3 scalar equations. Then one variable can be chosen as a parameter among the set of these n + 4 unknown variables for a given movement. This choice, useful for the definition of a cyclic trajectory, is detailed in Appendix A.

Impact

We observed numerically in previous work [START_REF] Kaddar | Effet du balancement des bras sur la consommation énergétique durant la marche d'un robot bipède[END_REF] that to obtain the cyclic walking gaits, which are composed of double and single supports, the velocity of the swing foot landing on its heel, at the end of the single support, has to be zero. Otherwise it is not possible to obtain a double support phase satisfying the unilateral constraints. Therefore, a zero velocity of the landing is considered when the swing leg touches the ground with its heel just before the double support phase. An impact occurs when toe of the front foot touches the ground at the end of phase of double support. The front foot (foot 1) remains on the ground in flat contact, to be the stance foot for the next single support phase. The velocity of the foot 1 just after impact is zero.

The joint configurations are continuous at the impact, while the joint velocities are discontinuous [START_REF] Bausset | Mécanique des systèmes de solides : avec modèles et exercices[END_REF]. The impact model is used to determine the velocities after impact, as well as the impulsive forces, according to the velocities and positions which are known before the impact. The impact model is given by:

D(x(T ds ))( ẋ+ -ẋ-) = J ⊤ 1 I 1 (3)
Here, ẋ-and ẋ+ are the joint velocity vectors just before and after impact respectively. I 1 ∈ R 3×1 represents the impulsive ground reaction wrench on the stance foot at toe impact. Matrix J 1 ∈ R (n+3)× (3) is the Jacobian matrix to take into account the constraints of no take off and no rotation of the landing foot (the ground reaction efforts are composed of an impulsive force and an impulsive moment).

To ensure a flat foot contact on the ground, the velocity of the sole of the front leg just after impact must be zero. This constraint is expressed as:

J 1 ẋ+ = 0 (4)
Finally, to calculate the joint velocities just after impact and the impulsive wrench on front foot, we have:

D -J ⊤ 1 J 1 0 ẋ+ I 1 = D ẋ- 0 (5)
3. Description of the joint motion

Generation of cyclic walking gaits

For a cyclic walking gait, all steps are identical. Then we only study one step. The swing leg at the end of a step becomes the stance leg for the next step. The duration T of one walking step is:

T = T ds + T ss (6)
T ds corresponds to the duration of the double support phase and T ss corresponds to the duration of the single support phase.

Let us note that the heel of the stance foot in single support, never takes off from the ground during one step, see figure 3. This heel can be considered as the biped's base during the step and then x h and y h depend on the angular variable of the stance leg. As a consequence, the reference motion is defined using the joint variables q only. In our study the joint evolution will be expressed as a polynomial functions of third order:

q j = a 0 + a 1 t + a 2 t 2 + a 3 t 3 j = 1, • • • , n + 1 (7)
To determine the four coefficients of the polynomial functions [START_REF] Kaddar | Arms swing effects on a walking planar biped[END_REF], four boundary conditions are used in each phase which are the initial and final values of q j and qj .

Motions with active motion of the arms

To define a movement it is necessary to determine the four coefficients of all polynomial functions [START_REF] Kaddar | Arms swing effects on a walking planar biped[END_REF] for the double and single support phases. The number of variables for these two phases is 2 × (4 × 9) = 72 unknown variables. However it is possible to reduce this number by taking into account the characteristics of the desired walking gait such as the impact model, the continuity properties between the single phase and the double support phase. This point is detailed as following.

Let us consider the beginning of the double support, t = 0. The locomotor system and the ground form a closed geometrical structure. One foot touches the ground with its heel, while the other foot has a flat contact. Its means that if the distance between both feet are given, only six generalized coordinates among the nine components of q(0) and six angular velocities among the nine components of q(0) are independent. During the double support both feet rotates on the ground, one with its heel and the other with its toe. The double support is ended at t = T ds by an impact on the ground of the foot, which rotates with its heel. At this instant the orientation of its sole with respect to the ground is null but its angular velocity does not equal zero. As a consequence the continuity in position and the impact model allows us to consider only six generalized coordinates among the nine components of q(T ds ) and seven angular velocities among the nine components of q(T ds ), i.e. just before the impact. Through the continuity and cyclicity properties, the exchange of the role of both legs makes the correspondence between the states of the biped at t = T and t = 0. As a consequence, it is possible to reduce the number of unknown variables from 72 to 26 angular positions and velocities in addition to the distance between the two feet in double support phase. These 27 unknown variables will be the optimization variables and are gathered in Table 2.

Motions with passive motion of the arms

We are looking here for the optimal cyclic walking with passive motion of the upper links of the biped. Only the locomotor system (legs and trunk) of the biped is actuated. Variables of the locomotor system q l can then be defined as in Sect 3.1.1 where the index "l" refers to the lower parts of the biped robot x l = [x h y h q p1 q p2 q 1 q 2 q 3 q 4 q 5 ] ⊤ . The variables of arms x u are not actuated and their motion are due to dynamics of the locomotor system, where the index "u" refers to the upper parts of the biped robot,

x u = [q 6 q 7 ] ⊤ , such as x = [x ⊤ l , x ⊤ u ] ⊤ .
Since the actuated variables are expressed as chosen polynomial function, we can imposed the continuity conditions between x(0) and x(t) to produce a cyclic motion. For the passive joints we cannot define a priori a cyclic motion. The motion of these passive joints are due to the dynamic of the locomoteur system. Periodic motion of the arms can be only obtained through equality constraints.

We look for the passive motion of the arms, due to the dynamic of the actuated locomotor system during a walking gait. Hence, we present here the equations to obtain this motion. No torques are applied to the arm joints. The matrix equation (1) of the biped robot can be rewritten:

D ll D lu D ul D uu ẍl ẍu + H l H u = B l Γ l 0 2×1 + J ⊤ 1 r 1 + J ⊤ 2 r 2 (8)
where H = N(q, q) ẋ + Q(q), ẍu ∈ R 2×1 is the accelerations vector of the upper parts of the biped,

D uu ∈ R 2×2 , D lu ∈ R 9×2 , D ul ∈ R 2×9 and D uu ∈ R 2×2 , H u ∈ R 2×1 and H l ∈ R 9×1 are subvectors of H. B l ∈ R 9×6 is the actuation matrix. Γ l ∈ R 6×1
is the joint torque vector of the locomotor system of the biped. Vector 0 2×1 corresponds to the assumption that no torque is exerted on the two shoulders since arm motion is passive.

The cyclic passive trajectories of the arms can be determined through the numerical resolution of:

ẍu = D -1 uu (-D ul ẍl -H u + W u ), (9)
with vector W u is composed of the two last components of J ⊤ 1 r 1 + J ⊤ 2 r 2 . Periodic motion is obtained for appropriate initial values of angular configurations and velocities of the arms. The computation of these initial values is now detailed.

Trajectories of the locomotor system x l (t), ẋl (t), ẍl (t) during the double support phase are generated by polynomial functions of third order. Thus, trajectory of each joint is defined by four boundary conditions, see Sect. 3.1.1.

Once the values x u (0), ẋu (0) are found, the integration to find x u (t) becomes possible by using a numerical resolution of [START_REF] Elftman | The function of the arms during walking[END_REF]. Now, trajectories are completely known during the double support phase, including the values at the end of this phase. After "toe impact", initial values of the single support phase (x(T ds ) and ẋ(T ds ) + ) are known by using the continuity condition and solving the impact model. Trajectories of the locomotor system during the single support phase can be calculated. It can be noted that the motion of arms affects the state of the locomoteur system after impact due to the coupling between the legs and the arms existing in impact model.

In the same way, these trajectories are used to find the passive motion of arms during the single support phase by the numerical resolution of (9). We thus obtain the joint variables x u (T ) and velocities ẋu (T ) of the arms at the end of the single support phase.

The desired arm passive motion is cyclic with a period which is the same as that of the locomotor system. By taking into account the exchange on the role of arms between final time of a step (t = T) and initial time of the following step (t = 0), the following equalities must be respected:

ẋu (0) = 0 1 1 0 ẋu (T ) and x u (0) = 0 1 1 0 x u (T ) (10)
To generate the passive movement of the arms, it is necessary to find the arm trajectories x u (t) such that the conditions given by (10) are satisfied.

Trajectory optimization

In the parametric optimization problem, a reference trajectory for a walking step of biped is obtained with the minimization of a criterion under constraints. A sthenic criterion is used for a given distance d to travel during one step of duration T .

C Γ = 1 d T 0 Γ ⊤ Γdt (11)
under nonlinear constraints and bounded conditions:

c(x) ≤ 0, cex(x) = 0 lb ≤ x ≤ ub (12)
The constraints are defined in the following section.

The optimization constraints

In order to ensure that the biped will successfully walk and that the trajectory is feasible, a number of constraints must be satisfied.

Constraints of contact with the ground:

• A foot i in contact must stay on the ground without taking-off neither slipping during various phases and the impact. To insure the contact, the following equalities must be satisfied:

µr iy ≥ |r ix | µI r iy ≥ |I r ix | (13)
where r iy is the vertical component of the reaction forces on the foot i in contact with the ground, µ is the coefficient of friction and I r ix , I r iy are the vertical and tangential components of ground reaction of the foot i in contact with the ground at the impact.

• The Zero Moment Point (ZMP) of the biped's stance foot must be inside the support polygon [START_REF] Kajita | Introduction to humanoid robotics[END_REF][START_REF] Chevallereau | Bipedal Robots[END_REF].

-l p ≤ ZMP x ≤ l d (14)
The Condition of ZMP must be verified during the single support phase and at the impact. In double support phase, if the constraint ( 13) is satisfied for each foot, the biped's balance is insured. Thus the ZMP is implicitly inside the polygon support defined by the two points of contacts belonging to the two feet.

• The heel and toe velocities of the foot 2 leaving the ground just after impact of the toe of foot 1 must be positive to ensure the take-off.

V heel ≥ 0 V toe ≥ 0 (15)
2. Geometric constraints:

The swing foot 2 must not touch the ground during the single support phase, i.e. the vertical position of swing foot heel and toe must be positive.

y heel > 0 y toe > 0 (16)
where y heel and y toe are respectively the vertical distances of the heel and toe of the swinging foot during single support phase.

3. Technological constraints: These constraints consist of physical limitations of the biped's actuators and joints. The constraints on joints position, velocity and torque are:

|Γ i | -Γ i,max ≤ 0, for i = 1, ..., n | qi | -qi,max ≤ 0, for i = 1, ..., n (17)
where n = 6 or 8 depending on if the arms are actuated or not, Γ i,max denotes the maximum value of torque for each actuator and qi,max represents the maximum value of velocity for each actuator.

The upper and lower bounds of joints for the configurations during the motion are: q i,min ≤ q i ≤ q i,max , for i = 1, ..., n.

where q i,min and q i,max are the minimum and maximum joint configuration limits respectively.

In the case of a passive motion of the arms, [START_REF] Ortega | Effects of aging and arm swing on the metabolic cost of stability in human walking[END_REF] are used in addition to all the previous constraints.

The optimization variables

The walking speed V is fixed for each optimization procedure. By considering the step length d as a parameter of optimization, the step duration T is then calculated from T = d/V . With the ratio T ds /T as a variable of optimization, T ds can be obtained.

The optimization variables to define an optimal walking gait is presented in Table 2. With these optimization variables, the impact equations, the boundary conditions between the double support phase and the single support phase, the coefficients of ( 7) can be calculated.

Optimization

Active Bound Passive Instant variables arms arms arms q q P 2 , q 1 , q 2 , q P 2 , q 1 , q 2 , q 3 q P 2 , q 1 , q 2 , q 3 T ds q 3 , q 6 , q 7 q qP 1 , qP 2 , q1 , qP 1 , qP 2 , q1 , qP 1 , qP 2 , q1 , T ds q2 , q3 , q6 , q7 q2 , q3 q2 , q3 q q P 2 , q 1 , q 2 , q P 2 , q 1 , q 2 , q 3 q P 2 , q 1 , q 2 , q 3 T q 3 , q 6 , q 7 q qP 2 , q1 , q2 , qP 2 , q1 , q2 , q3 qP In the following, we present the different types of arm motion and then we illustrate the results of trajectories optimization for the different evolutions of the arms.

Optimal walk

Optimal gaits are defined for several speeds and for different modes.

Active motion of the arms and bound arm mode

• Active motion of the arms:

An optimal walking gait at V = 1 m/s is shown in Fig. 4, where the maximal absolute values of q 6 and q 7 are fixed to q 6,max = 60 o . The arms can have a very large amplitude of swinging if they are not constrained. • Bound arm mode: Fig. 5 shows walking gait obtained at walking speed 1 m/s. Several values of the criterion are shown as function of the walking speed in Fig. 6. Numerical results show that the arm swing reduces the criterion cost during its walking. It is interesting to note that an optimal walking with arm swing can be obtained for higher walking speeds until 2.1m/s. An optimal motion of biped without arms cannot be obtained for a walking speed above 1.65 m/s.

The profiles of the joint torques are shown on two steps and for a walking speed V = 1 m/s, see Fig. 7. The torques during the double support phase are higher than those during single support.

The numerical results show that for active arms, the value of the sthenic criterion is lower than for bound arms for any motion velocity speed. We recall here that for bound arms, the torque required to maintain the arm are not included since there are assumed to be produced by external mechanical device. The active arms allow to reduce the torques in the locomotor system. Figure 8 shows the evolutions of articular configurations of the bipedal robot with bound and active arms respectively. They are quite similar in shape as function of time and with small difference in amplitude. Absolute angles shown in Fig. 9 b,are used in figure 8 to allow a comparison of the optimal motions of biped with the curves of Fig. 9 a. Barliya and al. [START_REF] Barliya | An analytical formulation of the law of intersegmental coordination during human locomotion[END_REF], which illustrate the absolute angles of human walking gaits. Between the biped and human several similarities in shape and amplitude of the absolute angles can be observed. Concerning the leg 1, the angle α is equal to q 2 in stance phase and to q 4 in phase of transfer. The angle β = q 1 or q 5 depending on whether the phase is the stance phase or transfer phase respectively. To calculate the angle of the foot 1, we have γ = π 2 + q p2 in phase of transfer and γ = π 2 in stance phase (Fig. 9 b). Step 1

Step 2 Joint configurations of the arms versus time at walking speed V = 1 m/s are illustrated in Fig. 10. The shape of the amplitude profile of the arm swing for both arms is not exactly symmetric with respect to the origin of the y-axis. It is probably due to dynamic coupling between the active arms and the torso with a forward inclination. Step 1

Step 2

Passive motion of the arms

We note that in the previous study, torques are not zero in arm joints for the optimal motions. We used polynomial expression to define the evolution of arms versus time. This representation can be unsuitable for a correct modeling of a passive movement. We are looking here for optimal trajectories with passive movements of the arms. Numerical results show that no passive motion with large amplitude of arms oscillation is possible for the initial design of the robot. All arm motions have small amplitude for all walking speeds. This can be explained by an inadequate choice of the step duration with respect to the natural frequency of the arm. The duration of walking stride 2T does not correspond to the natural period T o of the oscillation of arms.

If the biped arm is considered as a simple pendulum suspended from a frictionless pivot as in Fig. 11, its model is:

I s θ + mgl sin(θ) = 0, (19)
where I s = I + ml 2 is the moment of inertia around the suspension point. For small oscillations, sin(θ) ≈ θ, the natural period of the pendulum T o is:

T o = 2π w o = 2π I s /(mgl) (20)
It depends on the mass, length, and inertia. We can change the natural period of arm oscillations by using torsion springs placed in the shoulders. In this case, the dynamic model of the pendulum becomes:

I s θ + mgl sinθ + kθ = 0, (21)
where k is the stiffness of the springs. The natural period of arm oscillations becomes:

T o = 2π w o = 2π I s /(mgl + k). (22)
We conducted a scan of the possible passive motions of the arms according to the value of the spring stiffness k. Starting from optimal variables corresponding to an optimal solution we looked for the possible passive movement of the arms at each given value of the spring stiffness k. This stiffness coefficient k is involved in the set of the optimization variables. Both sthenic criterion and maximal amplitude between the arms are plotted as a function of k in figure 12) for a walking speed V = 1.0 m/s. And then from the Fig. 12 we can numerically observe that it is possible to obtain a large amplitude passive movement of arms through a spring with a stiffness coefficient k = 4.8 N.m/rad, which corresponds to the first amplitude peak, with a minimal value of the sthenic criterion. In this case, the natural period of the arm is given with [START_REF] Kajita | Introduction to humanoid robotics[END_REF] is such that T o1 = 2T . The peaks of the evolution of the maximum amplitude of q 6 , which correspond to the stiffness coefficients T o1 , T o2 , T o3 , • • • , T on , T o(n+1) . These natural periods of the oscillations of the arms are related to the stride duration of walking gait 2T as follow:

k 1 , k 2 , k 3 , , • • • , k n , k n+1 ,
2T = T o1 2T = 2T o2 2T = 3T o3 . . . 2T = nT on 2T = (n + 1)T o(n+1) (23)
A passive motion with a large amplitude is possible if and only if the period 2T of walking stride (two steps) is close enough to a multiple of the natural period T o of arms oscillation. The odd coefficients correspond to opposite phase movements of both arms. While for even coefficients, both arms swing in phase with large oscillations. For walking speeds higher than 1.0 m/s, large amplitude oscillations of arms are obtained only to the even coefficients. For walking speeds lower or equal to 1.2 m/s, opposite phase movements are also achievable.

This observation offers an analogy with the human walking gait. Wagenaar et al. [START_REF] Wagenaar | Resonant frequencies of arms and legs identify different walking patterns[END_REF] shown experimentally with young healthy subjects, that for velocities between 0.3 -0.8 m/s the frequency of the arm swing synchronizes with the frequency of one step. For higher velocities the frequency of the arm swing corresponds to those of two steps.

Figures 13 and14, propose also a comparaison between passive and active swings of the arms when a spring is added in the shoulders. The main information, which can be claimed from these figures is that for our bipedal robot the active movement of the swing arm leads to lower values of the sthenic criterion than the passive motion of arm. Optimal stiffness coefficients are close for passive or active arm motions. For the walking speed V = 1 m/s, the evolutions of joint torques during a walking stride are illustrated in Fig. 16. The maximal amplitude of the oscillations of arms with respect to the vertical axis is reached at the end of the single support phase. It is coherent with the human walking, when the arm movement frequencies are synchronized with the step frequency, see [START_REF] Elftman | The function of the arms during walking[END_REF], [START_REF] Wagenaar | Resonant frequencies of arms and legs identify different walking patterns[END_REF], and [START_REF] Freedland | Developmental changes in interlimb coordination: Transition to hands-and-knees crawling[END_REF]. For the walking speed V = 1 m/s, the absolute angles of legs and the evolution of arm joints versus time are illustrated in Fig. 17

Comparaison and Discussion

The biped trajectories are optimized for all cases of arms modes, i.e. bound arm mode, active arm swing with spring or without spring, and passive arm swing. These cases are compared according to the sthenic criterion in figure 18. The performances obtained with passive arm swing and bound arm mode are very close. If we consider the effort to maintain arm, we can says that the passive arm swing is better than bound arm mode. The lowest values of the criterion is obtained with the active arm swing with spring. Then for our biped, with the optimal walking gaits and the considered we can say that the optimal motion is obtained with an active arm swing (with or without spring because both cases are close). This observation could support the idea that the arm swing of humain is not passive, even if the modeling of our biped is far from the complex dynamics of human. Step 1

Step 2 When arm joints are actuated, the criterion value is lower than in the case of passive arms. Furthermore, the values of the criterion in the case of the active arms are lower with regard to arms bound case for all walking speeds.

We can conclude that the optimal motion of the arms is not passive and that the actuation of the arms reduces the torques needed in the actuators on the other joints of the biped and therefore less value of criterion will be required.

Conclusion and perspectives

For optimal walking gaits, three cases of the biped arms are compared: bound arm mode, active arm swing and passive arm swing. For all given walking speeds, the sthenic criterion when the actuated arms swing is lower than that when the biped has the bound arms. The actuation of the arms reduces the torques required in the other joints of the biped and therefore a less value of criterion is obtained. Optimal motion of the arms requires torques in arm joints especially during the double support phase. This is coherent with the studies on human walking, which suppose that the arm swinging is not a passive movement and that the deltoid muscles are active during walking [START_REF] Jackson | A mathematical model of arm swing during human locomotion[END_REF][START_REF] Donker | Adaptations in arm movements for added mass to wrist or ankle during walking[END_REF].

Yet, polynomial functions were used to obtain joint evolution including arm evolution. This representation can be unsuitable to model correctly a passive movement. Therefore, we explored passive arms movements of the biped due to the dynamics of the locomotor system. Only the locomotor system of the biped was actuated. Numerical results showed that trajectories with passive movements of arms have higher values of the sthenic criterion than trajectories where shoulders are actuated.

The effects of springs placed in shoulders on the natural period of oscillation of arms were explored on the passive and active movements of the arms. Solutions including movements with large amplitudes of arms exist if the duration of walking stride corresponds to the natural period of oscillation of arms. Both passive or active arms swing together according to the stiffness of springs.

We assumed that the stance foot stay on the ground with a flat foot during the single support phase. Our perspectives are to consider a sub-phase in single support with partial contact on the stance foot and to design running gait as in [START_REF] Chevallereau | Optimal reference trajectories for walking and running of a biped robot[END_REF], especially to observe if the effect of arms on the sthenic criterion augments when the walking speed increases.

The expression of C *

Γ can be written as:

C * Γ = Γ ⊤ Γ = F 1 ⊤ F 1 + 2F 1 ⊤ F 2 r 2x + F 2 ⊤ F 2 r 2 2x (A.6)
Term F 2 ⊤ F 2 being strictly positive, then C * Γ as function of r 2x has a minimum. The value r 2x which allows to minimize C * Γ can be calculated by writing that the derivative of C * Γ with regard to r 2x is equal to zero.

∂C * Γ ∂r 2x = 0 => 2F 1 ⊤ F 2 + 2F 2 ⊤ F 2 r 2x opt Γ = 0 r 2x opt Γ = -(F 2 ⊤ F 2 ) -1 F 1 ⊤ F 2 (A.7)
The solution r 2x , found with (A.7), minimizes C * Γ without constraints. Having calculated r 2x , we can use (A.3) and (A.1) to calculate r 2y and r 1 respectively. These reaction forces will be used to calculate and to impose constraints of no-slipping and no-take-off [START_REF] Kaddar | Effet du balancement des bras sur la consommation énergétique durant la marche d'un robot bipède[END_REF]. If the constraints of friction are not verified by algorithm, we choose r 2x to be as close as possible to the optimal value [START_REF] Miossec | A simplified stability study for a biped walk with underactuated and overactuated phases[END_REF].

Figure 1 :

 1 Figure 1: Planar biped: generalized coordinates representation and applied torques.

Figure 2 :

 2 Figure 2: Details of the foot.

Figure 3 :

 3 Figure 3: Walking gait

Figure 4 :

 4 Figure 4: Walking gait of biped with arms during one step for walking speed V = 1 m/s; q 6,max = 60 o .

Figure 5 :

 5 Figure 5: Walking gait of biped without arms during one step for walking speed V = 1 m/s.

Figure 6 :

 6 Figure 6: Evolution of sthenic criterion versus walking speed

Figure 7 :

 7 Figure 7: Evolutions of joint torques during two steps for a walking speed V = 1 m/s.

Figure 8 :

 8 Figure 8: Evolutions of the articular configurations of the biped during four steps of walking at V = 1 m/s.

Figure 9 :

 9 Figure 9: Characteristics of human walking gaits used by A. Barliya and al. [23]. Absolute angles for human of thigh, shank and foot are plotted in solid lines. Three harmonics of Fourier series are plotted for each segment with dashed lines [23].

Figure 10 :

 10 Figure 10: Evolution of arms versus time at walking speed V = 1 m/s

Figure 11 :

 11 Figure 11: Simple pendulum

  represent different natural periods of arm oscillations

Figure 12 :

 12 Figure12: The evolutions of the sthenic criterion and the maximum amplitude q 6 as a function of k at walking speed V = 1.0 m/s.

Figure 13 :

 13 Figure 13: Sthenic criterion as function of the velocity for active and passive swings of the arms.

Figure 14 :

 14 Figure 14: Stiffness coefficient k as a function of the velocity: for values of k less than 10 N.m/rad the arms swing in opposite phase, for higher values of k and a velocity greater than 1.1 m/s they swing in phase (parallel mode).

Figure 15

 15 Figure 15 illustrates an optimal walking gait with passive motion of the arms at walking speed V = 1 m/s, (k = 4.8 N.m/rad).

Figure 15 :

 15 Figure 15: Optimal walking gait at walking speed V = 1 m/s

Figure 16 :

 16 Figure 16: Evolutions of joint torques during a walking stride (two steps) at walking speed V = 1 m/s.

  .

Figure 17 :

 17 Figure 17: Evolutions of variables versus time at walking speed V = 1 m/s.

Figure 18 :

 18 Figure 18: Evolution of sthenic criterion versus walking speed.

Table 1 :

 1 Physical parameters of the robot,[START_REF] Tilley | The measure of man and woman, human factors in design[END_REF].

		Mass	Length	Center of	Inertia
		Kg	m	mass m	Kg.m 2
	Foot 0.678 L p =0.207	sp x = 0.0135 0.00175
			h p =0.06425 sp y = 0.03212
			l p =0.072
	Tibia 2.188	0.392	0.1685	0.0276
	Femur 5.025	0.392	0.1685	0.0664
	Trunk 24.97	0.5428	0.2013	0.6848
	Arm	2.15	0.586	0.2418	0.0578

Table 2 :

 2 Optimization variables

Appendix A. Calculation of r 2x

In double support phase the biped is in contact with the ground through the heel of the front foot and the toe of the rear foot for a given reference trajectory, the inverse dynamic model (1) has n+3 scalar equations and n+4 unknown variables, i.e. n torques and the four components r 1x , r 1yx , r 2x , and r 2y of both ground reaction forces. Then among the set of these unknown variables, one variable can be chosen as an optimization variable during the double support phase. To choose this optimization variable let us consider the global equilibrium about the center of mass of the biped, written in translation and rotation. In double support phase with contacts of the heel of the front foot and the toe of the rear foot (Fig. A.19), the following equations are obtained:

Where m is the biped's mass, ẍg and ÿg represent the tangential and horizontal components of acceleration of CoM of the biped, r 1 and r 2 are the ground reaction acting in the front hell and the rear toe and γ g is the time derivative of the angular momentum of the biped with respect to its center of mass.

The system of equations (A.1) has three equations for four unknown variables. For a given reference trajectory mẍ g is known, and then the sum r 1x + r 2x through the second equation of (A.1). Consequently r 1y and r 2y are the unique solution of the first and third equations of (A.1). It means that in double support, for the same movement, several solutions for r 1x or r 2x are possible as functions of torques. Then r 1x or r 2x can be used as a optimization variable.

The reaction r 2x is selected to minimize the optimization criterion. To calculate r 2x , the dynamic equation will be solved in such a way as r 2x is going to minimize the criterion of optimization based on the torques C * Γ taking into account the constraint that reaction forces of the ground r 1 and r 2 are compatible with the assumed contact; that is to say without taking off nor sliding.

When r 2x is known, the reaction of the ground r 1 on the front foot can be found.

Besides, joint torques as well as the vertical component of ground reaction force on rear foot can be calculated through the orthogonal matrix J ⊥ 1 (6×(n+3)), such that left multiplying it by (1) we obtain:

Where J ⊤ 2(:,1) defines the first column of the matrix J ⊤ 2 . We can thus obtain the components of the reaction of the ground on the foot 1 with (A.3).

Considering that the left-hand side of ( 1) is calculated from the desired movement. It is noted φ such that:

We can get:

Where

] -1 J ⊤ 2(:,1) ) (1:n) .


Pierre Halmagrand
email: pierre.halmagrand@inria.fr

Using Deduction Modulo in Set Theory

Keywords: Automated Theorem Proving, Tableaux, Deduction Modulo, Rewriting, Set Theory, B Method, Zenon Modulo

We present some improvements of Zenon Modulo and the application of this tool to sets of problems coming from set theory. Zenon Modulo is an extension of the tableau-based first order automated theorem prover Zenon to deduction modulo. Deduction modulo is an extension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well-suited for proof-search in axiomatic theories, as it turns axioms into rewrite rules. The improvements discussed here consist in a better heuristic to automatically build rewrite systems given a set of axioms, and some optimizations in the rewriting process used during the proof search. We also present some updated results obtained on benchmarks provided by the TPTP library for set theory categories. Finally, we discuss some recent work about the application of our tool to the B method set theory, in particular the way we treat equality and the comprehension scheme.

Introduction

The development of large-scale industrial projects based on formal software is constrained by the efficiency of verification tools that themselves rely on automated theorem provers to mechanize a maximal part of the formalization process. Therefore, to allow a wider dissemination of these techniques, a particular attention must be paid to the development of automated theorem prover. Since many formal developments may be based on specific theories, like the widely used B method [START_REF] Halmagrand | The B-Book, Assigning Programs to Meanings[END_REF] which relies on a particular typed set theory, we must pay attention to reason within axiomatic theories. A solution to improve verification tools is to combine different approaches in automated deduction and specialize them for a specific theory, like SMT solvers.

The BWare project [START_REF]The BWare Project[END_REF] aims to provide a generic platform relying on different theorem provers (first order provers and SMT solvers) to verify proof obligations coming from the development of industrial applications using the B method.

As part of this project, the development of Zenon Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF] is driven by its application to set theory.

Our approach is to extend the tableau-based first order automated theorem prover Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] to deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF]. Deduction modulo is an extension of predicate calculus, which allows to rewrite terms as well as propositions. This is well suited for proof-search in axiomatic theories, as it turns axioms into rewrite rules. For instance, we can express Zermelo set theory without any axiom [START_REF] Dowek | Cut Elimination for Zermelo Set Theory[END_REF], and turn non-deterministic proof-search among axioms into computations, which reduces the proof-search space. Moreover, Zenon Modulo, like Zenon, adopts a certifying approach and produces proof certificates that can be checked by external proof checkers. Since the proofs produced by Zenon Modulo should keep the advantage of conciseness of deduction modulo, we do not want to record all the computational steps of rewriting [START_REF] Delahaye | Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps[END_REF]. As a result, in order to verify such proofs, we use Dedukti [START_REF] Boespflug | The λΠ-Calculus Modulo as a Universal Proof Language[END_REF], a simple proof checker based on the λΠ-calculus modulo which can deal with rewriting.

We also present an updated heuristic, used by Zenon Modulo to automatically transform axioms into rewrite rules. The new heuristic captures more axioms and guarantees to have a more meaningful rewrite system and impacts both rewrite rules over terms and over propositions. We should notice here that this heuristic has been developed to be used as a preprocessing tool that allows a fully automatic use of Zenon Modulo on problems in the TPTP format. A second option is to give manually the rewrite system to Zenon Modulo. This second option is the one chosen for the B method set theory since there is a limited number of axioms and definitions, and we can afford to design a customized rewrite system.

To assess our approach, we apply this new heuristic to the SET and SEU categories of the first-order problems of the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF] which deal with set theory, and compare results obtained by Zenon and Zenon Modulo with both heuristics. In particular, we exhibit some examples of difficult problems that can be proved by our tool using the new heuristic.

Finally, we discuss the application of Zenon Modulo to the B method set theory [START_REF] Halmagrand | The B-Book, Assigning Programs to Meanings[END_REF]. We will especially focus on equality and the comprehension scheme in first order logic. This paper is organized as follows: in Sec. 2, we first introduce the basic notions of deduction modulo and its application to Zenon Modulo; we then present in Sec. 3 the new heuristic for Zenon Modulo; we expose in Sec. 4 the experimental results obtained on the benchmarks provided by the TPTP library; finally, in Sec. 5, we discuss the ongoing work on the B set theory.

Zenon with Deduction Modulo

Zenon Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF] is an extension of the tableau-based first order automated theorem prover Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] to deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF]. This extension is partially inspired by the presentation of tableaux modulo in [START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF]. The proof-search rules are applied with the usual tableau method: starting from the negation of the goal, apply the rules in a top-down fashion to build a tree. When all branches can be closed by applying a closure rule, the tree itself is said closed, and this closed tree is a proof of the goal.

Deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] extends the predicate calculus by introducing a congruence relation over propositions and the ability to perform conversion between propositions that are equivalent modulo the congruence. Given a set of axioms, the congruence is generated by the rewrite system coming from the transformation of axioms into rewrite rules. One of the major interests of deduction modulo lies in reasoning modulo this congruence, since it reduces the search space by removal of axioms from the context. For example, considering the following definition of inclusion in set theory:

∀X, Y (X ⊆ Y ⇔ ∀x (x ∈ X ⇒ x ∈ Y ))
The proof of A ⊆ A produced by Zenon has the following shape:

¬(A ⊆ A), ∀X, Y (X ⊆ Y ⇔ ∀x (x ∈ X ⇒ x ∈ Y )) γ ∀inst ∀Y (A ⊆ Y ⇔ ∀x (x ∈ A ⇒ x ∈ Y )) γ ∀inst A ⊆ A ⇔ ∀x (x ∈ A ⇒ x ∈ A) β ⇔ ¬∀x (x ∈ A ⇒ x ∈ A) δ ¬∀ ¬(τ ∈ A ⇒ τ ∈ A) α ¬⇒ τ ∈ A, ¬(τ ∈ A) A ⊆ A where τ = x.¬(x ∈ A ⇒ x ∈ A
) is a Hilbert epsilon-term formed with a variable x and the formula ¬(x ∈ A ⇒ x ∈ A), which is the formula existentially quantified over. The Hilbert epsilon-term denotes the term that satisfies the formula, seen as a predicate on x, if it exists [START_REF] Wirth | Hilbert's epsilon as an operator of indefinite committed choice[END_REF]. It can be seen as a Skolem term that records the formula itself.

Deduction modulo replaces the axiom by the rewrite rule, where X and Y are variables:

X ⊆ Y -→ ∀x (x ∈ X ⇒ x ∈ Y )
The proof produced by Zenon Modulo is then:

¬(A ⊆ A) δ ¬∀ , A ⊆ A -→ ∀x (x ∈ A ⇒ x ∈ A) ¬(τ ∈ A ⇒ τ ∈ A) α ¬⇒ τ ∈ A, ¬(τ ∈ A) where τ = x.¬(x ∈ A ⇒ x ∈ A).
It can be seen that computations are interleaved with the deduction rules. It can be noticed that the proof is much simpler than the one produced by Zenon. In addition to simplicity, deduction modulo also allows for unbounded proof size reduction [START_REF] Burel | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo[END_REF].

Dealing with large sets of axioms is quite difficult when building theories modulo. In the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF], the first order problems category has almost 7,000,000 axioms and the subset of set theory problems has more than 170,000 axioms. Since we cannot manually build rewrite systems for such large sets of axioms, we develop a heuristic to automatically turn axioms into rewrite rules.

The heuristic described below is based on the following guidelines. We never introduce a free variable that was not bound at the head of the formula by a universal quantifier. For rewrite rules over terms, we want to capture equality properties of terms, except axioms expressing commutativity for obvious termination reasons. We also excluded to rewrite a variable to a more complicated term for the same reason. For rewrite rules over propositions, we select axioms expressing equivalence properties of propositions. The left hand side of the rewrite rule must be an atom, or its negation, as required by deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF], and the right hand side may be any proposition. We also handle cases where the atomic proposition is an equality, in this case we require that at least one side of the equality is a function symbol. Moreover, axioms with just an atomic proposition, or its negation, are turned to rewrite to true, and false respectively. Finally, conjunctions of propositions that satisfy one of the previous conditions, are separated into multiple rewrite rules, accordingly to the logical equivalence of ∀x ϕ ∧ ψ and ∀x ϕ ∧ ∀x ψ, where ϕ and ψ are two arbitrary formulas.

In the following, t 1 and t 2 are terms, P is an atomic formula that is not an equation, and ϕ is an arbitrary formula. FV(ϕ) refers to the set of free variables of ϕ. Here are the shapes of axioms that are handled by our heuristic and the corresponding rewrite rule that is generated:

• ∀x t 1 = t 2
If FV(t 2 ) ⊆ FV(t 1 ) and t 1 is not a variable, then the term rewrite rule t 1 -→ t 2 is generated; Otherwise, if FV(t 1 ) ⊆ FV(t 2 ) and t 2 is not a variable, then the term rewrite rule t 2 -→ t 1 is generated;

In addition, all axioms expressing the commutativity of a given symbol are excluded.

• ∀x P (resp. ∀x ¬P )

The proposition rewrite rule P -→ is generated (resp. P -→ ⊥).

• ∀x P ⇔ ϕ (resp. ∀x ¬P ⇔ ϕ) If FV(ϕ) ⊆ FV(P ), then the proposition rewrite rule P -→ ϕ is generated (resp. P -→ ¬ϕ); Otherwise, if ϕ is a literal and FV(P ) ⊆ FV(ϕ), then we apply the heuristic to the formula ∀x ϕ ⇔ P (resp. ∀x ϕ ⇔ ¬P ).

• ∀x

(t 1 = t 2 ) ⇔ ϕ (resp. ∀x ¬(t 1 = t 2 ) ⇔ ϕ) If FV(ϕ) ⊆ FV(t 1 ) ∪ FV(t 2
) and at least one of the two terms t 1 and t 2 is not a variable, then the proposition rewrite rule (t

1 = t 2 ) -→ ϕ is generated (resp. (t 1 = t 2 ) -→ ¬ϕ).
The main difference between this new heuristic and the previous one presented in [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF] is the last item of the list above. With this new rule, we can transform into rewrite rules axioms which express an equivalence between equality of two terms and a proposition. An example of a proof using such rewrite rule is given in Sec. [START_REF] Boespflug | The λΠ-Calculus Modulo as a Universal Proof Language[END_REF]. In addition, we improve the generation of rewrite rules over terms in order to exclude to rewrite variables, and we deal with conjunctions of propositions that satisfy one the conditions listed above.

Experimental Results

TPTP Benchmarks

The TPTP library (v6.0.0) provides a large set of standard benchmark examples for automated theorem proving systems [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF]. To assess our approach, we perform experiments over all the first order problems coming from the TPTP library and dealing with set theory. This leads to select the SET and SEU categories that have respectively 462 and 900 problems. We compare Zenon, the old version of Zenon Modulo and the new version of Zenon Modulo which uses the heuristic described in Sec. 3. This experiment was done on an Intel Core i7-4770 3.40GHz computer, with a memory limit of 1GB and a timeout of 300s.

The results are summarized in Tab. 1. This table has three columns: the first one provides the number of problems proved by Zenon for each category, while the other two show the results for the old and new versions of Zenon Modulo. In addition, for both old and new versions of Zenon Modulo, we provide some detailed results with profit and loss between provers.

From the results of Tab. 1, we observe that the new version of Zenon Modulo proves more problems than Zenon and the old version of Zenon Modulo for both SET and SEU categories. The total profit of 5 problems in SET category (resulting from the gain of 12 problems and the loss of 7) may seem low, regarding to the difference of 73 problems between Zenon and the old version of Zenon Modulo, but we have gained some very difficult problems, as shown below. The improvement is more significant than for the SEU category. We notice a net profit of 8 problems, coming from a gain of 26 problems and a loss of 18. We also show an example from the SEU category below.

The verification by Dedukti of proofs produced by Zenon Modulo is almost total. Over the 227 proofs in SET category, 224 are correctly verified. The three missing proofs are due to termination issues of the translation of the proof from Zenon Modulo to Dedukti by the backend of Zenon Modulo. In SEU category, all the 110 proofs are declared well typed by Dedukti.

Analysis of Two Proofs From Set Theory

The TPTP library provides a ranking system to evaluate problems. This note, between 0 and 1, expresses the percentage of automated theorem provers that are not able to prove the problem. A note of 0 means that the problem is trivial (every prover solves it), and a note of 1 means that all provers fail. According to the TPTP ranking, Zenon Modulo is able to prove some quite difficult problems. The hardest problem is SET817+4, with a ranking of 0.97 in TPTP v6.0.0 (solved only by Muscadet [START_REF] Pastre | Muscadet 2.3: A knowledge-based theorem prover based on natural deduction[END_REF]), and which neither Zenon or the previous version of Zenon Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF] was able to prove. It states that the intersection of all elements of a non-empty set of ordinal numbers is an ordinal. Among the 8 axioms needed by Zenon Modulo to solve this problem, 7 are transformed into rewrite rules by our heuristic. The proof of this problem is too big to be displayed here.

An other example coming from the set theory, and that bodes well for application to the B method set theory, is the problem SEU194+1. This problem, with a ranking of 0.70, and which neither Zenon or the previous version of Zenon Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF] was able to prove, states that for any set s, if p is a relation, then the domain of the restriction of p to s is equal to the intersection of the domain of p and the set s. Among the twenty eight axioms provided with the conjecture, Zenon Modulo needs only two axioms to solve it, of which one is turned into a rewrite rule. In the following, s, t and u are sets, p is a relation, a is an element of a set, rel is a predicate for relations, dom a function that returns the domain of a relation, and rest a function that returns the restriction of a relation.

• Conjecture: ∀s, p (rel(p) ⇒ dom(rest(p, s)) = dom(p) ∩ s) • Axiom: ∀a, s, p (rel(p) ⇒ (a ∈ dom(rest(p, s)) ⇔ (a ∈ s) ∧ (a ∈ dom(p)))) • Rewrite rule: u = s ∩ t -→ ∀a (a ∈ u ⇔ ((a ∈ s) ∧ (a ∈ t)))
Zenon Modulo produces the proof of Fig. 1, presented in a format combining deduction steps in solid line and rewriting steps in dashed line. In addition, we omit some unnecessary formulas resulting from the application of β ⇔ rules to lighten the presentation.

¬(∀s, p (rel(p) ⇒ dom(rest(p, s)) = dom(p) ∩ s)), ∀a, s, p (rel(p) ⇒ (a ∈ dom(rest(p, s)) ⇔ a ∈ s ∧ a ∈ dom(p))) δ ¬∀ × 2 ¬(rel(τ2) ⇒ dom(rest(τ2, τ1)) = dom(τ2) ∩ τ1) α¬⇒ rel(τ2), ¬(dom(rest(τ2, τ1)) = dom(τ2) ∩ τ1) rewrite ¬(∀a (a ∈ dom(rest(τ2, τ1)) ⇔ a ∈ dom(τ2) ∧ a ∈ τ1)) δ ¬∀ ¬(τ3 ∈ dom(rest(τ2, τ1)) ⇔ τ3 ∈ dom(τ2) ∧ τ3 ∈ τ1) β¬⇔ Π1 τ3 ∈ dom(rest(τ2, τ1)), ¬(τ3 ∈ dom(τ2) ∧ τ3 ∈ τ1) β¬∧ Π2 Π3 Π1 ¬(τ3 ∈ dom(rest(τ2, τ1))), τ3 ∈ dom(τ2) ∧ τ3 ∈ τ1 α∧ τ3 ∈ dom(τ2), τ3 ∈ τ1 γ ∀ × 3 rel(τ2) ⇒ (τ3 ∈ dom(rest(τ2, τ1)) ⇔ τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2)) β⇒ ¬(rel(τ2)) τ3 ∈ dom(rest(τ2, τ1)) ⇔ τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2) β⇔ ¬(τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2)) β¬∧ ¬(τ3 ∈ τ1) ¬(τ3 ∈ dom(τ2)) τ3 ∈ dom(rest(τ2, τ1)) Π2 ¬(τ3 ∈ dom(τ2)) γ ∀ × 3 rel(τ2) ⇒ (τ3 ∈ dom(rest(τ2, τ1)) ⇔ τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2)) β⇒ ¬(rel(τ2)) τ3 ∈ dom(rest(τ2, τ1)) ⇔ τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2) β⇔ ¬(τ3 ∈ dom(rest(τ2, τ1))) τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2) α∧ τ3 ∈ τ1, τ3 ∈ dom(τ2) Π3 ¬(τ3 ∈ τ1) γ ∀ × 3 rel(τ2) ⇒ (τ3 ∈ dom(rest(τ2, τ1)) ⇔ τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2)) β⇒ ¬(rel(τ2)) τ3 ∈ dom(rest(τ2, τ1)) ⇔ τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2) β⇔ ¬(τ3 ∈ dom(rest(τ2, τ1))) τ3 ∈ τ1 ∧ τ3 ∈ dom(τ2) α∧ τ3 ∈ τ1, τ3 ∈ dom(τ2)
where :

τ1 = (s).¬(rel(p) ⇒ dom(rest(p, s)) = dom(p) ∩ s) τ2 = (p).¬(rel(p) ⇒ dom(rest(p, τ1)) = dom(p) ∩ τ1) τ3 = (a).¬(a ∈ dom(rest(τ2, τ1) ⇔ a ∈ dom(τ2) ∧ a ∈ τ1)) Fig. 1. Proof of Problem SEU194+1
The BWare project [START_REF]The BWare Project[END_REF] aims to provide a generic platform based on Why3 [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF] relying on different deduction tools, such as Alt-Ergo [START_REF] Bobot | Implementing Polymorphism in SMT solvers[END_REF], iProver Modulo [START_REF] Burel | Experimenting with Deduction Modulo[END_REF], Super Zenon [START_REF] Jacquel | Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover[END_REF] and Zenon Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF], in order to verify proof obligations coming from the development of industrial applications using the B method. Since B proof obligations are translated into the input language of Why3 [14], the B method set theory has been axiomatized in the WhyML language.

Building the B set theory modulo consists mainly in turning six axioms and many derived constructs into rewrite rules. The first two axioms, dealing with membership of an ordered pair in a cartesian product and the membership of a set in the power-set, can be easily turned into rewrite rules. The third axiom, defining the comprehension scheme, is removed due to its high-order definition, we present below how to deal with derived constructs defined with the comprehension scheme. The fourth axiom is the extensionality axiom and states that two sets s and t are equal if being a member of s is equivalent to be a member of t. This is not the only property of the equality symbol, as we will see below. Finally, the last two axioms, the axiom of choice and the existence of an infinite set are easy to deal with.

Following the notations of the B-Book, s and t are sets, E and F some expressions, x a variable, P(t) the power-set of the set t and BIG the constant infinite set. Here is the set of rewrite rules generated from the axioms:

           (E, F ) ∈ (s × t) -→ (E ∈ s ∧ F ∈ t) (pair) s ∈ P(t) -→ ∀x (x ∈ s ⇒ x ∈ t) (power) s = t -→ ∀x (x ∈ s ⇔ x ∈ t) (extensionality) choice(s) ∈ s -→ ∃x (x ∈ s) (choice) infinite(BIG) -→ (infinite)

Removal of the Comprehension Scheme

In the B-book, the comprehension scheme is used to define non-primitive symbols. For instance, the union of two sets is defined as follows:

s ∪ t := {a | a ∈ u ∧ (a ∈ s ∨ a ∈ t)}
where u is a set, and s and t and two subsets of u.

Since we have dismissed the comprehension scheme, we expand the above definition by directly defining membership to the union, thereby removing the use of comprehension:

x ∈ s ∪ t -→ x ∈ s ∨ x ∈ t (union)
This rewrite rule, combined with extensionality, is equivalent to the previous definition of the union. Handling the other non-primitive symbols, like intersection of sets, inverse of a relation or also the identity relation, in this systematic way, allows a total removal of the comprehension scheme used to define derived constructs in the B-Book. Unfortunately, this method do not permit us to manage user-defined sets using the comprehension scheme for the moment.

Here is, as an example, the proof produced by Zenon Modulo for the commutativity of union:

¬∀A, B (A ∪ B = B ∪ A) δ ¬∀ ¬∀B (τ 1 ∪ B = B ∪ τ 1 ) δ ¬∀ τ 1 ∪ τ 2 = τ 2 ∪ τ 1 extensionality ¬∀X (X ∈ τ 1 ∪ τ 2 ⇔ X ∈ τ 2 ∪ τ 1 ) δ ¬∀ ¬(τ 3 ∈ τ 1 ∪ τ 2 ⇔ τ 3 ∈ τ 2 ∪ τ 1 ) β ¬⇔ Π 1 Π 2
where Π 1 and Π 2 are the following subtrees:

Π 1 ¬(τ 3 ∈ τ 1 ∪ τ 2 ), τ 3 ∈ τ 2 ∪ τ 1 union × 2 ¬(τ 3 ∈ τ 1 ∨ τ 3 ∈ τ 2 ), τ 3 ∈ τ 2 ∨ τ 3 ∈ τ 1 α ¬∨ ¬(τ 3 ∈ τ 1 ), ¬(τ 3 ∈ τ 2 ) β ∨ τ 3 ∈ τ 2 τ 3 ∈ τ 1 Π 2 τ 3 ∈ τ 1 ∪ τ 2 , ¬(τ 3 ∈ τ 2 ∪ τ 1 ) union × 2 τ 3 ∈ τ 1 ∨ τ 3 ∈ τ 2 , ¬(τ 3 ∈ τ 2 ∨ τ 3 ∈ τ 1 ) α ¬∨ ¬(τ 3 ∈ τ 2 ), ¬(τ 3 ∈ τ 1 ) β ∨ τ 3 ∈ τ 1 τ 3 ∈ τ 2
and where:

τ 1 = A.¬(A ∪ B = B ∪ A) τ 2 = B.¬(τ 1 ∪ B = B ∪ τ 1 ) τ 3 = X.¬(X ∈ τ 1 ∪ τ 2 ⇔ X ∈ τ 2 ∪ τ 1 )
We notice that the subtrees Π 1 and Π 2 are symmetric, the proof of the commutativity of union resulting of the commutativity of the disjunction.

Dealing with Equality

The set theory of the B-book relies heavily on a primitive notion of equality, introduced before axioms for the set theory [START_REF] Halmagrand | The B-Book, Assigning Programs to Meanings[END_REF]. The main property of the equality is substitutivity (i.e. an expression can be replaced by another one in a proposition provided they are equal). Starting from substitutivity and reflexivity of equality, other properties like symmetry and transitivity can be derived. Zenon already have rules that deal with this equational reasoning [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF].

The second property of equality, introduced much later, and that has to deal directly with set theory is extensionality as shown in Fig. 2. Turning the axiom of extensionality into a rewrite rule allows Zenon Modulo to extend the equality symbol into membership equivalence at each step of the proof-search.

Choosing between equational reasoning and the extensionality properties of equality during proof-search may be decisive to find a proof. There are different solutions to deal with this problem. A first idea is to try both equational reasoning and extensionality every time we meet an equality symbol, but this solution may not be efficient since we duplicate the work for each equality symbol. The solution we are working on is to implement a heuristic into Zenon Modulo that decides to apply the extensionality rewrite rule, or to use the equational reasoning of Zenon, based on the shape of terms. For instance, if both sides of the equality are variables, we do not apply the extensionality rewrite rule, otherwise we use it.

Conclusion

We have presented some improvements of Zenon Modulo, in particular a new heuristic to transform axioms into rewrite rules over terms and propositions. This heuristic is used as a preprocessing tool to automatically build theories modulo given sets of axioms. We have also presented results obtained on set theory problems, coming from the benchmarks provided by the TPTP library. This experiment was performed using the new heuristic. In particular, we have shown that this new version proves some new difficult problems according to the TPTP ranking.

We have also discussed some recent work about the application of our tool to the B method set theory. Since we want to use Zenon Modulo to verify proof obligations coming from the development of industrial applications using the B method, we have to build a B set theory modulo. We have described a method to remove the comprehension scheme used to define non-primitive symbols like union of sets. Finally, we have presented some ideas to handle equality in the B set theory.

As future work, we first aim to implement a heuristic into Zenon Modulo that handles the equality of B set theory. In particular, this heuristic should decide whether to apply the extensionality rewrite rule, or to use the equational reasoning of Zenon. To assess our work, we will first try to prove a large part of derived lemmas coming from the B-Book. Finally, we will apply Zenon Modulo to the set of proof obligations provided by the benchmarks of the BWare project.

Fig. 2 .

 2 Fig. 2. Expression of the Axioms of the B Set Theory as a Rewrite System

Table 1 .

 1 Experimental Results over the TPTP Library

	TPTP Category	Zenon	Zenon Modulo (Old)	Zenon Modulo (New Version)
		Total	Total	vs. Zenon	Total	vs. Zenon	vs. Old
	SET 462 prob.	149	222	+86 -13	227	+91 -13	+12 -7
	SEU 900 prob.	96	102	+14 -8	110	+32 -18	+26 -18

Acknowledgement. Many thanks to O. Hermant, and D. Doligez for their detailed comments on this paper, and to the Deducteam Inria research team for the many interactions.

This work is supported by the BWare project [17] (ANR-12-INSE-0010) funded by the INS programme of the French National Research Agency (ANR).