Isaac Ohavi

COMPARISON PRINCIPLE FOR WALSH'S SPIDER HJB EQUATIONS WITH NON LINEAR LOCAL TIME KIRCHHOFF'S BOUNDARY TRANSMISSION

Keywords: Discontinuous non degenerate Hamilton-Jacobi-Bellman equations, non linear local-time Kirchhoff's boundary transmission, comparison principle, speed of Hamiltonian, Kirchhoff

The main purpose of this work is to obtain a comparison principle for viscosity solutions of a system of elliptic Walsh's spider Hamilton-Jacobi-Bellman equations, possessing a new boundary condition called non linear local-time Kirchhoff 's transmission. The main idea is to build test functions at the neighborhood of the vertex solutions of ODE, with well-designed coefficients. The key point is to impose a 'local-time' derivative at the vertex absorbing the error term induced by -what we decide to call herethe Kirchhoff 's speed of the Hamiltonians.

Introduction

We are given R > 0 and K > 0 two boundaries of a 'space/local-time' domain (0, R) × (0, K) ∋ (x, l), This research was supported by the GIF grant 1489-304.6/2019. I am grateful to Miguel Martinez ℶ for the several discussions and collaborations on spider diffusions and their related partial differential equations. ℶ Université Gustave Eiffel, LAMA UMR 8050, France, miguel.martinez@univ-eiffel.fr.

an integer number I (with I ≥ 2), I distinct angles (θ 1 , . . . , θ I ) ∈ [0, 2π) I in the plane R 2 , and a controlled spider measure S with constant support (θ 1 , . . . , θ I ):

S :=        [0, K] × O → M [0, 2π) , (l, ϑ) → I i=1 S θ i , l, ϑ)δ θ i (dθ)
, where O is a compact of R I (and M [0, 2π) denotes the set of the angle measures en the plan).

The main target of this work is to obtain a comparison theorem (thus uniqueness) for continuous viscosity solution of the following Walsh's spider Hamilton-Jacobi-Bellman system -W alsh (S) -having a new boundary condition at the vertex 0, called non linear local-time Kirchhoff 's boundary transmission:

W alsh (S) :=                                              λu i (x, l) + sup β i ∈B i -σ i (x, l, β i )∂ 2 x u i (x, l)+ b i (x, l, β i )∂ x u i (x, l) + h i (x, l, β i ) = 0, (x, l) ∈ (0, R) × (0, K),
Non linear local-time Kirchhoff 's boundary transmission:

∂ l u(0, l) + inf ϑ∈O I i=1
S(θ i , l, ϑ)∂ x u i (0, l) + h 0 (l, ϑ) = 0, l ∈ (0, K) 2 , ∀l ∈ [0, K], u i (0, l) = u j (0, l).

u i (R, l) = χ i (l), l ∈ [0, K], u i (x, K) = T i (x), x ∈ [0, R] ∀(i, j) ∈ [[1, I]]
(

) 1
In order to simplify our study, we have assumed in our framework that all the rays

R i = [0, R] × {i}, i ∈ [[1, I]
] have the same length R > 0, and that Dirichlet boundary condition χ i holds at x = R and T i at l = K. A more general setting could be treated with similar tools: one could for instance consider more general rays, and/or a mix of local-time Kirchoff's and Dirichlet boundary conditions at the x = R, l = K, etc.

On the other hand, it should be noted that the supremums and infinimums appearing in the system do not play a preponderant role in the proof of our comparison theorem, and no convexity is required. The reader can easily obtain the same lines of proof by considering other supremums or infinimums, such as Isaac's HJB equations. We wanted to formulate the non linearity using Hamiltonians that appear naturally in stochastic control theory.

The intuition is for the reader to keep an eye on the underlying process, in order to better understand the behavior of the process at the junction point and its non-stickiness. It is more precisely the understanding of the non-stickiness, in particular its proof in the case of a Walsh's spider diffusion (see few lines below for a brief introduction), that gave us some intuitions for the construction of the test functions.

Fully nonlinear Hamiltonians can be considered, as soon as they satisfy an ellipticity condition on each domain R i = [0, R] × {i}, i ∈ [ [1, I]]; quadratic growth with respect to the gradient; whereas the Kirchhoff's condition at the vertex 0 must simply be strictly increasing with respect to the gradient. We aim in an upcoming work, to obtain existence and uniqueness of system [START_REF] Barles | A Bellman approach for two-domains optimal control problems in R N[END_REF] with more general Hamiltonians, and especially with a more general angular measure. Let us finally mention that our results can be also extended to time-dependent problems using classical arguments arising from the theory of viscosity solutions.

We start by explaining why we decided to call the system given in (1): Walsh's spider

Hamilton-Jacobi-Bellman system -W alsh (S) -before describing more precisely the origins and the motivations which pushed us to consider a new condition called non linear localtime Kirchhoff 's boundary transmission, at the vertex 0.

System (1) -W alsh (S) and its variants, whether in the linear or non-linear frameworks, are more often called in the literature: "system of PDE posed on a star-shaped network".

See for instance amongst the vast works on this subject: [START_REF] Imbert | Flux-limited solutions for quasi-convex Hamilton Jacobi equations on networks preprint[END_REF], [START_REF] Lions | Viscosity solutions for junctions: well posedness and stability[END_REF], [START_REF] Lions | Well-posedness for multi-dimensional junction problems with Kirchhoff-type conditions[END_REF], [START_REF] Lions | Effective transmission conditions for second-order elliptic equations on networks in the limit of thin domains[END_REF], [START_REF] Martinez | Well posedness of linear Parabolic partial differential equation posed on a star-shaped network with local-time Kirchhoff's boundary condition at the vertex (submitted)[END_REF], [START_REF] Ohavi | Quasi-linear parabolic PDE posed on a network with nonlinear Neumann boundary condition at vertices[END_REF], [START_REF] Below | Classical solvability of linear parabolic equations on networks[END_REF], [START_REF] Below | A maximum principle for semi linear parabolic network equations[END_REF], [START_REF] Below | An existence result for semi linear parabolic network equations with dynamical node conditions. Partial differential equations: elliptic and parabolic problems (Pont-à-Mousson[END_REF]...

It is crucial to note that in the most works in literature dealing with the analysis of these PDE systems posed on networks, the angles appearing in the geometry of the network do not play any role in obtaining existence, regularity, comparison theorem... Indeed it appears that we can consider any star-shaped network with exactly the same rays in any Euclidean space R n , n ≥ 2; spaced by the same number of angles, without modifying the mathematical analysis of these PDE systems.

However, PDE posed on networks, are naturally related to diffusions on graphs introduced in the seminal works of Freidlin and Wentzell [START_REF] Freidlin | Diffusion processes on an open book and the averaging principle[END_REF] and Freidlin and Sheu α i = 1, it is proved in [START_REF] Freidlin | Diffusion processes on an open book and the averaging principle[END_REF] that there exists a continuous Feller Markov process x(•), i(•) valued in the star-shaped network, whose generator is given by the following operator:

L :      C 2 (N R ) → C(N R ), f = f i (x) → b i (x)∂ x f i (x) + σ 2 i (x) 2 ∂ 2 x f i (x)
, with domain

D(L) := f ∈ C 2 (N R ), I i=1 α i ∂ x f i (0) = 0 .
Recall that it is shown in [START_REF] Freidlin | Diffusion processes on graphs: stochastic differential equations, large deviation principle[END_REF] that there exists a one dimensional Wiener process W defined on a probability space (Ω, F, P) and adapted to the natural filtration of x(•), i(•) , such that the process x(•) satisfies the following stochastic differential equality:

dx(t) = b i(t) (x(t))dt + σ i(t) (x(t))dW (t) + dℓ(t) , 0 ≤ t ≤ T.
In the above equality, the process ℓ(•) is the local time of the process x(•) at the vertex 0. Moreover, the process ℓ(•) has continuous increasing paths, starts from 0 and satisfies:

∀t ∈ [0, T ], t 0 1 {x(s)>0} dℓ(s) = 0, P -a.s.
Recall also that the following Itô's formula was proved in [START_REF] Freidlin | Diffusion processes on graphs: stochastic differential equations, large deviation principle[END_REF]:

df i(t) (x(t)) = b i(t) (x(t))∂ x f i(t) (x(t)) + 1 2 σ 2 i(t) (x(t))∂ 2 x f i(t) (x(t)) dt + ∂ x f i(t) (x(t))σ i(t) (x(t))dW (t) + I i=1 α i ∂ x f i (0)dℓ(t), P -a.s, (2)
for any sufficiently regular f .

Diffusions on graphs can also be seen as part of the family of Walsh processes introduced in the epilogue [START_REF] Walsh | A diffusion with a discontinuous local time[END_REF]. Indeed, if one introduces a spider measure S, such that:

∀i ∈ [[1, I]], S(θ i ) = α i ,
the Kirchhoff's term in the Itô's formula [START_REF] Barles | A Bellman approach for regional optimal control problems in R N[END_REF], can be rewritten as:

I i=1 α i ∂ x f i (0)dℓ(t) = 2π 0 ∂ x f θ (0)S(dθ) dℓ(t),
We now see under this formulation that the geometry of the system is uniquely determined by the support of the spider measure S, namely the angles (θ 1 , ..., θ I ). This is the main reason which pushed us to call the system (1): Walsh's spider Hamilton-Jacobi-Bellman system -W alsh (S), keeping in mind the extension of our result to more general angular measure. The non linear local-time Kirchhoff 's term appearing in (1) will be transformed in:

∂ l u(0, l) + inf ϑ∈O 2π 0 ∂ x u θ (0, l)W(l, ϑ)(dθ) + h 0 (l, ϑ) , with W : [0, K] × O → M [0, 2π) .
In the linear (parabolic) framework:

                                                   ∂ t u i (t, x, l) -a i (t, x, l)∂ 2 x u i (t, x, l) + b i (t, x, l)∂ x u i (t, x, l) +c i (t, x, l)u i (t, x, l) = f i (t, x, l), (t, x, l) ∈ (0, T ) × (0, R) × (0, K),
Local time Kirchhoff 's boundary condition:

∂ l u(t, 0, l) + I i=1 α i (t, l)∂ x u i (t, 0, l) = ϕ(t, l), (t, l) ∈ (0, T ) × (0, K), ∂ x u i (t, R, l) = 0, (t, l) ∈ (0, T ) × (0, K), ∀(i, j) ∈ [[1, I]] 2 , u i (t, 0, l) = u j (t, 0, l) = u(t, 0, l), (t, l) ∈ |0, T ] × [0, K], ∀i ∈ [[1, I]], u i (t, x, K) = ψ i (t, x), (t, x) ∈ [0, T ] × [0, R], ∀i ∈ [[1, I]], u i (0, x, l) = g i (x, l), (x, l) ∈ [0, R] × [0, K], (3)
system (3) has been studied recently by Martinez-Ohavi in [START_REF] Martinez | Well posedness of linear Parabolic partial differential equation posed on a star-shaped network with local-time Kirchhoff's boundary condition at the vertex (submitted)[END_REF].

From a PDE technical aspect, since the variable l drives dynamically the system only at the junction point 0 with the presence of the derivative ∂ l u(t, 0, l) in the local time Kirchhoff's boundary condition, the main challenge was to understand the regularity of the solution. Under mild assumptions, it is shown that classical solutions of the system

(3) belong to the class C 1,2 in the interior of each edge and C 0,1 in the whole domain (with respect to the time-space variables (t, x)). One can expect a regularity in the class C 1 for l → u(t, 0, l) and this is indeed the case (see Theorem 2.4 and point iv) in Definition 2.1 in [START_REF] Martinez | Well posedness of linear Parabolic partial differential equation posed on a star-shaped network with local-time Kirchhoff's boundary condition at the vertex (submitted)[END_REF]). Another technical aspect, was to obtain an Hölder continuity of the partial functions l → ∂ t u i (t, x, l), ∂ x u i (t, x, l), ∂ 2 x u i (t, x, l) for any x > 0. It is shown using Schauder's estimates, that such regularity is guaranteed by the central assumption on the ellipticity of the diffusion coefficients on each rays, together with the mild dependency of the coefficients and free term with respect to the variable l. The comparison theorem holds true in the linear case under such regularity class; see Theorem 2.6 in [START_REF] Martinez | Well posedness of linear Parabolic partial differential equation posed on a star-shaped network with local-time Kirchhoff's boundary condition at the vertex (submitted)[END_REF]. The reader has to keep in mind that this class of regularity will be naturally used for test functions of system (1) -W alsh (S) -since if a viscosity solution is in this regularity class, then the formulation with test functions in this class remains compatible.

Keeping in mind that system (1) characterizes the value function of a problem of a stochastic scattering control of Walsh's spider diffusion, with optimal directions selected by its own local time, the same authors studied existence and uniqueness of Walsh's spider process with spinning measure selected from the local time in [START_REF] Martinez | Martingale problem for a Walsh's spider diffusion with spinning measure selected from its own local time[END_REF]. More precisely, it is shown that there exists a unique probability measure P, such that the following process

f i(s) (s, x(s)) -f i (0, x) - s 0 ∂ t f i(u) (u, x(u)) + 1 2 σ 2 i(u) (u, x(u), l(u))∂ 2 xx f i(u) (u, x(u)) + b i(u) (u, x(u), l(u))∂ x f i(u) (u, x(u)) du - I j=1 s 0 α j (u, l(u))∂ x f j (u, 0)dl(u) 0≤s≤T ,
is a martingale under P, for any f smooth enough. Up to our knowledge, this is the first result in literature dealing with a non constant spinning measure for a Walsh diffusion.

Moreover, let us quote that uniqueness in distribution of such a process is completely determined by the uniqueness of the corresponding PDE system given in [START_REF] Barles | Almost) everything you always wanted to know about deterministic control problems in stratified domains[END_REF].

Now let us now describe the whys and wherefores of considering a non linear local-time

Kirchhoff 's transmission, in the non-linear framework for W alsh (S).

Assume that one wants to find the optimal strategy, or the optimal scattering control at the vertex 0, using the following Kirchhoff's Hamiltonian (like it appears naturally in the Itô's rule (2)):

inf ϑ∈O I i=1 α i (ϑ)∂ x u i (0) .
As it appears, the optimal control ϑ * depends naturally only on the gradient of the value function at 0, namely:

ϑ * (u) = ϑ * ∂ x u 1 (0), ..., ∂ x u I (0) ,
and behaves like a system of first order. This is quite intriguing, since the trajectories of the spider are chaotic at the junction point, whereas a first continuous order system does not present any irregularities induced by the behavior of a Brownian motion. Hence, ϑ * should depend in some way on the second order terms.

The local time ℓ of the spider is related to the second order terms by the following quadratic approximation:

lim ε→0 E P 1 2ε I i=1 • 0 σ 2 i (0)1 {0≤x(s)≤ε,i(s)=i} ds -ℓ(•) 2 (0,T ) = 0. ( 4
)
When the coefficients σ 2 i (0) i∈[ [1,I]] vanish, the local time disappears and the system behaves more like a first order HJB system.

It appears therefore natural to consider the local time as an intrinsic variable to the stochastic control problem with the non linear local-time Kirchhoff 's boundary transmission (induced by the Itô's rule extended now to the web/local-time space):

∂ l u(0, ℓ) + inf ϑ∈O I i=1 S(θ i , ℓ, ϑ)∂ x u i (0, ℓ) ,
and to obtain an optimal control ϑ * at the vertex 0 given by:

ϑ * (u, ℓ) = ϑ * ∂ x u 1 (0, ℓ), ..., ∂ x u I (0, ℓ), ℓ .
The dependence on the second order terms appears now with the quadratic approximation of the local time ℓ given in [START_REF] Bressan | Optimal control problems on stratified domains[END_REF].

Another key point when we study the behavior of a Walsh's spider motion, is to notice that all discontinuities generated by the coefficients b i (0) ̸ = b j (0), σ i (0) ̸ = σ j (0) i̸ =j , disappear in Itô's rule [START_REF] Barles | A Bellman approach for regional optimal control problems in R N[END_REF] with the aid of what we call the non-stickiness condition satisfied by the Walsh's spider x(t), i(t) t≥0 at 0: ∀t ≥ 0, t 0 1 {x(s)=0} ds = 0, P a.s.

To obtain this non-stickiness condition, the authors in [START_REF] Freidlin | Diffusion processes on graphs: stochastic differential equations, large deviation principle[END_REF] used an ordinary differential equation (ODE). This ODE involves coefficients depending on the speed measure s i (x)dx of the Walsh's spider on each rays:

∀x > 0, ∀i ∈ [[1, I]], s i (x)dx = 2 σ 2 i (x) exp x 0 2b i (z) σ 2 i (z) dz dx. (5)
This fact has given us the intuitions to build test functions of system (1) at the vertex 0.

If one considers the following Hamiltonians H i , i ∈ [ [1, I]] :

H i :=        [0, R] × [0, K] × R 3 → R,
(x, l, u, p, S) → λu + sup

β i ∈B i -σ i (x, l, β i )S + b i (x, l, β i )p + h i (x, l, β i ) ,
appearing on each rays of system (1), we can define similarly to the speed measure s i (x)dx, the speed of the Hamiltonians S peed

(H i ), i ∈ [[1, I]] as: S peed (H i ) :=        [0, R] × [0, K] × R → R, (x, l, p) → sup β i ∈B i b i (x, l, β i )p + h i (x, l, β i ) σ i (x, l, β i )
.

To prove the comparison theorem for system (1), we will build test functions at the junction point 0 solutions of ODE with coefficients that may be viewed as a kind of envelope of all possible errors of the speed of the Hamiltonians S peed (H i ) i∈[ [1,I]] . The key point in this construction is to impose a local-time derivative with respect to variable l, at 0 -∂ l ϕ(0, l) -that will absorb all the error term induced by -that we have decide to call -the Kirchhoff 's speed of the Hamiltonians -

K f S peed (H i ), i ∈ [[1, I]
] -given by:

K f S peed :=        [0, R] × [0, K] × R → R, (x, l, p) → inf ϑ∈O I i=1 S(θ i , l, ϑ)S peed (H i )(x, l, p)
.

Up to our knowledge, this is the first result of uniqueness for HJB elliptic PDE system posed on a star shaped-network, having a nonlinear Kirchhoff's condition and non vanishing viscosity at the vertex.

Recall that in the theory of viscosity solutions, the formulation of upper and sub solutions for a second order nonlinear problem with Neumann N (or Kirchhoff"s) boundary condition: ). More precisely, in almost all cases the proof of the comparison theorem consists in introducing the doubling variable method, with the function:

     H x, u(x), ∇u(x), ∆u(x) = 0, x ∈ Ω, N x, u(x), ∇u(x) = 0, x ∈ ∂Ω , (6)
∀ε > 0, w ε x, y) = u(x) -v(y) - |x -y| 2 R n 2ε 2 , (x, y) ∈ R n ,
(where u is a supper solution, whereas v is a sub solution of ( 6)) and to obtain a contradiction, passing to the limit when ε ↘ 0, locally at any point x ∈ Ω. When x ∈ ∂Ω, both conditions F and H are then considered, and the Hamiltonian H has to be continuous at the neighborhood of any point x ∈ ∂Ω. Consequently, we will get that this method will fail for system (1), because of the discontinuities of the Hamiltonians at 0.

We will see that the construction of the test function for proving the comparison theorem in this work, allow us to formulate supper and sub viscosity solution in the strong sense at 0. Note that the non linear local-time Kirchhoff 's boundary transmission appears at 0, without considering any values of the Hamiltonians at the vertex.

To finish this introduction, let us give an account of the main works that have been done in literature for similar systems close to [START_REF] Barles | A Bellman approach for two-domains optimal control problems in R N[END_REF]. Note that the key fact in most all of them, is to consider a vanishing viscosity at the vertex 0, which is not the case here.

In [START_REF] Lions | Viscosity solutions for junctions: well posedness and stability[END_REF], the authors introduce a notion of state-constraint viscosity solutions for one dimensional "junction"-type problems for first order Hamilton-Jacobi equations with nonconvex coercive Hamiltonians and study its well-posedness and stability properties. Let us quote that in this work, the main results do not require any convexity conditions on the Hamiltonians, contrary to all the previous literature that is based on the control (deterministic) theoretical interpretation of the problem. Among the long list of references on this topic with convex Hamiltonians, we can cite for instance: [START_REF] Barles | A Bellman approach for two-domains optimal control problems in R N[END_REF], [START_REF] Barles | A Bellman approach for regional optimal control problems in R N[END_REF], [START_REF] Barles | Almost) everything you always wanted to know about deterministic control problems in stratified domains[END_REF], [START_REF] Bressan | Optimal control problems on stratified domains[END_REF], [START_REF] Imbert | Flux-limited solutions for quasi-convex Hamilton Jacobi equations on networks preprint[END_REF], [START_REF] Imbert | Generalized junction conditions for degenerate parabolic equations[END_REF]. The same authors in [START_REF] Lions | Well-posedness for multi-dimensional junction problems with Kirchhoff-type conditions[END_REF] have studied multi-dimensional junction problems for first and second-order PDE with Kirchhoff-type Neumann boundary conditions, showing that their generalized viscosity solutions are unique, but still with a vanishing viscosity at the vertex for the second order terms. Finally, let us cite the interesting approach studied in [START_REF] Lions | Effective transmission conditions for second-order elliptic equations on networks in the limit of thin domains[END_REF], where it is considered star-shaped tubular domains consisting of a number of nonintersecting, semi-infinite strips of small thickness that are connected by a central region.

It is shown that classical regular solutions of uniformly elliptic partial differential equations converge in the thin-domain limit, to the unique solution of a second-order partial differential equation on the network satisfying an effective Kirchhoff-type transmission condition at the junction.

The paper is organized as follows: In Section 2, we introduce the main notations and we state the main Theorem 2.2 of this work. Section 3 is dedicated to give a sketch of proof in the linear case of our method, for simple elliptic PDE, in order to give to the reader some intuitions and ideas that will be used for the construction of tests functions for our central Theorem 2.2. Finally in Section 4, we prove our main Theorem, that is the comparison principle for system (1).

Notations and Definitions

In this section, we introduce the main notations-definitions and we state our main Theorem 2.2. In all this work, we fix R > 0 and K > 0 the boundary of the 'space/localtime' domain

(0, R) × (0, K) ∋ (x, l)
where the system (1) will be studied.

We are given an integer number I (with I ≥ 2) and I distinct angles (θ 1 , . . . , θ I ) ∈ [0, 2π) I in the plane R 2 . We introduce the space of the spiders measures on the plan R 2 , denoted by:

Z (θ i ) i∈[[1,I]] .
consisting on the set of the discrete measures [0, 2π), B([0, 2π) , having (θ 1 , . . . , θ I ) as constant support.

In other terms M ∈ Z (θ i ) i∈[ [1,I]] if and only if there exists M(θ 1 ), . . . , M(θ I ) ∈ [0, +∞) I such that:

M(dθ) = I i=1 M(θ i )δ θ i (dθ).
To the angles (θ 1 , . . . , θ I ), we associate on the oriented euclidean plan (0 R 2 , ⃗ u, ⃗ v), a bounded star-shaped network N R defined by:

N R = I i=1 R i , with ∀i ∈ [[1, I]], ⃗ u, ⃗ R i = θ i , ∀i ∈ [[1, I]] R i := [0, R] and ∀(i, j) ∈ [[1, I]] 2 , i ̸ = j, R i ∩ R j = 0 R 2 , consisting of I compact rays R i ∼ = [0, R] (R > 0) emanating from the origin 0 R 2 of
the plane R 2 -that we will often call the junction point or the vertex 0 -and spaced successively to the abscissa axis by the angles (θ 1 , . . . , θ I ).

Let (B i ) i∈[[1,I]] be a collection of I compact sets of R and O a compact set of R I .
We introduce the following data:

Data: (D)                                            σ i ∈ C [0, R] × [0, K] × B i , R i∈[[1,I]] b i ∈ C [0, R] × [0, K] × B i , R i∈[[1,I]] h i ∈ C [0, R] × [0, K] × B i , R i∈[[1,I]] S ∈ C [0, K] × O, Z (θ i ) i∈[[1,I]] h 0 ∈ C [0, K] × O, R , χ i ∈ C [0, K], R i∈[[1,I]]
,

T i ∈ C [0, R], R i∈[[1,I]]
.

.

We assume that the data (D) satisfy the following assumptions: (where (A) stands for the spider measure S, (E) for ellipticity, and (R) for Lipschitz regularity uniformly with respect to the control variables):

Assumption (H) (A) ∃ ζ > 0, ∀i ∈ [[1, I]], ∀(l, ϑ) ∈ [0, K] × O, S(θ i , l, ϑ) ≥ ζ. (E) ∃ σ > 0, ∀i ∈ [[1, I]], ∀(x, l, β i ) ∈ [0, R] × [0, K] × B i , σ i (x, l, β i ) ≥ σ. (R) ∃ (|b|, |h|, ζ, σ) ∈ (0, +∞) 4 , ∀i ∈ [[1, I]], (R -i) sup x,l,β i |b i (x, l, β i )| + sup l,β i sup (x,y), x̸ =y |b i (x, l, β i ) -b i (y, l, β i )| |x -y| + sup x,β i sup (l,l ′ ), l̸ =l ′ |b i (x, l, β i ) -b i (x, l ′ , β i )| |l -l ′ | ≤ |b|, (R -ii) sup x,l,β i |σ i (x, l, β i )| + sup l,β i sup (x,y), x̸ =y |σ i (x, l, β i ) -σ i (y, l, β i )| |x -y| + sup x,β i sup (l,l ′ ), l̸ =l ′ |σ i (x, l, β i ) -σ i (x, l ′ , β i )| |l -l ′ | ≤ σ, (R -iii) sup x,l,β i |h i (x, l, β i )| + sup l,β i sup (x,y), x̸ =y |h i (x, l, β i ) -h i (y, l, β i )| |x -y| + sup x,β i sup (l,l ′ ), l̸ =l ′ |h i (x, l, β i ) -h i (x, l ′ , β i )| |l -l ′ | ≤ |h|, (R -iv) sup l,ϑ |S(θ i , l, ϑ)| + sup ϑ sup (l,l ′ ), l̸ =l ′ |S(θ i , l, ϑ) -S(θ i , l ′ , ϑ)| |l -l ′ | ≤ ζ, (R -v) sup l,ϑ |h 0 (l, ϑ)| + sup ϑ sup (l,l ′ ), l̸ =l ′ |h 0 (l, ϑ) -h 0 (l ′ , ϑ)| |l -l ′ | ≤ |h|.
Fix now all around this work: λ > 0.

In this study, we will obtain a comparison theorem for the following Walsh's spider Hamilton-Jacbi-Bellman system W alsh (S), having a non linear local-time Kirchhoff 's boundary transmission at 0:

W alsh (S) :=                                              λu i (x, l) + sup β i ∈B i -σ i (x, l, β i )∂ 2 x u i (x, l)+ b i (x, l, β i )∂ x u i (x, l) + h i (x, l, β i ) = 0, (x, l) ∈ (0, R) × (0, K),
Non linear local-time Kirchhoff 's boundary transmission:

∂ l u(0, l) + inf ϑ∈O I i=1 S(θ i , l, ϑ)∂ x u i (0, l) + h 0 (l, ϑ) = 0, l ∈ (0, K) u i (R, l) = χ i (l), l ∈ [0, K], u i (x, K) = T i (x), x ∈ [0, R] ∀(i, j) ∈ [[1, I]] 2 , ∀l ∈ [0, K], u i (0, l) = u j (0, l). (7)
Given the following Hamiltonians H i , i ∈ [[1, I]] defined by:

H i :=        [0, R] × [0, K] × R 3 → R, (x, l, u, p, S) → sup β i ∈B i λu -σ i (x, l, β i )S + b i (x, l, β i )p + h i (x, l, β i ) .
we will often refer in this work to the speed of the Hamiltonians S peed

(H i ), i ∈ [[1, I]]
and the Kirchhoff 's speed of the Hamiltonians

K f S peed (H i ), i ∈ [[1, I]]
, that are both defined by:

S peed (H i ) :=        [0, R] × [0, K] × R → R, (x, l, p) → sup β i ∈B i b i (x, l, β i )p + h i (x, l, β i ) σ i (x, l, β i ) , and
K f S peed :=        [0, R] × [0, K] × R → R, (x, l, p) → inf ϑ∈O I i=1 S(θ i , l, ϑ)S peed (H i )(x, l, p)
.

In order to remain consistent with the results obtained in [START_REF] Martinez | Well posedness of linear Parabolic partial differential equation posed on a star-shaped network with local-time Kirchhoff's boundary condition at the vertex (submitted)[END_REF], more precisely with the class of regularity of the solutions in the linear framework (see Introduction in [START_REF] Martinez | Well posedness of linear Parabolic partial differential equation posed on a star-shaped network with local-time Kirchhoff's boundary condition at the vertex (submitted)[END_REF]), we introduce the following space of test functions for continuous viscosity solutions of the system W alsh (S):

C 2,0 0,1 N R × [0, K] := f : N R × [0, K], ((x, i), l) → f i (x, l) ∀i ∈ [[1, I]], f i : [0, R] × [0, K] → R, (x, l) → f i (x, l) ∈ C 2,0 ([0, R] × [0, K]), ∀(i, j, l) ∈ [[1, I]] 2 × [0, K], f i (0, l) = f j (0, l) = f (0, l), f (0, •) ∈ C 1 [0, K] .
We continue this section by giving the definition of continuous viscosity supper and sub solutions that belong to C N R × [0, K] , defined by:

C N R × [0, K] := f : N R × [0, K], ((x, i), l) → f i (x, l) ∀i ∈ [[1, I]], f i : [0, R] × [0, K] → R, (x, l) → f i (x, l) ∈ C 0 ([0, R] × [0, K]), ∀(i, j, l) ∈ [[1, I]] 2 × [0, K], f i (0, l) = f j (0, l) = f (0, l) .
for the Walsh's spider HJB system -W alsh (S) -given in [START_REF] Imbert | Generalized junction conditions for degenerate parabolic equations[END_REF].

Definition 2.1. Let u ∈ C N R × [0, K] . a)
We say that u is a continuous viscosity supper solution of the W alsh (S) system (7), if for all test function ϕ ∈ C 2,0 0,1 N R × [0, K] and for all local minimum point

(x ⋆ , i ⋆ , l ⋆ ) ∈ [0, R] × [[1, I]] × [0, K] of u -ϕ, we have:                  λϕ i⋆ (x ⋆ , l ⋆ ) + sup β i⋆ ∈B i⋆ -σ i⋆ (x ⋆ , l ⋆ , β i )∂ 2 x ϕ i⋆ (x ⋆ , l ⋆ )+ b i⋆ (x ⋆ , l ⋆ , β i )∂ x ϕ i⋆ (x ⋆ , l ⋆ ) + h i⋆ (x ⋆ , l ⋆ , β i ) ≥ 0, if (x ⋆ , l ⋆ ) ∈ (0, R) × (0, K), ∂ l ϕ(0, l ⋆ ) + inf ϑ∈O I i=1 S(θ i , l ⋆ , ϑ)∂ x ϕ i (0, l ⋆ ) + h 0 (l ⋆ , ϑ) ≤ 0, if x ⋆ = 0. l ⋆ ∈ (0, K), .
b) We say that u is a continuous viscosity sub solution of the W alsh (S) system [START_REF] Imbert | Generalized junction conditions for degenerate parabolic equations[END_REF], if for all test function ϕ ∈ C 2,0 0,1 N R × [0, K] and for all local maximum point

(x ⋆ , i ⋆ , l ⋆ ) ∈ [0, R] × [[1, I]] × [0, K] of u -ϕ, we have:                  λϕ i⋆ (x ⋆ , l ⋆ ) + sup β i⋆ ∈B i⋆ -σ i⋆ (x ⋆ , l ⋆ , β i )∂ 2 x ϕ i⋆ (x ⋆ , l ⋆ )+ b i⋆ (x ⋆ , l ⋆ , β i )∂ x ϕ i⋆ (x ⋆ , l ⋆ ) + h i⋆ (x ⋆ , l ⋆ , β i ) ≤ 0, if (x ⋆ , l ⋆ ) ∈ (0, R) × (0, K), ∂ l ϕ(0, l ⋆ ) + inf ϑ∈O I i=1 S(θ i , l ⋆ , ϑ)∂ x ϕ i (0, l ⋆ ) + h 0 (l ⋆ , ϑ) ≥ 0, if x ⋆ = 0. l ⋆ ∈ (0, K), .
c) We say that u is a continuous viscosity solution of the W alsh (S) system (7), if it is both a continuous viscosity supper and sub solution of the W alsh (S) system [START_REF] Imbert | Generalized junction conditions for degenerate parabolic equations[END_REF].

The main result of this work is the following Theorem:

Theorem 2.2. (Comparison Theorem.) Assume assumption (H). Let v ∈ C N R × [0, K] a continuous viscosity sub solution and u ∈ C N R × [0, K] a continuous viscosity
supper solution of the Walsh's spider HJB system -W alsh (S) -given in [START_REF] Imbert | Generalized junction conditions for degenerate parabolic equations[END_REF], satisfying the following boundary conditions:

∀i ∈ [[1, I]], ∀l ∈ [0, K], u i (R, l) ≥ v i (R, l), ∀i ∈ [[1, I]], ∀x ∈ [0, R], u i (x, K) ≥ v i (x, K).
Then we have:

∀(x, i, l) ∈ [0, R] × [[1, I]] × [0, K], u i (x, l) ≥ v i (x, l).

A short example for the construction of test functions in the linear case

As a short introduction of the method that will be used in this work to prove our main Theorem 2.2, we propose in this section for the convenience of the reader, a simple example in the linear framework.

     λu(x) -σ(x)∂ 2 x u(x) = 0, x ∈ (0, R), ∂ x u(0) = 0, u(R) = z, (8)
where λ > 0. σ ∈ C[0, R] is strictly positive (elliptic) and z ∈ R. We are going to give a simple sketch of proof for a comparison theorem.

Let f (and resp. g) be a supper (resp. sub) continuous viscosity solution of (8) (namely in the class C([0, R]) in the sens of Definition 2.1 adapted to the simple example ( 8)).

As explained in introduction, all our concentrations are focused on the behavior at the boundary x = 0, hence we will only show that the following assumption:

sup x∈[0,R] g(x) -f (x) = g(0) -f (0) > 0, (9)
will lead to a contradiction.

Let η > 0 and γ > 0 be two small parameters and ε ∈ (0, R) designed to drive the construction of the test functions at the neighborhood x = 0. Define ϕ = ϕ(ε, η, γ) the solution of the following ordinary differential equation:

     -∂ 2 x ϕ(x) + λf (x) σ(x) = -η, x ∈ (0, ε), ϕ(0) = 0, ϕ(ε) = f (ε) -f (0) -γ, , (10)
The solution satisfies:

∀x ∈ [0, ε], ϕ(x) = f (ε) -f (0) -γ + ∂ x ϕ(0)(x -ε) + x ε u 0 η + λf (z) σ(z) dzdu.
We are going to prove that ϕ is a test function of the supper solution f at x = 0. To obtain this fact, it is enough to show that the minimum of f -ϕ on the compact set [0, ε] is necessary reached at x = 0, and this is the case since:

-we have f (0) -ϕ(0) < f (ε) -ϕ(ε),

-and if the minimum of f -ϕ is reached at the interior of [0, ε], for instance at y ∈ (0, ε), because f is a supper solution we should have:

-ησ(y) = -σ(y)∂ 2 x ϕ(y) + λf (y) ≥ 0,
which is a contradiction (recall that η > 0 and σ(y) > 0). Therefore ϕ is a test function of the supper solution f at x = 0, and this implies:

∂ x ϕ(0) ≤ 0.
Using that ϕ(0) = 0, we get:

0 ≥ ∂ x ϕ(0)ε = f (ε) -f (0) -γ + 0 ε u 0 η + λf (z) σ(z) dzdu,
and therefore:

ε 0 u 0 η + λf (z) σ(z) dzdu ≥ f (ε) -f (0) -γ. (11)
Analogously for the sub solution g, we define ϕ = ϕ(ε, η, γ) the solution of the following ordinary differential equation:

     -∂ 2 x ϕ(x) + λg(x) σ(x) = η, x ∈ (0, ε), ϕ(0) = 0, ϕ = g(ε) -g(0) + γ, . (12)
The solution satisfies:

∀x ∈ [0, ε], ϕ(x) = g(ε) -g(0) + γ + ϕ(x -ε) + x ε u 0 -η + λg(z) σ(z) dzdu,
and with the same arguments behind, we can show that ϕ is a test function of the sub solution g at x = 0 (the maximum of g -ϕ on the compact set [0, ε] is necessary reached at x = 0). We get then:

∂ x ϕ(0) ≥ 0,
and therefore using that ϕ(0) = 0:

ε 0 u 0 -η + λg(z) σ(z) dzdu ≤ g(ε) -g(0) + γ. (13)
Now combining both ( 11) and ( 13), we obtain:

ε 0 u 0 -2η + λ g(z) -f (z)) σ(z) dzdu ≤ g(ε) -g(0) -f (ε) + f (0) + 2γ.
Sending γ ↘ 0 and η ↘ 0, we have:

lim sup η↘0 ε 0 u 0 -2η + λ g(z) -f (z)) σ(z) dzdu ≤ lim inf γ↘0 g(ε) -g(0) -f (ε) + f (0) + 2γ ,
which leads to:

ε 0 u 0 λ g(z) -f (z)) σ(z) dzdu ≤ g(ε) -g(0) -f (ε) + f (0).
Therefore as expected at the beginning of the sketch of proof, if we assume (9) that is:

sup x∈[0,R] g(x) -f (x) = g(0) -f (0) > 0,
we get:

ε 0 u 0 λ g(z) -f (z)) σ(z) dzdu ≤ 0.
Dividing by ε 2 we obtain:

1 ε 2 ε 0 u 0 λ g(z) -f (z)) σ(z) dzdu ≤ 0,
and finally sending ε ↘ 0:

lim ε↘0 1 ε 2 ε 0 u 0 λ g(z) -f (z)) σ(z) dzdu ≤ 0, we get: λ σ(0) g(0) -f (0) ≤ 0,
and this leads to a contradiction with the assumption (9) using that λ > 0 and the ellipticity condition at x = 0: (σ(0) > 0). We obtain therefore the result expected at the beginning of this sketch of proof.

Proof of Theorem 2.2

We state first the following Proposition, that will be useful for the construction of the test functions at the neighborhood of the vertex 0.

Proposition 4.1. Let r > 0 and (B, H) ∈ R 2 . Fix ε > 0, κ > 0 and (η, γ) ∈ R 2 , be four small parameters (ε, κ, |η|, |γ| << 1) (expected to be sent to 0.) Assume that ε is small enough in order to satisfy:

1 -|B|ε exp(|B|ε) > 0. ( 14
)
Let w κ and z ε,κ i i∈[[1,I]] be real bounded sequences indexed by (ε, κ):

∃w ≥ 0, ∃z ≥ 0, sup κ≥0 |w κ | ≤ w, max i∈[[1,I]] sup ε≥0 sup κ≥0 |z ε,κ i | ≤ z.
For a given ℓ ∈ (0, +∞) and S ≥ 0:

(i)-the following parametric ordinary differential equation posed on the domain

N ε × [ℓ - κ, ℓ + κ]:      rψ i (x, l) -∂ 2 x ψ i (x, l) + B|∂ x ψ i (x, l)| + H + η = 0, x ∈ (0, ε), l ∈ (ℓ -κ, ℓ + κ), ψ(0, l) = w κ + S(l -ℓ), ψ i (ε, l) = z ε,κ i + S(l -ℓ) + γ, l ∈ [ℓ -κ, ℓ + κ], , (15)
admits a unique solution:

ψ = ψ ε, κ, η, γ, S, w κ , z ε,κ i i∈[[1,I]] in the class C 2,0 0,1 N ε × [ℓ -κ, ℓ + κ] . (ii)-Fix β > 0.
As soon as we impose κ = κ ε small enough in order to verify

1 - β ε rκ exp(|B|ε) -1 -β rκ|B| exp(2|B|ε) 1 -|B|ε exp(|B|ε) > 0, ( 16
)
then there exists

S(β) = S β, ε, κ, η, γ, w κ , z ε,κ i i∈[[1,I]] ≥ 0 such that: ∀l ∈ [ℓ -κ, ℓ + κ], ∂ l ψ(0, l) = S(β) ≥ β ε |B||∂ x ψ| + |H| + |η| . (17)
(iii)-Assume moreover that the sequences w κ , z ε,κ i i∈[ [1,I]] satisfy:

∀i ∈ [[1, I]], lim ε↘0 lim sup κ↘0 z ε,κ i -w κ = 0.
Then for all β > 0 and the choice of the parameter

S(β) = S β, ε, κ, η, γ, w κ , z ε,κ i i∈[[1,I]]
satisfying [START_REF] Ohavi | Quasi-linear parabolic PDE posed on a network with nonlinear Neumann boundary condition at vertices[END_REF], the solution: sup

ψ = ψ ε, κ, η, γ, S(β), w κ , z ε,κ i i∈[[1,I]] = ψ ε,κ,η,γ β of (
l∈[ℓ-κ,ℓ+κ] 2 ε 2 ε 0 u 0 ψ ε,κ,η,γ i,β (z, l)dzdu -w κ = 0. ( 18
)
Proof. Fix for a while l ∈ [ℓ -κ, ℓ + κ], viewed as an external parameter. We obtain easily the unique solvability on each rays R ε,i := [0, ε] × {i}, i ∈ [ [1, I]] of (15) (using for instance the Corollary 1.9-II given in [START_REF] Granas | Nonlinear boundary value problems for ordinary differential equations[END_REF]). Remarking that the sequence w κ is independent of

i ∈ [[1, I]],
we obtain by extension the unique solvability in the class C 2 N ε .

Set

M = M (κ, γ, η, S) = w + z + κS + |γ| + |H| + |η| r . ( 19
)
It is easy to check that constant map x → M (resp. x → -M ) is a supper solution (resp.

sub solution) of ( 15), which implies that:

∀i ∈ [[1, I]], ∀(x, l) ∈ [0, ε] × [ℓ -κ, ℓ + κ], |ψ i (x, l)| ≤ M. ( 20
)
Since we have for all i ∈ [ [1, I]] and for all (x, l) ∈ (0, ε) × (ℓ -κ, ℓ + κ):

|∂ 2 x ψ i (x, l)| ≤ |B||∂ x ψ i (x, l)| + rM + |H| + |η|,
it follows from Grönwall's Lemma that for all (x, l) ∈ (0, ε) × (ℓ -κ, ℓ + κ):

|∂ x ψ i (x, l)| ≤ |∂ x ψ i (0, l)| exp(|B|ε) + rM + |H| + |η| |B| exp(|B|ε) -1 , (21)
(with the convention exp(|B|ε) -1 /|B| |B|=0 = ε).

Observe now that for all l ∈ (ℓ -κ, ℓ + κ) and for all i ∈ [[1, I]]:

γ + z ε,κ i -w κ = ε∂ x ψ i (0, l) + ε 0 u 0 rψ i (z, l) + B|∂ x ψ i (z, l)| + H + η dzdu, (22)
and therefore from ( 19), ( 20) and (22):

|∂ x ψ i (0, l)| ≤ 1 ε |γ + z ε,κ i -w κ | + ε exp(|B|ε) C 1 (κ, γ, η, S) + |B||∂ x ψ i (0, l)| , (23)
C 1 = C 1 (κ, γ, η, S) = r(w + z + κS + |γ|) + 2(|H| + |η|) (24)
From ( 23), we see that as soon as we impose ε small enough to get:

1 -|B|ε exp(|B|ε) > 0,
we obtain that for all l ∈ (ℓ -κ, ℓ + κ) and for all i ∈ [[1, I]]:

|∂ x ψ i (0, l)| ≤ 1 1 -|B|ε exp(|B|ε) 1 ε |γ + z ε,κ i -w κ | + C 1 ε exp(|B|ε) . ( 25
)
Since the sequences w κ and z ε,κ i are uniformly bounded and the parameter κ << 1 is small enough, we obtain clearly that the sequence ψ(•, l) l∈[ℓ-κ,ℓ+κ] is equicontinuous in the class C 2+α N ε (for some α ∈ (0, 1)), uniformly with respect to the parameter

l ∈ [ℓ -κ, ℓ + κ].
In other words:

sup l∈[ℓ-κ,ℓ+κ] ∥ψ(•, l)∥ C 2+α (Nε) ≤ C ε , (26)
where C ε ≥ 0 is a positive constant independent of κ.

Let us show that ψ and its first-second derivative are continuous with respect to variable l. For this purpose, let (l n ) be a sequence of [ℓ-κ, ℓ+κ] converging to l ∈ [ℓ-κ, ℓ+κ]. We deduce with the aid of ( 26), Ascoli's theorem and the boundary conditions, that ψ(•, l n )

will converge up to sub sequence in C 2+α N ε to a solution of [START_REF] Martinez | Martingale problem for a Walsh's spider diffusion with spinning measure selected from its own local time[END_REF], that is indeed ψ(•, l) by uniqueness. Therefore the map:

     [ℓ -κ, ℓ + κ] → C 2+α N ε l → ψ(•, l), , is continuous. We conclude that ψ is in the class C 2,0 0,1 N ε × [ℓ -κ, ℓ + κ] , since clearly l → ψ(0, l) ∈ C 1 [ℓ -κ, ℓ + κ] .
Let us show now [START_REF] Ohavi | Quasi-linear parabolic PDE posed on a network with nonlinear Neumann boundary condition at vertices[END_REF]. Fix β > 0. With the aid of ( 21) and (25), we have:

|∂ x ψ| = max i∈[[1,I]] sup |∂ x ψ i (x, l)|, (x, l) ∈ [0, ε] × [ℓ -κ, ℓ + κ] ≤ exp(|B|ε) 1 -|B|ε exp(|B|ε) max i∈[[1,I]] 1 ε |γ + z ε,κ i -w κ | + C 1 (κ, γ, η, S)ε exp(|B|ε) + C 1 (κ, γ, η, S) |B| exp(|B|ε) -1 , (27)
where we recall that C 1 = C 1 (κ, γ, η, S) is given in (24) by:

C 1 (κ, γ, η, S) = r(w + z + κS + |γ|) + 2(|H| + |η|).
Let choose κ ε > 0 small enough, such that for all κ ≤ κ ε :

1 - β ε rκ exp(|B|ε) -1 -β rκ|B| exp(2|B|ε) 1 -|B|ε exp(|B|ε) > 0.
We observe from (27) and the expression of the constant C 1 (κ, γ, η, S), that if we set the parameter S ≥ 0:

S = S(β) = S β, ε, κ, η, γ, w κ , z ε,κ i i∈[[1,I]] ≥ 0,
such that:

S(β) := β|B| ε exp(|B|ε) 1 -|B|ε exp(|B|ε) max i∈[[1,I]] 1 ε |γ + z ε,κ i -w κ | + C 2 (γ, η)ε exp(|B|ε) 1 - β ε rκ exp(|B|ε) -1 -β rκ|B| exp(2|B|ε) 1 -|B|ε exp(|B|ε) , + β|B| ε C 2 (γ, η) |B| exp(|B|ε) -1 1 - β ε rκ exp(|B|ε) -1 -β rκ|B| exp(2|B|ε) 1 -|B|ε exp(|B|ε) + β|B| ε |H| + |η|) (28)
with:

C 2 (γ, η) = r(w + z + |γ|) + 2(|H| + |η|). ( 29
)
we will obtain:

S(β) ≥ β ε |B||∂ x ψ| + |H| + |η| , namely (17)
holds true.

To conclude observe first that since both sequences w κ and z ε,κ i are uniformly bounded, we will obtain in (28) that the parameter:

S(β) = S β, ε, κ, η, γ, w κ , z ε,κ i i∈[[1,I]] = S β, ε, κ, η, γ
will satisfy:

lim sup κ↘0 lim sup η↘0 lim sup γ↘0 κS β, ε, κ, η, γ = 0. ( 30
) Let l ∈ [ℓ -κ, ℓ + κ]. Now for ψ = ψ ε,κ,η,γ β
, which satisfies:

∂ l ψ(0, l) = S β, ε, κ, η, γ , we have for all i ∈ [[1, I]] (recall that: ψ ε,κ,η,γ β (0, l) = w κ + S β, ε, κ, η, γ (l -ℓ)): 2 ε 2 ε 0 u 0 ψ ε,κ,η,γ i,β (z, l)dzdu -w κ ≤ 2 ε 2 ε 0 u 0 ψ ε,κ,η,γ i,β (z, l) -w κ + S β, ε, κ, η, γ (l -ℓ) dzdu + κS β, ε, κ, η, γ ≤ 1 2ε 2 ε 0 u 0 z 0 ∂ x ψ ε,κ,η,γ i,β (t)dtdzdu + κS β, ε, κ, η, γ ≤ ε 2 |∂ x ψ ε,κ,η,γ β | + κS β, ε, κ, η, γ . Hence if the sequences w κ , z ε,κ i i∈[[1,I]] satisfy: ∀i ∈ [[1, I]], lim ε↘0 lim sup κ↘0 z ε,κ i -w κ = 0,
we see from the expression given (27) and the convergence (30), that we will obtain:

lim sup ε↘0 lim sup κ↘0 lim sup η↘0 lim sup γ↘0 max i∈[[1,I]] sup l∈[ℓ-κ,ℓ+κ] 2 ε 2 ε 0 u 0 ψ ε,κ,η,γ i,β (z, l)dzdu -w κ = 0.
The proof is complete. □

We are able now to prove the central result of this work: Theorem 2.2.

Proof. Let f (and resp. g) be a supper (resp. sub) continuous viscosity solution of [START_REF] Freidlin | Diffusion processes on graphs: stochastic differential equations, large deviation principle[END_REF].

Fix in the sequel ℓ ∈ [0, K). We argue by contradiction assuming that:

sup g i (x) -f i (x), (x, i), l ∈ N R × [ℓ, K] > 0.
Since f and g are in the class C N R × [0, K] , using the boundary condition given in the assumptions of the Theorem, the last supremum is necessary reached at a point:

x ⋆ , i ⋆ , l ⋆ ∈ [0, R) × [[1, I]] × [ℓ, K).
Step 1: Classical arguments at the interior of each rays. Assume first that: x ⋆ > 0.

Let V(x ⋆ ) be a neighborhood of x ⋆ strictly included in the ray R i⋆ . When l ⋆ ∈ [ℓ, K) is fixed, the following Hamiltonian (parameterized by l ⋆ ) :

H l⋆ i⋆ :=            V(x ⋆ ) × R 3 → R (x, u, p.S) → λu + sup β i⋆ ∈B i⋆ -σ 2 i⋆ (x, l ⋆ , β i⋆ )S+ b i⋆ (x, l ⋆ , β i⋆ )p + h i⋆ (x, l ⋆ , β i⋆ ) , , is continuous because:
-linear in u, -convex in (p, S),

-assumption (H -R) states that all the coefficients (σ i , b i , h i ) i∈[ [1,I]] are Lipschitz continuous, uniformly in the control variables (β i ∈ B i ) i∈[ [1,I]] . This imply the Lipschitz continuity of H l⋆ i⋆ with respect to the variable x.

Moreover, we have that the classical assumptions introduced in the seminal work [START_REF] Crandall | User's guide to viscosity solutions of second order Partial Differential Equations[END_REF] (Theorem 3.3) hold true, which are:

(i) ∀(x, u, v, p, S) ∈ [0, R] × R 3 , if u ≥ v, then H l⋆ i⋆ (x, u, p, S) -H l⋆ i⋆ (x, v, p.S) ≥ λ(u -v), with λ > 0, (ii) ∃ω ∈ C(R + , R + ), ω(0) = 0, ∀α > 0, ∀(x, y, u, p, X, Y ) ∈ [0, R] 2 × R 4 , such that: -3α   1 0 0 1   ≤   X 0 0 -Y   ≤ 3α   1 -1 -1 1   , then : H l⋆ i⋆ (y, u, β(x -y).Y ) -H l⋆ i⋆ (x, u, α(x -y), X) ≤ ω α|x -y| 2 + |x -y| .
(Recall that the last property (ii) holds true since the coefficients

(σ i , b i , h i ) i∈[[1,I]] , are
Lipschitz continuous uniformly in the control variables (

β i ∈ B i ) i∈[[1,I]] -see Example 3.6
in [START_REF] Crandall | User's guide to viscosity solutions of second order Partial Differential Equations[END_REF] for instance -and l = l ⋆ is fixed).

Since the Hamiltonian H l⋆ i⋆ does not have any dependency with some derivative with respect to the variable l, we can proceed with the classical arguments of the theory of viscosity solution to obtain a contradiction, that are:

-applying the doubling variable method with the function (here parameterized by (i ⋆ .l ⋆ )) defined by :

∀ε > 0, w (i⋆.l⋆) ε (x, y) = g i⋆ (x, l ⋆ ) -f i⋆ (x, l ⋆ ) - 1 2ε 2 |x -y| 2 , (x, y) ∈ V i⋆ (x ⋆ ) × V i⋆ (x ⋆ ), (recall that V i⋆ (x ⋆ ) is a neighborhood of x ⋆ strictly included in R i⋆ ).
-use the Ishii's matrix lemma (see for example Theorem 3.2 in [START_REF] Crandall | User's guide to viscosity solutions of second order Partial Differential Equations[END_REF]). (Recall that H l⋆ i⋆ is continuous at the neighborhood of x ⋆ , which implies that the equivalent definition of a supper (resp. sub solutions) with the closure of the second-order supper jet (resp. sub jet) of f (resp. g) at x ⋆ holds true).

In the rest of this proof we assume that:

sup g i (x, l) -f i (x, l), (x, i), l ∈ N R × [ℓ, K] = g(0, l ⋆ ) -f (0, l ⋆ ) > 0, (31)
where we recall that:

l ⋆ ∈ [ℓ, K), ℓ ∈ (0, K).
Step 2: introduction of test functions depending on the speed of the Hamiltonians. We scale first f and g at the vertex 0. Set:

Θ(f, g) = 1 2 f (0, l ⋆ ) + g(0, l ⋆ ) .
It is easy to verify that:

u = f -Θ(f, g), v = g -Θ(f, g), (32)
are respectively supper solution and sub solution of the following system with non linear local time's Kirchhoff 's boundary transmission, posed on the domain N R × [0, K]:

                                     λw i (x, l) + λΘ(f, g) + sup β i ∈B i -σ i (x, l, β i )∂ 2 x w i (x, l)+ b i (x, l, β i )∂ x w i (x, l) + h i (x, l, β i ) = 0, (x, l) ∈ (0, R) × (0, K), ∂ l w(0, l) + inf ϑ∈O I i=1 S(θ i , l, ϑ)∂ x w i (l, 0) + h 0 (l, ϑ) = 0, l ∈ (0, K) w i (R, l) = χ i (l) -Θ(f, g), l ∈ [0, K], w i (x, K) = T i (x) -Θ(f, g), x ∈ [0, R] ∀(i, j) ∈ [[1, I]] 2 , ∀l ∈ [0, K], w i (0, l) = w j (0, l). (33)
Remark that:

u(0, l ⋆ ) = 1 2 f (0, l ⋆ ) -g(0, l ⋆ ) < 0, v(0, l ⋆ ) = 1 2 g(0, l ⋆ ) -f (0, l ⋆ ) > 0, v(0, l ⋆ ) -u(0, l ⋆ ) = g(0, l ⋆ ) -f (0, l ⋆ ) > 0. ( 34
)
In the sequel, drawing on the method introduced in the last Section 3, we will build in the neighborhood of (0, l ⋆ ) test functions for the supper solution u (resp. sub solution v) of (33) that will solve ordinary differential equations possessing only constant coefficients.

This coefficients may be viewed as a kind a supreme envelope of all possible first order errors of the speed of the Hamiltonians S peed (H i ), i ∈ [ [1, I]] defined by:

S peed (H i ) :=        [0, R] × [0, K] × R → R, (x, l, p) → sup β i ∈B i b i (x, l, β i )p + h i (x, l, β i ) σ i (x, l, β i ) ,
where the Hamiltonian H i , i ∈ [ [1, I]] are given by:

H i :=        [0, R] × [0, K] × R 3 → R,
(x, l, u, p, S) → λu + sup

β i ∈B i -σ i (x, l, β i )S + b i (x, l, β i )p + h i (x, l, β i ) .
The key point in the construction is to impose a derivative with respect to the 'local-time' variable l at x = 0 that will absorb all the errors induced by the Kirchhoff 's speed of the Hamiltonians, given by:

K f S peed :=        [0, R] × [0, K] × R → R, (x, l, p) → inf ϑ∈O I i=1
S(θ i , l, ϑ) sup

β i ∈B i b i (x, l, β i )p + h i (x, l, β i ) σ i (x, l, β i ) . (35)
Fix ε > 0 and κ > 0 two small parameters expected to be sent to 0. Using (34) and the continuity of u and v, there exists a neighborhood of the vertex (0, l ⋆ ) denoted by V (0, l ⋆ ), (ε, κ) and defined by:

V (0, l ⋆ ), (ε.κ) := (x, i), l ∈ N R × [ℓ, K], x ≤ ε, 0 < l ⋆ -κ ≤ l ≤ l ⋆ + κ < K ,
such that:

∀ (x, i), l ∈ V (0, l ⋆ ), (ε, κ) , v i (x, l) ≥ 0, u i (x, l) ≤ 0, v i (x, l) -u i (x, l) ≥ 0. ( 36
)
In the sequel we introduce also η > 0 and γ > 0 two small strictly positive parameters, designed to drive the construction of the test functions at the neighborhood of the vertex (0, l ⋆ ).

Set in the sequel:

t λ, Θ(f, g) = λΘ(f, g) 1 σ 1 Θ(f,g)>0 + 1 σ 1 Θ(f,g)≤0 , t λ, Θ(f, g) = λΘ(f, g) 1 σ 1 Θ(f,g)≤0 + 1 σ 1 Θ(f,g)>0 , (37)
u κ (0) = sup u(0, l), l ∈ [l ⋆ -κ, l ⋆ + κ] , ∀i ∈ [[1, I]], u κ i (ε) = inf u i (ε, l), l ∈ [l ⋆ -κ, l ⋆ + κ] , v κ (0) = inf v(0, l), l ∈ [l ⋆ -κ, l ⋆ + κ] , ∀i ∈ [[1, I]], v κ i (ε) = sup v i (ε, l), l ∈ [l ⋆ -κ, l ⋆ + κ] , (38)
                   λ σ ϕ i -∂ 2 x ϕ i (x, l) + t λ, Θ(f, g) + |b||∂ x ϕ i (x, l)| + |h| σ = -η, (x, l) ∈ (0, ε) × (l ⋆ -κ, l ⋆ + κ), ϕ(0, l) = u κ (0) + S(l -l ⋆ ), ϕ i (ε, l) = u κ i (ε) -γ + S(l -l ⋆ ), l ∈ [l ⋆ -κ, l ⋆ + κ], i ∈ [[1, I]]. , (39)
and:

                   λ σ ϕ i -∂ 2 x ϕ i (x, l) + t λ, Θ(f, g) -|b||∂ x ϕ i (x, l)| + |h| σ = η, (x, l) ∈ (0, ε) × (l ⋆ -κ, l ⋆ + κ), ϕ(0, l) = v κ (0) -S(l -l ⋆ ), ϕ i (ε, l) = v κ i (ε) + γ -S(l -l ⋆ ), l ∈ [l ⋆ -κ, l ⋆ + κ], i ∈ [[1, I]].
.

Assumption (H) combined with Proposition 4.1 state that both solutions ϕ and ϕ are unique and in the class of test functions

C 2,0 0,1 N ε × [l ⋆ -κ, l ⋆ + κ] .
Step 3: ϕ (resp. ϕ) is a test function of the supper solution u (resp. the sub solution v) at the vertex 0 of the Walsh's spider HJB system (33).

We start to show that ϕ is a test function of the supper solution u at 0 of the HJB system (33). The second case involving ϕ for the sub solution v can be treated with the same arguments.

We are then going to show that the minimum of u-ϕ on the domain

N ε ×[l ⋆ -κ, l ⋆ +κ],
is necessarily reached at some point (0, l κ ) with l κ ∈ [l ⋆ -κ, l ⋆ + κ]. Using the boundary conditions satisfied by ϕ and the expressions given in (37), we obtain that ∀i ∈ [[1, I]] and

∀l ∈ [l ⋆ -κ, l ⋆ + κ]: u(0, l) -ϕ(0, l) = u(0, l) -u κ (0) -S(l -l ⋆ ) ≤ -S(l -l ⋆ ), ∀i ∈ [[1, I]], u i (ε, l) -ϕ i (ε, l) = u i (ε, l) -u κ i (ε) -S(l -l ⋆ ) + γ > -S(l -l ⋆ ),
which implies that the minimum of u -ϕ can not be reached at (

x = ε, l) with l ∈ [l ⋆ -κ, l ⋆ + κ].
Assume now that minimum of u -ϕ is reached at some point

y, j, ℓ ∈ (0, ε) × [[1, I]] × [l ⋆ -κ, l ⋆ + κ].
As it is classical in the viscosity formulation, we can without lose of generality assume that:

u j (y, ℓ) = ϕ j (y, ℓ).
Since u is a supper solution of the system (33), we have by definition (recall that 0 < l ⋆ -κ < l ⋆ + κ < K):

λu j (y, ℓ) + λΘ(f, g)+ sup β j ∈B j -σ j (y, ℓ, β j )∂ 2 x ϕ j (y, ℓ) + b j (y, ℓ, β j )∂ x ϕ j (y, ℓ) + h j (y, ℓ, β j ) ≥ 0. ( 41
)
Hence using the expression of the system of ordinary differential equation (39) satisfied by ϕ we get: λu j (y, ℓ) + λΘ(f, g) + sup

β j ∈B j -σ j (y, ℓ, β j )η -σ j (y, ℓ, β j ) λu j (y, ℓ) σ -σ j (y, ℓ, β j )t λ, Θ(f, g) -σ j (y, ℓ, β j ) |b||∂ x ϕ j (y, ℓ)| + |h| σ + b j (y, ℓ, β j )∂ x ϕ j (y, ℓ) + h j (y, ℓ, β j ) ≥ 0. ( 42
)
Using now that η > 0, u j (y, ℓ) ≤ 0 (see (36)), the expression of t λ, Θ(f, g) given in (37)

and the central ellipticity condition satisfied by the coefficient σ j (assumption H -E), we get that the last quantity (42) is smaller than:

λu j (y, ℓ) + sup β j ∈B j {-σ j (y, ℓ, β j ) λu j (y, ℓ) σ } + λΘ(f, g) + sup β j ∈B j {-σ j (y, ℓ, β j )t λ, Θ(f, g) } + |b||∂ x ϕ j (y, ℓ)| + |h| -|b||∂ x ϕ j (y, ℓ)| + |h| + sup β j ∈B j {-σ j (y, ℓ, β j )η} ≤ -ση < 0,
and that leads to a contradiction with (41). We conclude that ϕ is a test function of the supper solution u at the vertex 0, namely there exists l κ ∈ [l ⋆ -κ, l ⋆ + κ] such that:

∂ l ϕ(0, l κ ) + inf ϑ∈O I i=1 S(θ i , l κ , ϑ)∂ x ϕ i (0, l κ ) + h 0 (l κ , ϑ) ≤ 0. ( 43
)
As announced at the beginning of this Step, using the same arguments, we can show easily that ϕ is a test function of the sub solution v at 0, namely there exists

l κ ∈ [l ⋆ -κ, l ⋆ + κ]
such that:

∂ l ϕ(0, l κ ) + inf ϑ∈O I i=1 S(θ i , l κ , ϑ)∂ x ϕ i (0, l κ ) + h 0 (l κ , ϑ) ≥ 0. ( 44
)
Step

S = S(ζ, ε, κ, η, γ) = S ζ, ε, κ, |t λ, Θ(f, g) | + η, |h|, |∂ x ϕ|, u κ (0), u κ i (ε) i∈[[1,I]] , S = S(ζ, ε, κ, η, γ) = S ζ, ε, κ, |t λ, Θ(f, g) | + η, |h|, |∂ x ϕ|, v κ (0), v κ i (ε) i∈[[1,I]] ,
such that:

∂ l ϕ(0, l κ ) = S(ζ, ε, κ, η, γ) ≥ Iζ ε |t λ, Θ(f, g) | + η + |b||∂ x ϕ| + |h| σ , (45)
∂ l ϕ(0, l κ ) = S(ζ, ε, κ, η, γ) ≥ Iζ ε |t λ, Θ(f, g) | + η + |b||∂ x ϕ| + |h| σ . (46)
Recall that ζ is given in assumption (H-R), and we have denoted for w ∈ C

κ ∈ [l ⋆ -κ, l ⋆ + κ] and l κ ∈ [l ⋆ -κ, l ⋆ + κ],
we have:

lim κ↘0 l κ = l ⋆ , lim κ↘0 l κ = l ⋆ (47)
and from the expressions given in (37) and the continuity of u and v we get:

∀i ∈ [[1, I]], lim ε↘0 lim sup κ↘0 v κ i (ε) = v(0, l ⋆ ), lim ε↘0 lim sup κ↘0 u κ i (ε) = u(0, l ⋆ ), lim κ↘0 v κ (0) = v(0, l ⋆ ), lim κ↘0 u κ (0) = u(0, l ⋆ ). (48)
Using ( 31) and (32), we know that for all i ∈ [[1, I]]:

u i (ε, l ⋆ ) -u(0, l ⋆ ) -v i (ε, l ⋆ ) + v(0, l ⋆ ) = f i (ε, l ⋆ ) -f (0, l ⋆ ) -g i (ε, l ⋆ ) + g(0, l ⋆ ) ≥ 0.
Hence we deduce that for all i ∈ [[1, I]]:

lim κ↘0 u κ i (ε) -u κ (0) -v κ i (ε) + v κ (0) ≥ 0,
and therefore:

∃κ ε > 0, ∀κ ≤ κ ε , u κ i (ε) -u κ (0) -v κ i (ε) + v κ (0) ≥ -ε 3 . (49)
From the expressions of the ordinary differential equations (39)-(40) satisfied by that ϕ and ϕ, we obtain: In the end we get: 0 ≥ Iζ λ σ (v(0, l ⋆ ) -u(0, l ⋆ )).

∂ x ϕ i (0, l κ ) = - γ ε + 1 ε u κ i (ε) -u κ (0) - ε 0 u 0 λϕ i (z, l κ ) σ dzdu - ε 0 u 0 t λ, Θ(f, g) + |b||∂ x ϕ i (z, l κ )| + |h| σ + η dzdu , ∂ x ϕ i (0, l κ ) = γ ε + 1 ε v κ i (ε) -v κ (0) - ε 0 u 0 λϕ i (z, l κ ) σ dzdu
Therefore (32) imply 0 ≥ g(0 , l ⋆ ) -f (0, l ⋆ ), and that leads to a contradiction with (31). We conclude that for all ℓ ∈ (0, K), for all (x, i) ∈ N R and for all l ∈ [ℓ, K]:

f i (x, l) ≥ g i (x, l).
We conclude the proof using the continuity of f and g with respect to variable l. □

  [START_REF] Freidlin | Diffusion processes on graphs: stochastic differential equations, large deviation principle[END_REF]. More precisely, given I pairs (σ i , b i ) i∈I of mild coefficients of diffusion from [0, +∞) to R satisfying the following condition of ellipticity: ∀i ∈ [[1, I]], σ i > 0, and given α 1 , . . . , α I ) positive constants satisfying I i=1

(

  where Ω denotes a smooth open set of R n ) can be stated in the strong sense namely using only the Neumann condition N (•) at the boundary for both upper and sub solutions, or in the classical sense with both terms N (•) and H(•), considering at the boundary ∂Ω the term N (•) ∧ H(•) for sub solutions and N (•) ∨ H(•) for supper solutions (see Section 7 in [5]

  Consider the following elliptic linear PDE posed on the open set (0, R), with Neumann boundary condition at x = 0 and Dirichlet boundary condition at x = R:

  Let S ≥ 0 and S ≥ 0 be two parameters designed to characterize the 'local-time' derivative of the tests functions at 0. Using Proposition 4.1, we introduce ϕ = ϕ(u, ε, η, γ, S), ϕ = ϕ(v, ε, η, γ, S) (denoted in the next lines lines ϕ, ϕ for the seek of clarity) the two solutions of the two following ordinary parametric differential equation systems posed on N ε × [0, κ]

3 :

 3 Conclusion. Fix ϑ ∈ O. Without loss of generality, in the construction of the tests functions in Step 1 and the results obtained in Step 2, we know from Proposition 4.1, that for ε << 1, κ << 1, there exists

0 -00-ε 2 ε 2 ε 2 ε 2

 02222 Θ(f, g) -|b||∂ x ϕ i (z, l κ )| + |h| σ -η dzdu ∂ l ϕ(0, l κ ) = S(ζ, ε, κ, η, γ), ∂ l ϕ(0, l κ ) = -S(ζ, ε, κ, η, γ). (50)Now we have the necessary tools to conclude. Recall that ϑ ∈ O is fixed. Write:∂ l ϕ(0, l κ ) + I i=1 S(θ i , l κ , ϑ)∂ x ϕ i (0, l κ ) + h 0 (l κ , ϑ)-∂ l ϕ(0, l κ ) + I i=1 S(θ i , l κ , ϑ)∂ x ϕ i (0, l κ ) + h 0 (l κ , ϑ) = S(ζ, ε, κ, η, γ) -I i=1 S(θ i , l κ , ϑ) Θ(f, g) + |b||∂ x ϕ i (z, l κ )| + |h| σ + η dzdu + S(ζ, ε, κ, η, γ)t λ, Θ(f, g) + |b||∂ x ϕ i (z, l κ )| + |h| σ + η dzdui , l κ , ϑ) u κ i (ε) -u κ (0) -v κ i (ε) + v κ (0i , l κ , ϑ) -S(θ i , l κ , ϑ) v κ i (ε) -v κ (0) + h 0 (l κ , ϑ) -h 0 (l κ , ϑ)+ I i=1 S(θ i , l κ , ϑ) λϕ i (z, l κ ) σ dzdu -I i=1 S(θ i , l κ , ϑ) λϕ i (z, l κ ) σ dzdu.Now using (45)-(46)-(49), together with assumption (H -R) we obtain that there exists∃κ ε > 0, ∀κ ≤ κ ε : ∂ l ϕ(0, l κ ) + I i=1 S(θ i , l κ , ϑ)∂ x ∂ x ϕ i (0, l κ ) + h 0 (l κ , ϑ)-∂ l ϕ(0, l κ ) + I i=1 S(θ i , l κ , ϑ)∂ x ϕ i (0, l κ ) + h 0 (l κ , ϑ) Iζ -2|v|Iζ ε |l κ -l κ | -|h||l κ -l κ | z, l κ ) σ dzdu. (51)Taking now the infimum over all the ϑ ∈ O in (51), we obtain with aid of (43) and (44):0 ≥ -γ ε 2Iζ -ε 2 Iζ -2|v|Iζ ε |l κ -l κ | -|h||l κ -l κ | all n > 0, there exists ϑ n = ϑ n (ε, κ, η, γ) such that: |l κ -l κ | -|l κ -l κ |i , l κ , ϑ n )i (z, l κ ) -v κ (0) i , l κ , ϑ n ) i (z, l κ ) -u κ (0) |l κ -l κ | -2 ε |h||l κ -l κ | -2 nε = 0.Secondly, from (34) and (48), we obtain that in (54) (because v κ (0) ≥ 0, and u κ (0) ≤ 0i , l κ , ϑ n )i , l κ , ϑ n ) ≥ Iζ λ σ v(0, l ⋆ ) -u(0, l ⋆ ) .Finally, for the term (55), since the boundary condition of ϕ = (ε, κ, η, γ), ϕ = (ε, κ, η, γ) satisfy the point (iii) of Proposition 4.1, namely (see (48)):∀i ∈ [[1, I]], lim l κ ) -u κ (0) σ dzdu = 0.


domain: info math

text:
Mathieu D'aquin
email: mathieu.daquin@loria.fr

Jean Lieber
email: jean.lieber@loria.fr

Combining Representation Formalisms for Reasoning upon Mathematical Knowledge

Keywords: knowledge modeling, knowledge representation, mathematical knowledge

Knowledge in mathematics (definitions, theorems, proofs, etc.) is usually expressed in a way that combines natural language and mathematical expressions (e.g. equations). Using an ontology formalism such as OWL DL is well-suited for formalizing the natural language part, but complex mathematical expressions can be better handled by symbolic computation systems. We examine this representation issue and propose an original extension of OWL DL by call formulas, i.e., formulas from which assertions can be drawn thanks to calls to external functions. Using this formalism makes it possible to classify a mathematical problem defined by its relations to instances and classes and by some mathematical expressions: if a theorem for solving this problem is represented in the knowledge base, it can be retrieved, and thus, the problem can be solved by applying this theorem. We describe an inference algorithm and discuss its properties as well as its limitations. Indeed, the proposed extension, algorithm, and implementation represent a first step towards a combined formalism for representing mathematical knowledge, with some open issues regarding the representation of more complex problems: the resolution of multiscale, multiphysics cases in physics are foreseen.

INTRODUCTION

Knowledge representation usually starts with deciding on a formalism to be used. Different languages and paradigms might indeed be better suited for certain tasks or certain types of knowledge [START_REF] Brachman | Knowledge Representation and Reasoning[END_REF]. Description logics and ontologies, for example, are more often used to represent conceptual knowledge, for reasoning tasks such as classification, and in contexts where the exchange of knowledge and interoperability are important. In other cases, other logics or approaches focused on computational aspects can be favored. However, in relatively complex domains, multiple representation formalisms might be required to fully capture the knowledge needed for a given task.

This work originates from a project in such a domain, as a collaboration between physicists, mathematicians, and computer scientists in modeling the physical properties and behavior of arrays of micro-mirrors (see, for example, [START_REF] Md Canonica | The twodimensional array of 2048 tilting micromirrors for astronomical spectroscopy[END_REF]). Arrays of micro-mirrors are optical devices permitting the development of breakthrough instruments for Earth and Universe Observation. These components are made of a high number of micron-scale tiltable mirrors and are controlled electrostatically. Predicting the actual position of each mirror with respect to the behavior of the neighboring mirrors is a complex case involving multiscale, multiphysics systems. These issues have been addressed thanks to the mathematical principles of asymptotic analysis of partial differential equations, and have been studied through term rewriting tools in order to represent both knowledge of the models and of the computations applicable to them [START_REF] Belkhir | A tool for aided multi-scale model derivation and its application to the simulation of a micro mirror array[END_REF][START_REF] Belkhir | Towards an automatic tool for multi-scale model derivation illustrated with a micro-mirror array[END_REF][START_REF] Nguyen | A multi-scale model of a micro-mirror array and an automatic model derivation tool[END_REF].

However, there are a number of aspects for which symbolic computation formalisms are insufficient (or inefficient). These specific aspects relate mostly to knowledge useful to recognize the situations in which specific computations are needed, particular resolution strategies should be applied, or a given theorem holds. The goal of this study is to examine how to organize mathematical knowledge in order to be able to select relevant modules (representing, for example, theorems) of a symbolic computation system, when a mathematical problem is raised (it is noteworthy that the goal is not to reason within mathematical knowledge).

To illustrate this, we consider (here and in the rest of this paper) an example simpler than the differential equations eventually targeted by this approach: the resolution of a second-degree polynomial equation such as 2𝑥 2 + 3𝑥 + 1 = 0. There are different methods to achieve this, which might apply in different cases, and even before starting to solve it, a system aiming to support the resolution of mathematical problems would first have to recognize that the aforementioned expression: 1-is an equation, 2-is a polynomial equation, 3-is a polynomial equation of degree 2. It might then, for example, calculate the discriminant of the equation to determine whether it has one, two, or no real solutions.

Even for such a simple example, the knowledge manipulated can be seen as having some conceptual aspects (a polynomial equation is a kind of equation, a second-degree polynomial equation, a.k.a. a quadratic equation, has a discriminant, etc.) and some computational aspects (how to obtain the degree of a polynomial equation, how to calculate the discriminant of a quadratic equation, etc.).

In this paper, we present a logic (OWL DL call ) to combine knowledge representation formalisms, which we design as an extension of the description logic underlying OWL DL [START_REF] Motik | OWL 2 web ontology language profiles[END_REF] with calls to external symbolic computation engines. While calls to external functions have been present in knowledge representation systems in the past (see, for example, [START_REF] Brachman | KL-ONE reference manual[END_REF]), our extension is designed to enable an inference algorithm, which is described here with a discussion on its formal properties. We also discuss the proposed implementation of this algorithm, illustrated with a simple example in mathematics using a popular symbolic computation tool (the Sympy Python library 1 ). It shows that the current version of OWL DL call , as a first attempt to combine multiple representation formalisms for mathematical knowledge, can already handle a large class of problems. We, however, also discuss its limitations and the way in which it will need to evolve in order to support more complex problems.

After a reminder on OWL DL ( §2), an example of a representation of a simple mathematical problem is detailed ( §3), leading to a new representation formalism ( §4). The paper ends with a discussion and a conclusion ( §5).

BACKGROUND ON OWL DL

This paper uses and extends the description logic SROIQ (D) that is assimilated to the W3C recommendation OWL DL in its version 2. In this section, only a fragment of this logic is presented, restricted to the needs of the paper.

Throughout the paper, classical notions in mathematics are used. In particular, N and R are the sets of natural numbers and real numbers,

N * = N \ {0}, R * = R \ {0}, and ⟦𝑎, 𝑏⟧ = 𝑛 ∈ N 𝑎 ≤ 𝑛 ≤ 𝑏 for 𝑎, 𝑏 ∈ N.

Concrete domains (datatypes).

Concrete domains in OWL DL corresponds to XML schema built-in datatypes, e.g. bool, float, unsigned int, etc. With 𝜏 one of these datatypes, the concrete domain associated to 𝜏 is given by the ordered pair (Δ 𝜏 , Φ 𝜏 ) where Δ 𝜏 is the set of values of type 𝜏 (e.g. Δ unsigned int = N) and Φ 𝜏 is a countable set of symbols that represent some subsets of Δ 𝜏 : for 𝜎 ∈ Φ 𝜏 , this subset of Δ 𝜏 is denoted by 𝜎 𝜏 . In particular, if 𝑣 ∈ Δ 𝜏 , {𝑣} ∈ Φ 𝜏 represents the singleton {𝑣} 𝜏 = {𝑣 }, and ⊤ 𝜏 ∈ Φ 𝜏 represents the set of all values of the concrete domain: (⊤ 𝜏 ) 𝜏 = Δ 𝜏 .

Syntax

Four pairwise disjoint and countable sets of symbols are assumed to be given: AC (set of atomic concepts, a.k.a. atomic classes), OP (set of object properties, a.k.a. roles), DP (set of datatype properties), and I𝑛𝑠 (set of instances). Moreover, each datatype property 𝑝 ∈ DP is associated to a datatype 𝜏 called range of 𝑝; 𝑝 is called a 𝜏-property in the following. Finally, a property is an element of OP ∪ DP.

A concept is either an atomic concept or an expression of one of the following forms (where 𝐶 and 𝐷 are concepts, 𝑟 ∈ OP, 𝑎 1 , 𝑎 2 , . . . , 𝑎 𝑛 ∈ I𝑛𝑠, 𝑝 is a 𝜏-property, and 𝜎 ∈ Φ 𝜏 ): ⊤, ⊥, 𝐶 ⊓ 𝐷, ∃𝑟 .𝐶, (≤ 1 𝑟 ), {𝑎 1 , 𝑎 2 , . . . , 𝑎 𝑛 }, ∃𝑝.𝜎. The notation (= 1 𝑟 ) is used as an abbreviation for (≤ 1 𝑟 ) ⊓ ∃𝑟 .⊤.

A formula of OWL DL is either a terminological formula (usually expressing general knowledge) or an assertion (usually expressing ground facts). A terminological formula is an expression of one of the following forms (𝐶 and 𝐷 are concepts, 𝑝 1 and 𝑝 2 are properties): 𝐶 ⊑ 𝐷, 𝐶 ≡ 𝐷, and 𝑝 1 ⊑ 𝑝 2 . An assertion is an expression of one of the following forms (𝐶 is a concept, 𝑟 is an object property, 𝑎 and 𝑏 are two instances, 𝑝 is a 𝜏-property, and 𝑣 ∈ Δ 𝜏 ): 𝐶 (𝑎), 𝑟 (𝑎, 𝑏), 𝑝 (𝑎, 𝑣).

Semantics

An interpretation I is an ordered pair (Δ I , • I ) where Δ I is a nonempty set and • I maps:

• An atomic concept 𝐴 to a subset 𝐴 I of Δ I ,

• An object property 𝑟 to a subset 𝑟 I of Δ I × Δ I (i.e. 𝑟 I is a binary relation on Δ I ), • A 𝜏-property 𝑝 to a partial function 𝑝 I : Δ I → Δ 𝜏 , and • An instance 𝑎 to an element 𝑎 I of Δ I .

• I is extended on all concepts as follows: • An ontology is a knowledge base containing only terminological formulas.

⊤ I = Δ I ⊥ I =
I |= 𝐶 ⊑ 𝐷 if 𝐶 I ⊆ 𝐷 I , • I |= 𝐶 ≡ 𝐷 if 𝐶 I = 𝐷 I , • I |= 𝑝 1 ⊑ 𝑝 2 if 𝑝 I 1 ⊆ 𝑝 I 2 , • I |= 𝐶 (𝑎) if 𝑎 I ∈ 𝐶 I , • I |= 𝑟 (𝑎, 𝑏) if (𝑎 I , 𝑏 I ) ∈ 𝑟 I , • I |= 𝑝 (𝑎, 𝑣) if (𝑎 I , 𝑣) ∈ 𝑝 I . A knowledge

Some practical notations

The following notions do not add to the expressivity of the logic but are useful for giving readable notations and are used in the remainder of the paper.

Domains.

Let 𝑟 be an object property, and 𝐷 be a concept. The sentence "𝐷 is a domain of 𝑟 " expresses informally the formula ∃𝑟 .⊤ ⊑ 𝐷. Therefore, the fact that an interpretation I satisfies this formula means that, for 𝑥, 𝑦 ∈ Δ I , if (𝑥, 𝑦) ∈ 𝑟 I then 𝑥 ∈ 𝐷 I . 𝐷 is qualified as a domain of 𝑟 . In general, there is no unicity of the domain of a property: if 𝐷 is a domain of 𝑟 and if 𝐸 is a superconcept of 𝐷 (i.e. 𝐷 ⊑ 𝐸 is entailed by the current ontology) then 𝐸 is also a domain of 𝑟 .

Similarly, the sentence "𝐷 is a domain of 𝑝", for a 𝜏-property 𝑝 expresses informally the formula ∃𝑝.⊤ 𝜏 ⊑ 𝐷, and 𝐷 is qualified as a domain of 𝑝.

Functional object property. Let 𝑟 be an object property. The sentence "𝑟 is functional" expresses informally the formula ⊤ ⊑ (≤ 1 𝑟 ). Therefore, the fact that an interpretation I satisfies this formula means that, for 𝑥, 𝑦 1 , 𝑦 2 ∈ Δ I , if (𝑥, 𝑦 1 ) ∈ 𝑟 I and (𝑥, 𝑦 2 ) ∈ 𝑟 I then

𝑦 1 = 𝑦 2 .
It is recalled that, in this paper, we consider every datatype property as functional.

Property chains. A property chain is an expression of the form 𝑟 1 ;𝑟 2 ; . . . ;𝑟 𝑛 ;𝑝 (with 𝑛 ∈ N) where 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑛 are object properties and 𝑝 is a property. The first purpose of this notion in this paper is to be used as a syntactic abbreviation for some assertions. Let 𝑎 be an instance and 𝑣 be an instance if 𝑝 is an object property, or an element of Δ 𝜏 if 𝑝 is a 𝜏-property. Then, that 𝑎 is related to 𝑣 by the property chain 𝑟 1 ;𝑟 2 ; . . . ;𝑟 𝑛 ;𝑝 can be expressed as

(∃𝑟 1 .∃𝑟 2 . . . . ∃𝑟 𝑛 .∃𝑝.{𝑣})(𝑎)
For the sake of readability, this assertion is abbreviated by (𝑟 1 ;𝑟 2 ; . . . ;𝑟 𝑛 ;𝑝)(𝑎, 𝑣)

Let 𝑝𝑐 = 𝑟 1 ;𝑟 2 ; . . . ;𝑟 𝑛 ;𝑝. A concept 𝐷 is a domain of 𝑝𝑐 if 𝐷 is a domain of 𝑟 1 if 𝑛 ≥ 1, and of 𝑝 if 𝑛 = 0.
If 𝑝 is a 𝜏-property then the range of 𝑝𝑐 is 𝜏, and, for an interpretation I, (𝑝𝑐) I denotes the set of (𝑥, 𝑣) ∈ Δ I × Δ 𝜏 such that 𝑥 is related to 𝑣 by the composition of 𝑟 I 1 , 𝑟 I 2 , . . . , 𝑟 I 𝑛 , and 𝑝 I .

A SIMPLE EXAMPLE

This section shows how to represent the concept corresponding to the problem of solving a second-degree equation, as well as two methods to solve instances of such a problem in our framework. By "represent", what is meant here is to describe it in a way that enables recognizing a particular problem to correspond to the resolution of a second degree equation and infer the method(s) which can be used to solve it. This simple example is here to point out modeling and representation issues, without the need to understand complex mathematics.

Definitions and theorems related to second degree equations

In this section, the notions to be represented are highlighted by bold italics typesetting.

Definitions. Solving an equation is a problem consisting in finding the (possibly empty and possibly infinite) set of bindings of the unknowns of an equation that satisfy the equality given by the equation. A second degree equation on R is an equation with one unknown, say 𝑥, of the form 𝑃 (𝑥) = 𝑄 (𝑥) where 𝑃 and 𝑄 are two polynomials such that the degree of the polynomial 𝑄 -𝑃 is equal to 2.

Here is an example of a second degree equation solving problem: Solve an equation of second degree

𝑥 2 + 2 = -3𝑥
an equality of the form 𝑃 (𝑥 ) = 𝑄 (𝑥 )

with unknown 𝑥 a problem of solving an equation of second degree [START_REF] Belkhir | A tool for aided multi-scale model derivation and its application to the simulation of a micro mirror array[END_REF] The solution of this equation is

𝑆 = {{𝑥 = -2}, {𝑥 = -1}}.
Here is another example of a second degree equation solving problem:

Solve 𝑡 2 + 4𝑡 + 1 = 0 with unknown 𝑡 (2)
The solution of this equation is

𝑆 = {{𝑡 = -2 - √ 3}, {𝑡 = -2 + √ 3}}.
Two methods for solving a second degree equation are presented below. The first one is simpler but is not complete, in the sense that it can fail: it succeeds for the problem (1) but fails for the problem (2). The second one is complete but is (a little bit) less simple. In both methods, the unknown is denoted by 𝑥 and the equality is of the form 𝑃 (𝑥) = 𝑄 (𝑥). Let 𝑅 = 𝑄 -𝑃: the equality is then equivalent to 𝑅(𝑥) = 0. Let (𝑎, 𝑏, 𝑐) ∈ R 3 such that 𝑅 = 𝑎𝑋 2 + 𝑏𝑋 + 𝑐 (with 𝑎 ≠ 0 since the degree of the equation is 2). A precondition for applying both methods is that it is established that this equation is a second degree equation.

The first method is called find an obvious solution. It consists in the following steps: (S1) For 𝑥 1 ∈ {-2, -1, 0, 1, 2} perform the test 𝑅(𝑥 1 ) = 0. (S2) If all the answers to this test are false then the method fails. (S3) Otherwise, with 𝑥 1 the smallest value satisfying this test, let

𝑥 2 = -𝑏 𝑎 -𝑥 1 .
Then, the solution is 𝑆 = {{𝑥 = 𝑥 1 }, {𝑥 = 𝑥 2 }}. The theorem associated with this method states that when this method does not fail, its result is the actual solution of the equation.

The second method is called use the discriminant. It consists in the following steps:

(S1) Compute Δ = 𝑏 2 -4𝑎𝑐. (S2) If Δ < 0 then the solution is 𝑆 = ∅. (S3) Otherwise, 𝑆 = 𝑥 = -𝑏 - √ Δ 2𝑎 , 𝑥 = -𝑏+ √ Δ 2𝑎 (if Δ = 0, 𝑆 contains one binding if Δ > 0, 𝑆 contains two bindings).

Partial representation in description logic

In this section, the notions and statements involved in the resolution of a second degree equation are partially represented in the description logic OWL DL. For the sake of simplicity, we use our own vocabulary, even though we could have used established ontologies for representing mathematical notions [START_REF] Lange | Ontologies and languages for representing mathematical knowledge on the semantic web[END_REF]. First, the general knowledge expressed by terminological formulas is presented:

• Solving an equation is a problem and it is associated with an equation.

1. EquationSolving ⊑ Problem ⊓ ∃hasEquation.Equation

• An equation with one real unknown is an equation that has exactly one unknown such that this unknown is of type real.

2.

Equation1RealUnknown ≡ Equation ⊓ (= 1 hasUnknown) ⊓ ∃hasUnknown.∃hasType.{real}

• A polynomial equation is necessarily an equation with one real unknown.

PolynomialEquation ⊑ Equation1RealUnknown

• An equation of second degree is a polynomial equation of degree 2. 2 4. Equation2ndDegree ≡ PolynomialEquation ⊓ ∃degree.{2}

• The method based on finding an obvious solution suited to the equation of second degree can be tried.

5.

EquationSolving ⊓ ∃hasEquation.Equation2ndDegree ⊑ ∃hasSolvingMethod.{findObviousSolEqDeg2}

• The method based on a discriminant for solving an equation of second degree can be tried.

6.

EquationSolving ⊓ ∃hasEquation.Equation2ndDegree ⊑ ∃hasSolvingMethod.{useDiscriminant}

Then, the two problems of the previous section are described by assertions:

• The first problem is a problem of solving equations.

EquationSolving(pb1)

• This problem is associated to an equation with one real unknown. 8. hasEquation(pb1, eq1) 9. Equation1RealUnknown(eq1) • This equality is based on the equality 𝑥 2 + 2 = -3𝑥 and its unkown's name is "𝑥". 10. hasEquality(eq1, "x ** 2 + 2 = -3 * x") 11. (hasUnknown;hasName)(eq1, "x")

• For the other problem, pb2, the assertions are the same, after substitutions of pb1 with pb2 and eq1 with eq2, with the exception of the two last formulas which become:

12.

hasEquality(eq2, "t ** 2 + 4 * t + 1 = 0") (hasUnknown;hasName) (eq2, "t")

Remainder of the representation by external functions

The knowledge base B §3.2 described in the previous section is insufficient to identify the two problems pb1 and pb2 as problems o solving a second degree equation. In other words, for pb ∈ {pb1, pb2}: 2 The degree of a polynomial equation 𝑃 (𝑥 ) = 𝑄 (𝑥 ) is the degree of 𝑄 -𝑃 .

B §3.2 ̸ |= EquationSolving ⊓ ∃hasEquation.Equation2ndDegree (pb)
Indeed, the base contains neither the knowledge that enables to identify the equations as being polynomial, nor to obtain the degrees of these equations. These inferences are based on expression handling, for which external computation is better suited. Two functions are assumed to be implemented in Sympy (i.e. Python with the Sympy library, but it could be in another programming language): isAPolEquation and degreeOfAPolynomialEquation. The inputs of both functions are strings representing Sympy expressions. The former outputs the Boolean true iff this expression is one of a polynomial expression. The latter outputs the degree of a polynomial equation.

Connecting representation entities of the two languages

Connections between OWL DL and Sympy have to be made since:

(C1) The function isAPolEquation written in Sympy can be used to properly classify the equations eq1 and eq2 under the concept PolynomialEquation, i.e. to be able to infer the assertions PolynomialEquation(pb) for pb ∈ {pb1, pb2}. (C2) The function degreeOfAPolynomialEquation written in Sympy can be used in order to infer the assertions degree(eq1, 2) and degree(eq2, 2).

From the description logic perspective, isAPolEquation and degreeOfAPolynomialEquation are considered external functions, regardless of the way they are implemented.

The connection (C1) is represented in the proposed approach by the following formula: The feature function of the call indicates the function name and the system under which this function has to be executed (here, Sympy). The feature params is associated with a list of property chains that indicate how the parameters of the function can be related to an instance of the domain (here, Equation1RealUnknown). The function has two arguments: the first one is the equality expression of the instance equation and the second one is the name of the unknown of the instance equation, both interpreted as strings by Sympy.

Formula 13 belongs to OWL DL call which is an extension of OWL DL proposed in Section 4. Intuitively, this formula means that if eq is inferred to be an instance of Equation1RealUnknown for which the equality and the name of the unknown are two identified strings, then the function isAPolEquation can be triggered with these strings as parameters and, if 𝑣 is the Boolean returned by this function, the assertion isAPolynomialEquation(eq, 𝑣) is inferred.

The idea is that with the formulas of B §3.2 , the above call formula and the additional OWL DL formula 14.

PolynomialEquation ≡ Equation1RealUnknown ⊓ ∃isAPolynomialEquation.{true} it can be entailed that eq1 and eq2 are instances of PolynomialEquation (provided that the call to Sympy of the function isAPolynomialEquation returns the expected value 3 ). The connection (C2) is represented in the proposed approach in a similar way: it can be entailed that eq1 and eq2 are instances of Equation2ndDegree and, therefore, the following assertions 17. hasSolvingMethod(pb1, findObviousSolEqDeg2) 18. hasSolvingMethod(pb1, useDiscriminant) 19. hasSolvingMethod(pb2, findObviousSolEqDeg2) 20. hasSolvingMethod(pb2, useDiscriminant) are consequences of B §3.4 , i.e. the union of B §3.2 and of the formulas of the current section, under the assumption of the correct execution of the function in Sympy.

REPRESENTING MATHEMATICAL KNOWLEDGE IN OWL DL call

This section presents the proposed approach for representing mathematical knowledge. First, the logic OWL DL call is presented ( §4.1).

Then, an algorithm for the inferences in this logic is described ( §4.2). Section 4.3 presents the implementation of the algorithm and some discussion on the practical and methodological aspects of using OWL DL call . Finally, Section 4.4 studies the issue of more complex examples that require an extension of this formalism.

OWL DL call

The syntax of formulas is the same as for OWL DL, with the following additional terminological formula construct: Therefore, according to the semantics of call formulas, it can be inferred that (𝑥, true) ∈ isAPolynomialEquation I . Finally, since I satisfies formula 14, it comes that 𝑥 ∈ PolynomialEquation I , i.e. I |= PolynomialEquation(eq1), which ends the proof.

An inference algorithm for OWL DL call

The inference algorithm presented in this section is based on an inference engine for OWL DL that is assumed to always terminate (e.g. Hermit [START_REF] Glimm | HermiT: an OWL 2 reasoner[END_REF]). This algorithm simply consists in (1) inferring a set of assertions 𝑝 (𝑎, 𝑣) from the formulas based on calls for a given instance 𝑎, (2) adding these assumptions to the knowledge base (for all instances 𝑎) and making OWL DL inferences on the updated knowledge base.

Step ( 1) is detailed in Algorithm 1.

Step ( 2) is detailed in Algorithm 2.

Properties of the algorithm. The study of the inference algorithm under general assumptions remains to be done. However, a study has been carried out under the following assumptions:

(A1) Satisfiability of the knowledge base B given as parameter (i.e. existence of an interpretation I that satisfies all the call-free formulas and all the call formulas); (A2) Functionality of the object properties involved in the chain properties of a call formula (i.e. for all call formula 𝑝 ⊒ call(𝑓 , 𝐿𝑃𝐶, 𝐷, 𝜏)), the object properties occurring in each property chain of 𝐿𝑃𝐶 are functional). First, it can be noted that under assumption (A1) if two call formulas enable to infer respectively 𝑝 (𝑎, 𝑣 1 ) and 𝑝 (𝑎, 𝑣 2 ) then 𝑣 1 and 𝑣 2 inputs • B: a knowledge base of OWL DL call ,

• 𝑎: an instance,

• cache: a dictionary whose keys are pairs (Γ, 𝑏) where Γ = (𝑝 ⊒ call(𝑓 , 𝐿𝑃𝐶, 𝐷, 𝜏)) is a call formula and 𝑏 is an instance, and values are assertions of the form 𝑝 (𝑏, 𝑣) (cache stores the value of previous calls and is initially empty). effect cache is updated. output A set of assertions 𝑝 (𝑎, 𝑣) entailed by B thanks to external function calls. function assertionsEntailedByCalls(B, 𝑎, cache): must be equal: in this paper, datatype properties are assumed to be interpreted as partial functions, therefore 𝑣 1 ≠ 𝑣 2 would lead to inconsistency. For instance, two methods for finding the degree of a polynomial equation have to lead to the same result when neither of them fail, otherwise, B would be inconsistent.

A ← ∅ B call ← the set of call formulas of B B noCall ← B \ B call C ← (𝑝 ⊒ call(𝑓 , 𝐿𝑃𝐶, 𝐷, 𝜏)) ∈ B call | B noCall |= 𝐷 (𝑎) for Γ = (𝑝 ⊒ call(𝑓 , 𝐿𝑃𝐶, 𝐷, 𝜏)) ∈ C
Under assumptions (A1) and (A2), the process always terminates. This is a consequence of (1) the fact that there is a finite number of pairs (Γ, 𝑎) where Γ is a call formula of B and 𝑎 is an instance occurring in B, (2) the OWL DL inference engine and the called functions always terminate.

The algorithm is sound: if 𝑝 (𝑎, 𝑣) is an assertion added to B by this algorithm then B init |= 𝑝 (𝑎, 𝑣), where B init is the value of B at the start of the algorithm (it does not add assertion that are not logically inferable from the knowledge base). This follows from the definition of the satisfaction of call formulas by interpretations.

Finally, it remains to be proven that the algorithm is complete in the following sense: for any formula 𝜑 of OWL DL, if B init |= 𝜑 in the logic OWL DL call then B final |= 𝜑 in the logic OWL DL (i.e. without taking into account call formulas), where B init and B final are the values of B before and after the application of Algorithm 2. In particular, this means that if an assertion 𝑝 (𝑎, 𝑣) (where 𝑝 is a 𝜏-property) can be inferred from B init using one or several call formulas but cannot be inferred from B init without call formulas, then it can be inferred from B final without call formula. Therefore, once Algorithm 2 is applied, the call formulas are useless until new formulas are added to the knowledge base.

Towards an improvement of the algorithm. This algorithm is based on an eager evaluation: all the calls to external functions that can be made are actually made. Now, a given query to the inference engine may not necessarily require all these calls. Therefore, triggering calls only when they are needed, according to the principle of lazy evaluation, would be beneficial in terms of computing time.

Using OWL DL call in practice

A first implementation of the algorithm described above is available online 4 , together with the ontology and call formulas for the running example used in this article. This Python implementation relies on the OwlReady2 library5 to manipulate knowledge in OWL DL and for interactions with the Hermit reasoner [START_REF] Glimm | HermiT: an OWL 2 reasoner[END_REF], and on SymPy to implement external functions based on symbolic computation. In practice, the tool takes as input an ontology that includes the definition of call formulas. It outputs a set of RDF triples corresponding to the assertions generated as results of executing the functions associated with those call formulas whenever relevant (i.e., the assertions that complete the ontology so that all inferences derivable from it based on OWL DL call can be obtained by a standard description logic reasoner). Therefore, taking inspiration from this example, a user might define new concepts of problems, the parts of their definitions that require computation, and the corresponding call formulas, so as to enable inferences combining both description logic reasoning and symbolic computation.

From a knowledge representation point of view, the following question must be raised: Given a mathematical piece of knowledge to be formalized, what parts of it should be represented in OWL DL and what part should be represented by external functions? In the example of Section 3, the choice consisted in leaving to the external functions the handling of mathematical expressions and keeping in OWL DL all the conceptual notions, that are usually expressed in natural language using a mathematical terminology. This seems to be a sensible approach to answer this representation question in general but, in some situations, this criterion may not be so simple to apply, for example, when the same theorem is expressed differently (with more or less formal parts) in two textbooks in mathematics. Therefore, this methodological question is likely to require more in-depth studies in the future.

Towards more complex cases

In the previous sections, it has been explained how some mathematical problems, represented by instances pb of the Problem concept can be solved thanks to the use of call-formulas in OWL DL call . Some mathematical problems, such as the ones arising in physics for the modeling of micro-mirror arrays, are more complex in the sense that they require the use of several definitions and theorems. Provided that each of these definitions and theorems is triggered by an instance and given a first instance pb init , the idea is to use call formulas to reify new instances (instead of datatype values).

Extension of the logic OWL DL call . This extension consists in considering the new call formulas 𝑟 ⊒ call(𝑓 , 𝐿𝑃𝐶, 𝐷, 𝑅) with the following differences with the call formulas of the previous sections:

• 𝑟 is an object property and 𝑅 is a concept;

• 𝑓 is interpreted in 𝑓 that returns a new instance inst (i.e. an instance not occurring in the knowledge base) accompanied by assertions associated to this instance;6 • In particular if the call formula is triggered on a instance 𝑎 of 𝐷, then one of the new assertions is always 𝑟 (𝑎, inst) (𝑅 is qualified as a range concept of 𝑟 ). In what follows we use the following OWL DL formula, not introduced before: 𝑟 1 ;𝑟 2 ; . . . ;𝑟 𝑛 ⊑ 𝑠 where 𝑟 1 , 𝑟 2 , . . . , 𝑟 𝑛 and 𝑠 are object properties. An interpretation I satisfies this formula if, for every pair of instances (𝑎, 𝑏), I |= (𝑟 1 ;𝑟 2 ; . . . ;𝑟 𝑛 ) (𝑎, 𝑏) entails I |= 𝑠 (𝑎, 𝑏).

Example. Let us consider the following problem:

pb init = find the eigenvalues of the matrix 𝑀 = 2 1 1 2

For solving this problem, the following definitions and theorems are used: (Def. 1) The characteristic polynomial of a square matrix 𝑀 of order 𝑛 is the polynomial det(𝑋 • 𝐼 𝑛 -𝑀) (where 𝐼 𝑛 is the unit matrix of order 𝑛 and det(𝐴) is the determinant of a square matrix 𝐴).

(Def.

2) The roots of a polynomial 𝑃 are the solutions of the polynomial equation 𝑃 (𝑡) = 0 with unknown 𝑡.

(Th. 1) The eingenvalues of a square matrix 𝑀 are the roots of its characteristic polynomial. -And the definitions and theorems of Section 3.

In the following, the principles for implementing this example in the extended logic are outlined.

The definition of pb init is based on the introduction of an instance mat representing the matrix 𝑀: 21. FindingEigenValues ⊑ Problem; 22. FindingEigenValues(pb init ); 23. hasMatrix(pb init , mat); 24. hasExpression(mat, "[ [START_REF] Belkhir | Towards an automatic tool for multi-scale model derivation illustrated with a micro-mirror array[END_REF][START_REF] Belkhir | A tool for aided multi-scale model derivation and its application to the simulation of a micro mirror array[END_REF], [START_REF] Belkhir | A tool for aided multi-scale model derivation and its application to the simulation of a micro mirror array[END_REF][START_REF] Belkhir | Towards an automatic tool for multi-scale model derivation illustrated with a micro-mirror array[END_REF]]"). 25. SquareMatrix(mat); 7Now, (Def. 1) can be formalized by: 26. hasCharacteristicPolynomial ⊒ call("computeCharPol", [hasExpression], SquareMatrix, Polynomial). using the Sympy function "computeCharPol".

From these formulas the following assertions can be inferred:

27. hasCharacteristicPolynomial(mat, inst1); 28. Polynomial(inst1); 29. hasExpression(inst1, "X ** 2 -4 * X + 3").

Now, (Def. 2) can be formalized by: 30. hasEquation;hasSolutionSet ⊑ hasRootSet; 31. hasEquation ⊒ call("polToEquation", [hasExpression], Polynomial, PolynomialEquation). where the Sympy function "polToEquation" consists in substituting "X" by "t", concatenating " = 0" to a string and generating a new instance and relevant assertions.

From this, the following assertions can be inferred:

32. hasEquation(inst1, inst2); 33. PolynomialEquation(inst2); 34. hasEquality(inst2, "t ** 2 -4 * t + 3 = 0"); 35. hasUnknown(inst2, "t").

The instance inst2 represents a second degree equation, which can be solved using the principles described in Section 3: using a call formula based on findObviousSolEqDeg2 leads to the solution set {𝑡 = 1, 𝑡 = 3} represented by the instance inst3:

36. hasSolutionSet(inst2, inst3). Now, (Th. 1) and the fact that the solution of a problem of finding eigenvalues of a matrix is the set of these eingenvalues can be expressed respectively by: 37. hasCharacteristicPolynomial;hasRootSet ⊑ hasSetOfEigenValues; 38. hasMatrix;hasRootSet ⊑ hasSolution.

from which it can be deduced that 39. hasSolution(pb init , inst3) which solves the problem.

Algorithmic issues. The application of the algorithm presented in Section 4.2 to this extension of OWL DL call does not always terminate as the example hereafter shows. Consider the formula 𝑟 ⊒ call(𝑓 , [𝑝], ⊤, unsigned int) where 𝑝 is a 𝜏-property with 𝜏 = unsigned int, and 𝑓 associates to 𝑣 ∈ N an instance inst together with the assertion 𝑝 (inst, 𝑣 + 1). Then, this call formula and an assertion 𝑝 (𝑎, 0) generates an infinite sequence of assertions 𝑟 (𝑎, inst1), 𝑝 (inst1, 1), 𝑟 (inst1, inst2), 𝑝 (inst2, 2), 𝑟 (inst2, inst3), 𝑝 (inst3, 3), etc., hence the non-termination of the algorithm.

Two directions of future work are considered in order to address this termination issue. The first one is to examine whether the inference relation in this logic is decidable and, if so, what algorithm can be proposed (intuitively, using lazy evaluation seems to be a good idea). The second one is to consider restrictions to ensure termination, even with the algorithm presented in Section 4.2. A possibility of such a restriction could be to have call formulas such that the set of concepts that are domains or ranges of these formulas are pairwise disjoint, which would avoid, at least, some loops.

Towards the representation and use of theorems in the domain of the asymptotic analysis of partial differential equations. Although the problems presented in this article are simple mathematical problems, the proposed approach has been developed with the goal to be adapted to the complex domain of asymptotic analysis of partial differential equations, a domain in which thousands of theorems have been developed in the literature. At this stage, the authors are convinced that at least a large proportion of such theorems can be represented in OWL DL call (with the extension presented in this section). However, scalability is an issue that might appear when actually dealing with an important number of theorems.

DISCUSSION AND CONCLUSION

This paper has presented a novel approach to the representation of mathematical knowledge in a formalism extending OWL DL by "call formulas", i.e. formulas related to calls to external functions (e.g. functions for handling mathematical expressions). The necessity of such a formalism has emerged from the way mathematicians express their knowledge, using both natural language with a mathematical terminology and mathematical expressions.

The use of calls to external functions is not a new issue in the realm of description logics and related formalisms, and it faces two opposing constraints: (1) the theoretical ideal of having a fully specified logic on which theoretical properties can be proven without additional assumptions, (2) the practical expressivity (i.e. the possibility of using all the required external functions).

The use of complex concrete domains as presented in [START_REF] Lutz | Description Logics with Concrete Domains -A Survey[END_REF] is more on the side of (1) on the (1)-(2) spectrum. For such a concrete domain 𝜏 = (Δ 𝜏 , Φ 𝜏 ), 𝜎 ∈ Φ 𝜏 represents a relation 𝜎 𝜏 of Δ 𝜏 that can be binary, ternary, etc., and not only unary as in concrete domains of OWL DL (in OWL DL, 𝜎 𝜏 is a subset of Δ 𝜏 hence a unary relation on Δ 𝜏 ). We have given up the idea of using complex concrete domains because this approach would make it difficult (if not impossible) to represent even simple examples of mathematical notions.

Our approach is more on the (2) side of the spectrum: priority has been given to expressiveness, and the study of theoretical properties requires assumptions on the external functions, while remaining more nuanced than previous attempts such as in KL-ONE [START_REF] Brachman | KL-ONE reference manual[END_REF]. Indeed, KL-ONE enabled the definition of interpretative hooks "in which direct instructions to the interpreter are expressed in the language that implements the interpreter itself" without any restriction, making it impossible to provide any theoretical guarantee regarding the properties of the language.

It appears clearly throughout the paper that a lot of work remains to be done in order to reach our goal: a general-purpose logic for representing mathematical knowledge associated with a scalable inference system. The current prototype can handle simple mathematical problems, but considering complex problems (involving, in our setting, the creation of new instances during the inference process) requires an extension of the logic that raises theoretical and practical issues, as described in Section 4.4.

Another issue to be studied occurs when several paths exist in order to solve a problem. In Section 3, each of the problems pb1 and pb2 can be solved using two methods: findObviousSolEqDeg2 and useDiscriminant, but which one should be tried first? Being able to infer from knowledge about mathematical problem-solving strategies the priority with which to consider each method and to use this priority in the inference algorithm constitutes another direction for future work.

From an application point of view, our objective is to represent and handle numerous theorems and their proofs in our target domain of asymptotic analysis of partial differential equations, in order to solve practical problems in physics, e.g. modeling micromirror arrays. Following this line, a (very) long-term future work would be to solve problems of this domain for which no theorem is available, by adapting some theorems (and their proofs) to such a problem, according to the principles of case-based reasoning [START_REF] Riesbeck | Inside Case-Based Reasoning[END_REF].

  ∅ (𝐶 ⊓ 𝐷) I = 𝐶 I ∩ 𝐷 I (∃𝑟 .𝐶) I = 𝑥 ∈ Δ I there exists 𝑦 ∈ Δ I such that (𝑥, 𝑦) ∈ 𝑟 I and 𝑦 ∈ 𝐶 I (≤ 1 𝑟 ) I = 𝑥 ∈ Δ I there exists at most one 𝑦 ∈ Δ I such that (𝑥, 𝑦) ∈ 𝑟 I {𝑎 1 , 𝑎 2 , . . . , 𝑎 𝑛 } I = {𝑎 I 1 , 𝑎 I 2 , . . . , 𝑎 I 𝑛 } (∃𝑝.𝜎) I = 𝑥 ∈ Δ I 𝑝 I (𝑥) is defined and 𝑝 I (𝑥) ∈ 𝜎 𝜏 Given an interpretation I and a formula 𝜑, I satisfies 𝜑 (denoted by I |= 𝜑) is defined as follows:

  base is a finite set of formulas of the considered logic. For a knowledge base B and an interpretation I, I |= B if I |= 𝛼 for each 𝛼 ∈ B. B is satisfiable if there is an interpretation I such that I |= B. Given a formula 𝜑 of OWL DL, B entails 𝜑 (noted B |= 𝜑) if for every interpretation I such that I |= B, I |= 𝜑.

  = "isAPolEquation @ Sympy", params = [hasEquality, hasUnknown;hasName], domain = Equation1RealUnknown, range = bool)

  = "degreeOfAPolynomialEquation @ Sympy", params = [hasEquality, hasUnknown;hasName], domain = PolynomialEquation, range = unsigned int)With the two call formulas in this section, the formulas in B §3.2 , and the following additional formula: 16.Equation2ndDegree ≡ PolynomialEquation ⊓ ∃degreePolynomialEquation.{2}

B

  §3.4 |= PolynomialEquation(eq1) Let I be an interpretation satisfying all the formulas of B §3.4 . Let 𝑥 = eq1 I , 𝑣 1 = "x ** 2 + 2 = -3 * x", 𝑣 2 = "x", and 𝑓 = isAPolEquation. The execution of 𝑓 (𝑣 1 , 𝑣 2 ) returns True and since I satisfies formulas 9, 10, and 11, it comes that: (a) 𝑥 ∈ Equation1RealUnknown I and (b) (𝑥, 𝑣 1 ) ∈ hasEquality I , (𝑥, 𝑣 2 ) ∈ (hasUnknown;hasName) I .

  𝐿𝑃𝐶 = [𝑝𝑐 1 , 𝑝𝑐 2 , . . . , 𝑝𝑐 𝑛𝑎 ] such that, for 𝑘 ∈ ⟦1, 𝑛𝑎⟧, 𝐷 is a domain of 𝑝𝑐 𝑘 and 𝑝𝑐 𝑘 is a 𝜏 𝑘 -property; • 𝑓 is a string providing access to an external function (e.g. the code or a URL to a service), this function having 𝑛𝑎 arguments and being denoted by 𝑓 in the following; • The types of the parameters of 𝑓 are 𝜏 1 , 𝜏 2 , . . . , 𝜏 𝑛𝑎 (in this order) and the type of its output is 𝜏; • The execution of 𝑓 (𝑣 1 , 𝑣 2 , . . . , 𝑣 𝑛𝑎 ), for 𝑣 𝑘 ∈ Δ 𝜏 𝑘 (𝑘 ∈ ⟦1, 𝑛𝑎⟧), is assumed to always terminate and may fail to return an answer in which case, this is denoted by 𝑓 (𝑣 1 , 𝑣 2 , . . . , 𝑣 𝑛𝑎 ) = failure. Moreover, two calls 𝑓 (𝑣 1 , 𝑣 2 , . . . , 𝑣 𝑛𝑎 ) with the same parameter values are assumed to return the same result; in particular, if one call fails, the other one also fails. In the following, this construct is often given with the following abbreviated form: 𝑝 ⊒ call(𝑓 , 𝐿𝑃𝐶, 𝐷, 𝜏) Such a formula is called a call formula. Other formulas are qualified as call-free. Let I = (Δ I , • I ) be an interpretation, I satisfies the formula 𝑝 ⊒ call(𝑓 , 𝐿𝑃𝐶, 𝐷, 𝜏) if, for every (𝑥, 𝑣) ∈ Δ I × Δ 𝜏 , if (a) 𝑥 ∈ 𝐷 I and (b) for every 𝑘 ∈ ⟦1, 𝑛𝑎⟧ there exists 𝑣 𝑘 such that (𝑥, 𝑣 𝑘 ) ∈ (𝑝𝑐 𝑘 ) I , and 𝑓 (𝑣 1 , 𝑣 2 , . . . , 𝑣 𝑛𝑎 ) = 𝑣 (and is therefore different from failure). then 𝑝 I (𝑥) = 𝑣.Now, as an illustration, it is proven, under the assumption that the Sympy function isAPolEquation is correctly implemented and that its implementation never fails, that

𝑝 ⊒ call(function = 𝑓 , params = 𝐿𝑃𝐶, domain = 𝐷, range = 𝜏 ) where

• 𝜏 is a datatype and 𝑝 is a 𝜏-property;

• 𝐷 is a concept;

• 𝐿𝑃𝐶 is a list of 𝑛𝑎 property chains,

  do if the access to cache with key (Γ, 𝑎) fails then 𝑛𝑎 ← length of 𝐿𝑃𝐶 Let 𝑝𝑐 1 , 𝑝𝑐 2 , . . . , 𝑝𝑐 𝑛𝑎 be such that 𝐿𝑃𝐶 = [𝑝𝑐 1 , 𝑝𝑐 2 , . . . , 𝑝𝑐 𝑛𝑎 ] parameter-tuples ← (𝑣 1 , 𝑣 2 , . . . , 𝑣 𝑛𝑎 ) B noCall |= 𝑝𝑐 𝑖 (𝑎, 𝑣 𝑖 ) for 𝑖 ∈ ⟦1, 𝑛𝑎⟧} newAssertions ← ∅ for (𝑣 1 , 𝑣 2 , . . . , 𝑣 𝑛𝑎 ) ∈ parameter-tuples do 𝑣 ← 𝑓 (𝑣 1 , 𝑣 2 , . . . , 𝑣 Computing assertions entailed by call formulas. input B: a knowledge base of OWL DL call , effect B is enriched with all the assertions deduced from the calls.

	end
	end
	return A
	Algorithm 1: function enrichByAssertionsInferredFromCalls(B):
	Ins ← the set of instances occurring in B
	cache ← empty dictionary
	repeat
	𝑠 ← card B
	for each instance 𝑎 occurring in B do
	B ← B ∪ assertionsEntailedByCalls(B, 𝑎, cache)
	end
	until card B = 𝑠;
	Algorithm 2: Enriching the knowledge base with assertions
	coming from calls.

𝑛𝑎 ) if 𝑣 ≠ failure then 𝛼 ← 𝑝 (𝑎, 𝑣) if B noCall ̸ |= 𝛼 then newAssertions ← newAssertions ∪ {𝛼 } end end end A ← A ∪ newAssertions B noCall ← B noCall ∪ newAssertions cache(Γ, 𝑎) ← newAssertions

Remark: if newAssertions = ∅, the cache retains the fact that no new assertion has been entailed from Γ about 𝑎.

https://www.sympy.org

This is shown at the end of Section

[START_REF] Brachman | Knowledge Representation and Reasoning[END_REF].1 for eq1.

https://github.com/mdaquin/OWLDLcall/

https://pypi.org/project/owlready2/

Technically, adding these new assertions to the knowledge base does not keep the equivalence (the knowledge base after this addition is not equivalent to the one before it). However, the equivalence is recovered if new instances are considered as existential variables (as in a skolemization process).

It is noteworthy that a call formula could be added to the knowledge base to make this assertion inferable from assertion 24 and this call formula.