I Abraham
email: romain.abraham@univ-orleans.fr

R Abraham

M Bergounioux
email: maitine.bergounioux@univ-orleans.fr.

G Carlier
email: carlier@ceremade.dauphine.fr.

Tomographic reconstruction from a few views: a multi-marginal optimal transport approach

Keywords:

In this article, we focus on tomographic reconstruction. The problem is to determine the shape of the interior interface using a tomographic approach while very few X-ray radiographs are performed. We use a multi-marginal optimal transport approach. Preliminary numerical results are presented.

Introduction

In this article, we focus on a specific application of tomographic reconstruction for a physical experiment whose goal is to study the behavior of a material under a shock. For this purpose, X-ray radiographs are performed, and the density of the object must then be reconstructed using a tomographic approach (see Figure 1.1). From a theoretical point of view, all the radiographs for a range of angles θ ∈ [0, π] are needed to obtain exact formulas to compute the solution (see [START_REF] Natterer | The mathematics of computerized tomography[END_REF][START_REF] Natterer | Mathematical methods in image reconstruction[END_REF] or [START_REF] Herman | Image reconstruction from projections: the fundamentals of computerized tomography[END_REF]). In practice, a finite (large) number of such radiographs is enough to get a good approximation of the solution (see ( [START_REF] Natterer | Mathematical methods in image reconstruction[END_REF], chapter 6 or [START_REF] Quinto | Singularities of the x-ray transform and limited data tomography in R 2 and R 3[END_REF]). Unfortunately, due to the experimental setup, only very few radiographs (two or three) are available in our case (Figure 1.2).

The number of available projections (views) is closely related to the ill-posedness of the reconstruction problem. Indeed, the smaller the number of data is, the larger is the kernel of the related operator. Roughly speaking, there are an infinity of solutions and this infinity is linked to the kernel dimension. Some methods have been proposed that allow a partial reconstruction of the object [START_REF] Dinten | Tomographie à partir d'un nombre limité de projections : régularisation par des champs markoviens[END_REF]. In the case where we deal with specific objects there exists methods selecting a solution with respect to some prior : in [START_REF] Hstao | Discrete tomography withj a very few views, using gibbs priors and a marginal posterior mode approach[END_REF], [START_REF] Hstao | A coordinate ascent approach to tomographic reconstruction of label images from a few projections[END_REF] the authors use a bayesian model while an optimization approach is used in [START_REF] Batenburg | A network flow algorithm for binary image reconstruction from few projections[END_REF], [START_REF] Batenburg | Reconstructing binary images from discrete x-rays[END_REF] where the problem is modeled as a minimal cost flow problem.

In [START_REF] Abraham | A penalization approach for tomographic reconstruction of binary axially symmetric objects[END_REF] we have assumed that the initial physical setup is axially symmetric so that a single radiograph suffices in theory to reconstruct the 3D object. The inverse problem remains ill-posed: existence and uniqueness of a solution are ensured but there is a lack of stability. However, interesting results have been obtained with a variational method based on the minimization of a penalized least squares cost function ( [START_REF] Bergounioux | A variational method using fractional order hilbert spaces for tomographic reconstruction of blurred and noised binary images[END_REF][START_REF] Abraham | A penalization approach for tomographic reconstruction of binary axially symmetric objects[END_REF]).

In the present paper, we abandon the axisymmetry assumption and we investigate a different modeling using an optimal transport approach (for an overview of optimal transport theory, see the textbooks of Villani [START_REF] Villani | Topics in optimal transportation[END_REF] or Santambrogio [START_REF] Santambrogio | Optimal Transport for Applied Mathematicians[END_REF]). To our knowledge, this point of view is new in the present tomography reconstruction context.

We first suppose that the studied object is described by a function (with compact support) f : R d -→ R that gives the attenuation coefficient of the material at the current point, and we set ρ(dx) = cf (x)dx where c is a normalizing constant so that ρ is a probability measure on R d (we denote by bold letters the vectors and by regular ones the real numbers). In what follows, we want to recover ρ from the data and some prior, and we will search ρ in the set of probability measures on R d (with finite second moments).

The data of tomographic reconstruction problem are

• a set of unitary directions r i ∈ S d-1 , i = 1, . . . k, where S d-1 denotes the unit ball of R d-1 , corresponding to the X-ray propagation directions.

• a corresponding collection of probability measures π i , i = 1, . . . , k respectively defined on r ⊥ i , with finite second moments.

The probability π i represents the X-ray measurement on a hyperplane r i ⊥ . Note that if d = 2 this hyperplane reduces to a line. In this case, we set d i := r i ⊥ ∈ S 1 , a generating direction.

We focus here on the case where d = 3. Moreover, we suppose that the incident X-rays are parallel so that the problems reduces to several 2D problems: the horizontal planes (orthogonal to the X-ray direction) are independent and we can reconstruct each of them separately (hence considering a two-dimensional object and one-dimensional data, see Figure 1.3). However, for the sake of mathematical generality we present the model in R d keeping 1D projections. The probability π i represents now the X-ray measurement on a line whose direction is d i . Let us denote by Π d i the projection operator on the line directed by d i and by and by T # µ the push-forward of the measure µ through the map T : T is a map from R n to R p , such that for every Borel subset A of R p T # µ(A) = µ(T -1 (A)).Then, without noise perturbation, , we have

π i = Π d i # ρ
or equivalently, for every continuous function

ϕ on R with compact support R ϕ(t)π i (dt) = R d ϕ(d i • x)ρ(dx).
This simplification would not be valid anymore if we add a regularization term in our assumptions that would link the different slices of the object together. Indeed, the problem cannot be reduced to many 2D ones any longer.

In practice, X-rays must cross a very dense object and only a few number of them arrive at the detector. It is therefore necessary to add some amplification devices and very sensitive detectors, which cause a high noise level [START_REF] Partouche-Sebban | Multi-mev flash radiography in shock physics experiments: Specific assemblages of monolithic scintillating crystals for use in ccd-based imagers[END_REF][START_REF] Partouche-Sebban | Scintillateur pour dispositif d'imagerie, module scintillateur, dispositif d'imagerie avec un tel scintillateur et procédé de fabrication d'un scintillateur[END_REF]. Therefore, these theoretical projections are perturbed by some noise that we do not need to model in our approach.

As said before, the measure ρ is not uniquely determined by these few projections and we must add some additional assumption to be able to perform the desired reconstruction. Here, we suppose that we have a prior ρ 0 (which is a theoretical object that can be for instance obtained by numerical simulations) and that the real object ρ is close to this prior.

The novelty of our approach is to consider, instead of more familiar L 2 criteria, optimal transport costs. We are looking for a probability measure ρ whose transportation cost from ρ 0 is small and whose projections match the data π i . As these data are noisy, this matching cannot be perfect and we introduce a variational problem that contains the squared Wasserstein distance between the object ρ and the prior ρ 0 as well as the squared Wasserstein distances between the projections of ρ and the data π i .

This variational problem (see Section 2 for a precise formulation) is very close to the Wasserstein barycenter problem studied in [START_REF] Agueh | Barycenters in the Wasserstein space[END_REF] for which we refer for certain proofs that can be adapted directly. Here, we shall rather emphasize the differences with respect to [START_REF] Agueh | Barycenters in the Wasserstein space[END_REF] both from a theoretical and numerical point of view due to the fact that the π i 's are one-dimensional. Another related problem, which has applications in texture mixing is the so-called sliced-Wasserstein distance (see [START_REF] Rabin | Wasserstein Barycenter and Its Application to Texture Mixing[END_REF] and [START_REF] Bonnotte | Unidimensional and Evolution Methods for Optimal Transportation[END_REF]). Due to the difficulty of computing Wasserstein distances in several dimensions, the sliced-Wasserstein distance, which roughly speaking is an average over directions of the corresponding one-dimensional Wasserstein distance was introduced in [START_REF] Rabin | Wasserstein Barycenter and Its Application to Texture Mixing[END_REF]. The sliced Wasserstein distance is easy to compute (unidimensional optimal transport is basically a sorting problem) and differentiate; so it can be used as a numerically tractable surrogate for multidimensional optimal transport. However, because of the distance to the multi-dimensional prior ρ 0 our variational problem cannot be brought down only to one-dimensional Wasserstein distances computations.

The paper is organized as follows. We first make the optimal transport model precise, give a dual formulation and prove existence and uniqueness of the solution. However, the numerical computation of the problem may costful (many inf-convolution process to compute). So, we give an equivalent multi-marginal formulation of the same problem in Section 3 and the associated dual problem, which seem easier to handle. In the last section, we present numerical hints based on the dual formulation of the multi-marginal problem and some preliminary results.

The variational problem and its dual 2.1 Primal formulation

In the sequel, P 2 (R d ) (respectively P 2 (R)) will denote the set of probability measures on R d (R) with finite second moment. For µ and ν in P 2 (R d ), the squared-2-Wasserstein distance between µ and ν is by definition

W 2 (µ, ν) := inf γ∈Γ(µ,ν) R d ×R d |x -y| 2 γ(dx, dy)
where Γ(µ, ν) denotes the set of probability measures on R d × R d having µ and ν as marginals. The fact that the previous infimum is attained is classical, also, we recall a useful dual formula due to Kantorovich (see for instance [START_REF] Villani | Topics in optimal transportation[END_REF], [START_REF] Santambrogio | Optimal Transport for Applied Mathematicians[END_REF]) that enables one to express W 2 as

W 2 (µ, ν) = sup (f,g)∈C b (R d )×C b (R d ) R d f dµ + R d gdν : f (x) + g(y) ≤ |x -y| 2
Slightly abusing notations, we shall also use the notations W 2 for the squared 2-Wasserstein distance between probability measures on the real line and the notation Γ(µ, ν) for the set of probability measures having µ and ν as marginals even if µ and ν are probability measures on spaces with different dimensions.

Given positive weights λ 0 , λ 1 , . . . , λ k , ρ 0 ∈ P 2 (R d ), and π i ∈ P 2 (R) for i = 1, . . . , k, we consider as cost the weighted sum of squared 2-Wasserstein distances i.e.

J(ρ)

:= λ 0 2 W 2 (ρ 0 , ρ) + 1 2 k i=1 λ i W 2 (π i , Π d i # ρ).
For further use, let us remark that it is easy to see that one may express the onedimensional squared 2-Wasserstein distance between π i and Π d i # ρ equivalently either as

W 2 (π i , Π d i # ρ) = inf γ i ∈Γ(π i ,Π d i # ρ) R×R (x i -y i ) 2 γ i (dx i , dy i ) or W 2 (π i , Π d i # ρ) = inf η i ∈Γ(π i ,ρ) R×R d (x i -x • d i ) 2 η i (dx i , dx). (2.1)
Our aim is to study the following (convex) minimization problem inf

ρ∈P 2 (R d ) J(ρ). (P)
The direct method of the calculus of variations applies (see Prop. 2.3 in [START_REF] Agueh | Barycenters in the Wasserstein space[END_REF] for details) so that Theorem 2.1. (P) admits at least a minimizer. Remark 2.2. We chose to take into account the constraints that Π d i # ρ should be close to π i via penalized terms with parameters λ i in the functional J. An alternative modelling would be to consider

inf W 2 (ρ 0 , ρ) : ρ ∈ P 2 (R d ), W 2 (π i , Π d i # ρ) ≤ σ i , i = 1, • • • , k where σ i , i = 1, • • • , k
is a relaxation parameter (that may represent a noise level for example). Interpreting the weights λ i as multipliers associated to the previous constraints, both formulations are actually equivalent. For the sake of the exposition, we have prefered to work with the penalized problem rather than with the constrained one.

Dual formulation

To address uniqueness of the minimizer and further characterize it, we shall use a dual formulation (see [START_REF] Ekeland | Convex Analysis and Variational Problems[END_REF]) as in [START_REF] Carlier | Matching for teams[END_REF] (compact case) and [START_REF] Agueh | Barycenters in the Wasserstein space[END_REF] (P 2 framework as in the present paper). Let f 0 be a real-valued function defined on R d ; we then define f λ 0 0 by the infimal convolution formula:

f λ 0 0 (x 0 ) := inf x∈R d λ 0 2 |x 0 -x| 2 -f 0 (x) , ∀x 0 ∈ R d . (2.2)
Note as soon as it is finite, this infimum define a semiconcave function of x 0 . In a similar way, for f i : R → R, we define

f λ i i (x i ) := inf y i ∈R d λ i 2 (x i -y i ) 2 -f i (y i ) , ∀x i ∈ R.
By construction, one has

f 0 (x) + f λ 0 0 (x 0 ) ≤ λ 0 2 |x 0 -x| 2 , f i (y i ) + f λ i i (x i ) ≤ λ i 2 (x i -y i ) 2 . (2.3)
Then define

F (f 0 , f 1 , . . . , f k ) := R d f λ 0 0 (x 0 )ρ 0 (dx 0 ) + k i=1 R f λ i i (x i )π i (dx i )
and consider the (concave) maximization problem sup

(f 0 ,...,f k )∈K F (f 0 , f 1 , . . . , f k ) (P * )
where K consists of continuous functions that have at most quadratic growth at infinity and such that

f 0 (x) + k i=1 f i (d i • x) = 0, ∀x ∈ R d . (2.4)
The fact that sup(P * ) ≤ inf(P) is easy to see. Indeed, take (f 0 , . . . , f k ) ∈ K, ρ ∈ P 2 (R d ), γ 0 ∈ Γ(ρ 0 , ρ) and η i ∈ Γ(π i , ρ), and using (2.4), we have

λ 0 2 R d ×R d |x 0 -x| 2 γ 0 (dx 0 , dx) + k i=1 λ i 2 R×R (x i -x • d i ) 2 η i (dx i , dx) ≥ R d (f 0 (x) + k i=1 f i (d i • x))ρ(dx) + F (f 0 , f 1 , . . . , f k ) = F (f 0 , f 1 , . . . , f k ).
Minimizing the left-hand side with respect to γ 0 ∈ Γ(ρ 0 , ρ) and η i ∈ Γ(π i , ρ) immediately gives sup(P * ) ≤ inf(P). The fact that there is no duality gap and that (P * ) has a maximizer requires some extra work for which we refer to [START_REF] Agueh | Barycenters in the Wasserstein space[END_REF]:

Theorem 2.3. The following duality relation holds inf(P) = sup(P * ).

Moreover, (P * ) admits a solution (f 0 , f 1 , . . . , f 1 ) that can be chosen in such a way that the functions v 1 , . . . , v k defined by

v i (t) := λ i 2 t 2 -f i (t), t ∈ R, i = 1, . . . , k (2.5)
are convex (which in particular implies that the functions f 1 , . . . , f k can be chosen semiconcave on R and f 0 semiconvex on R d ).

From the previous duality result we may deduce (as usual with convex duality) the following optimality conditions. Let ρ solve (P), γ 0 ∈ Γ(ρ 0 , ρ) be an optimal transport plan for W 2 (ρ 0 , ρ) and η i ∈ Γ(π i , ρ) be optimal in (2.1), we then have

J(ρ) = λ 0 2 R d ×R d |x 0 -x| 2 γ 0 (dx 0 , dx) + k i=1 λ i 2 R×R (x i -x • d i ) 2 η i (dx i , dx) = F (f 0 , f 1 . . . , f k ) = R d ×R d (f λ 0 0 (x 0 ) + f 0 (x))γ 0 (dx 0 , dx) + k i=1 R×R (f λ i i (x i ) + f i (x • x i ))η i (dx i , dx),
so that for γ 0 -a.e. (x 0 , x) one has

f λ 0 0 (x 0 ) = λ 0 2 |x 0 -x| 2 -f 0 (x) = inf z∈R d λ 0 2 |x 0 -z| 2 -f 0 (z) (2.6)
and, similarly for η i -a.e. (x i , x),

f λ i i (x i ) = λ i 2 (x i -x • d i ) 2 -f i (x • x i ) = inf z∈R λ i 2 (x i -z) 2 -f i (z) . (2.7)
If f λ 0 0 is differentiable at x 0 , we deduce from (2.6) that Since semiconvex functions are differentiable on the complement on a small set, one immediately deduces from the duality theorem 2.3 the following uniqueness result: Corollary 2.5. If ρ 0 vanishes on small sets, problem (P) admits a unique solution ρ. More precisely, if (f 0 , f 1 , . . . , f k ) solves (P * ), then ρ = T 0# ρ 0 where

∇f λ 0 0 (x 0 ) = λ 0 (x 0 -x), i.e. x = x 0 - 1 λ 0 ∇f λ 0 0 (x 0 ). (2.8) Similarly, if f λ i i is differentiable at x i , one gets from (2.7) that (f λ i i ) (x i ) = λ i (x i -x • d i ), i.e. x • d i = x i - 1 λ i (f λ i i ) (x i ). ( 2
T 0 (x 0 ) := x 0 - 1 λ 0 ∇f λ 0 0 (x 0 ), ∀x 0 ∈ R d .
Proof. The proof is a straightforward consequence of the fact that f λ 0 0 being semiconvex, it is differentiable ρ 0 a.e. and formula (2.8).

Remark 2.6. When ρ 0 vanishes on small sets, it is well-known that ρ → W 2 (ρ, ρ 0 ) is strictly convex (see for instance proposition 7.19 in [START_REF] Santambrogio | Optimal Transport for Applied Mathematicians[END_REF]), and so is J as well. This can be used to give another uniqueness proof.

Assume that ρ 0 vanishes on small sets, as soon as one knows a solution of (P * ), the minimizer ρ of (P) may be deduced by the previous corollary . At first glance, (P * ) looks simpler than (P) because it only involves k functions of one variable (f 0 being deduced from f 1 , . . . , f k by (2.4)). However, it is not easy to solve in practice since it involves the computation of infimal convolutions for all the potentials f 0 , f 1 , . . . , f k . We propose in the next section a multi-marginal reformulation whose dual requires only one such infimum computation.

Multi-marginal reformulation

Our aim now is to give an equivalent linear reformulation that takes the form of a multimarginal optimal transport problem. For any

x := (x 0 , x 1 , . . . , x k ) ∈ R d × R k , let us define c(x) := inf x∈R d λ 0 2 |x 0 -x| 2 + k i=1 λ i 2 (x i -x • d i ) 2 . (3.1)
This quadratic problem has a unique minimizer that we denote T (x); its expression is easy to compute and reads as

T (x) = λ 0 id + k i=1 λ i d i ⊗ d i -1 (λ 0 x 0 + k i=1 λ i x i d i ). (3.2)
Replacing and developing the squares then gives

c(x) = λ 0 2 |x 0 | 2 + k i=1 λ i 2 x 2 i - 1 2 T (x) • (λ 0 x 0 + k i=1 λ i x i d i )
which we can rewrite in a more concise way as

c(x) = λ 0 2 |x 0 | 2 + k i=1 λ i 2 x 2 i - 1 2 Az(x) • z(x) (3.3)
with

A := λ 0 id + k i=1 λ i d i ⊗ d i -1 and z(x) := λ 0 x 0 + k i=1 λ i x i d i . (3.4)
The multi-marginal optimal transport problem then reads inf

γ∈Γ(ρ 0 ,π 1 ,...,π k ) R d ×R k c(x)γ(dx) (P m )
where Γ(ρ 0 , π 1 , . . . , π k ) denotes the set of probability measures on R d ×R k having ρ 0 , π 1 , . . . , π k as marginals and c is the cost computed above. Again the existence of an optimal measure for (P m ) is easy to prove.

Equivalence

The connection between (P) and (P m ) is then given by Proposition 3.1. If γ solves (P m ) then ρ := T # γ (where T is given by (3.2)) solves (P).

Proof. Let γ be a solution of (P m ). Let ρ ∈ P 2 (R d ), γ 0 ∈ Γ(ρ 0 , ρ) be an optimal transport plan for W 2 (ρ 0 , ρ) and η i ∈ Γ(π i , ρ) be optimal in (2.1). Using the disintegration theorem (see for instance [START_REF] Dellacherie | Probabilities and Potential[END_REF]) we may write

γ 0 = γ x 0 ⊗ ρ, η i = η x i ⊗ ρ. Then define ξ ∈ P 2 (R d × R d × R k ) by ξ := γ x 0 k i=1 η x i ⊗ ρ i.e. for every ϕ ∈ C c (R d × R d × R k ) R d ×R d ×R k ϕ dξ = R d R d ×R k ϕ(x 0 , x, x 1 , . . . , x k )γ x 0 (dx 0 )η x 1 (dx 1 ) • • • η x k (dx k ) ρ(dx).
Let γ ∈ P 2 (R d × R k ) be defined by:

R d ×R k ψdγ = R d ×R d ×R k ψ(x 0 , x 1 , . . . , x k )ξ(dx 0 , dx, dx 1 , . . . , dx k ). for every ψ ∈ C c (R d × R k ).
By construction, the projection of ξ on the (x 0 , x) variables (respectively (x i , x) variables) is γ 0 (respectively η i ); this implies in particular that γ ∈ Γ(ρ 0 , π 1 , . . . , π k ) and we have

J(ρ) = R d ×R d ×R k λ 0 2 |x 0 -x| 2 + k i=1 λ i 2 (x i -x • d i ) 2 ξ(dx 0 , dx, dx 1 , . . . , dx k ) ≥ R d ×R k c(x)γ(dx) ≥ R d ×R k c(x)γ(dx)
(again using the concise notation x := (x 0 , x 1 , . . . , x k )). Now for ρ := T # γ, we have

J(ρ) ≤ R d ××R k λ 0 2 |x 0 -T (x)| 2 + k i=1 λ i 2 (x i -T (x) • d i ) 2 γ(dx) = R d ×R k c(x)γ(dx).
This proves the optimality of ρ in (P).

Remark 3.2. It follows from the previous proposition and the fact that A is linear that ρ has compact support as soon as ρ 0 and π 1 , . . . , π k are compactly supported. More precisely, recalling (3.2)-(3.4), we have

spt(ρ) ⊂ A(λ 0 spt(ρ 0 ) + k i=1 λ i spt(π i )d i ).

Duality

Thank to expression (3.3), problem (P m ) is equivalent to

sup γ∈Γ(ρ 0 ,π 1 ,...,π k ) 1 2 R d ×R k Az(x) • z(x)γ(dx) (3.5)
where the symmetric positive definite matrix A and the linear map z are defined in (3.4). It is well known (see for instance [START_REF] Gangbo | Optimal maps for the multidimensional Monge-Kantorovich problem[END_REF]) that this linear problem admits the dual formulation inf

R d u 0 ρ 0 + k i=1 R u i π i : u 0 (x 0 )+ k i=1 u i (x i ) ≥ 1 2 Az(x) • z(x), ∀x ∈ R d × R k (P * m )
and that the latter admits a minimizer which satisfies

u 0 (x 0 ) = sup (x 1 ,...x k ) 1 2 A(λ 0 x 0 + k i=1 λ i x i d i ) • (λ 0 x 0 + k i=1 λ i x i d i ) - k i=1 u i (x i ) ,
as well as

u j (x j ) = sup (x 0 ,x i =j ) 1 2 A(λ 0 x 0 + k i=1 λ i x i d i ) • (λ 0 x 0 + k i=1 λ i x i d i )) - k i=1, i =j u i (x i ) -u 0 (x 0 ) .
It is easy seen that x 0 → u 0 (x 0 ) -

λ 2 0 2 Ax 0 • x 0 and x i → u i (x i ) - λ 2 i 2 (Ad i • d i )x 2
i are convex so that the potentials u 0 , u 1 , . . . , u k are strongly convex (i.e. have an Hessian that is bounded from below away from zero). By duality, if γ is optimal for (3.5) and (u 0 , u 1 , . . . , u k ) solves (P * m ), then for γ a.e. x = (x 0 , x 1 , . . . , x k ) one has

u 0 (x 0 ) + k i=1 u i (x i ) = 1 2 Az(x) • z(x).
If, in addition, u 0 is differentiable at x 0 and u i is differentiable at x i one has:

∇u 0 (x 0 ) = λ 0 Az(x) ⇒ z(x) = A -1 ∇u 0 (x 0 ) λ 0 (3.6)
and using the fact that u i is injective since u i is strongly convex, we also have

u i (x i ) = λ i Az(x) • d i = λ i λ 0 ∇u 0 (x 0 ) • d i ⇒ x i = (u i ) -1 λ i λ 0 ∇u 0 (x 0 ) • d i . (3.7)

Characterization and regularity

From the previous duality relations we deduce the following result on uniqueness of the optimal measure γ for (3.5) and that it is of Monge type (i.e. supported by a graph over the x 0 variable):

Theorem 3.3.
Assume that ρ 0 vanishes on small sets and that π i does not charge points for i = 1, . . . , k. Then (3.5) admits a unique solution γ that is of Monge-Type (i.e. induced by a map) and given by γ := Ψ # ρ 0 where

Ψ(x 0 ) := x 0 , (u 1 ) -1 λ 1 λ 0 ∇u 0 (x 0 ) • d 1 , . . . , (u k ) -1 λ k λ 0 ∇u 0 (x 0 ) • d k
and the strongly convex potentials u 0 , u 1 , . . . , u k solve the dual problem (P * m ). Proof. The proof comes from the fact that u 0 , u 1 , . . . , u k are differentiable γ-almost everywhere (since these are convex potentials) and the relations (3.6)-(3.7).

Combining the previous with proposition 3.1 we obtain Corollary 3.4. Under the assumptions of theorem 3.3, the solution ρ of (P) is of Monge type and given by ρ

= F # ρ 0 where F (x 0 ) := A λ 0 x 0 + i=1 λ i (u i ) -1 λ i λ 0 ∇u 0 (x 0 ) • d i d i . (3.8)
In the sequel (especially for numerical tests) we use a formulation derived from equations (3.7) and(3.8) as F (x 0 ) = x 0 + δx 0 , where δx 0 stands for the displacement. Indeed, these two equations yield

A -1 (F (x 0 )) = A -1 (x 0 + δx 0 ) = λ 0 x 0 + k i=1 λ i x i d i .
With (3.4), we get

A -1 (δx 0 ) + k i=1 λ i (d i ⊗ d i )x 0 = k i=1 λ i x i d i that is A -1 (δx 0 ) = k i=1 λ i (x i -x 0 • d i )d i . Finally F (x 0 ) = x 0 + A k i=1 λ i (x i -x 0 • d i )d i .
(3.9)

Proceeding as in [START_REF] Agueh | Barycenters in the Wasserstein space[END_REF], we deduce the following regularity result:

Theorem 3.5. If, in addition to the assumptions of Theorem 3.3, ρ 0 belongs to L ∞ (R d ) then ρ belongs to L ∞ (R d ) as well.

Proof. Recalling formula (3.8) and using the fact that A is nonsingular, we see that it is enough to prove that ν := G # ρ 0 is L ∞ where G is defined by

G(x 0 ) := λ 0 x 0 + k i=1 λ i (u i ) -1 λ i λ 0 ∇u 0 (x 0 ) • d i which, setting ϕ i (p) := λ 0 u * i λ i λ 0 p • d i , ∀p ∈ R d
can be rewritten as

G = λ 0 id + k i=1 ∇ϕ i • ∇u 0 .
If the convex functions u 0 and ϕ i were smooth we could then write

DG = λ 0 id +S 1 S 2
where S 1 and S 2 are symmetric positive definite which would imply that det(DG) ≥ λ d 0 hence that ρ 0 (x 0 ) = det(DG(x 0 ))ν(G(x 0 )) ≥ λ d 0 ν(G(x 0 )) which gives the desired L ∞ bound on ν. We refer to [START_REF] Agueh | Barycenters in the Wasserstein space[END_REF], proof of proposition 5.1, for a detailed regularization to recover this inequality in general.

Numerical experiments

In this section, we give preliminary results. Indeed, the numerical realization is quite delicate and deserves a finer study (by comparing different points of view) that will be performed in a forthcoming paper. What follows is rather a validation of the model than a complete numerical investigation. Let us describe the numerical process to solve problem (P * m ) (which involves the computation of only one infimal convolution, whereas (P * ) involves k of them) inf The above constraint can be equivalently written as

R d u 0 ρ 0 + k i=1 R u i π i | u 0 (x 0 ) + k i=1 u i (x i ) ≥ 1 2 Az(x) • z(x), ∀x ∈ R d × R k . where u = (u 1 , • • • , u k ), x = (x 1 , • • • , x k ) ∈ R k , x = (x 0 , x) ∈ R d × R k , A,
∀x 0 ∈ R d u 0 (x 0 ) = -min x∈R k k i=1 u i (x i ) - 1 2 Az(x 0 , x) • z(x 0 , x) , (4.1)
so that problem (P * m ) writes

inf u k i=1 R u i π i - R d min x∈R k k i=1 u i (x i ) - 1 2 Az(x 0 , x) • z(x 0 , x) ρ 0 (dx 0 ) . (4.2)
We set

H(u, x 0 , x) = k i=1 u i (x i ) - 1 2 Az(x 0 , x) • z(x 0 , x)
and compute, if possible, a solution to min

x∈R k H(u, x 0 , x) . (4.3)
Note that the existence and uniqueness of solutions is not a priori ensured. It depends on the behavior of the functions u with respect to the quadratic form Az(x 0 , x) • z(x 0 , x). Indeed we know by the theory that the solution u is strongly convex. We must ensure coercivity for H. This will be the case if the strong convexity constant of u is greater that the one of the quadratic form. The latter is driven by the parameters λ i , i = 0, • • • , k. As the different directions d i play the same role it is consistent to choose

λ i = 1, i = 1, • • • , k.
The only parameter to tune is λ = λ 0 . We have chosen λ small so that the weight of the prior is small, which is better since the prior information is less faithful in some sense.

For numerics we set λ = 10 -4 . Assuming that problem (4.3) has at least a solution x * we may use Euler equation and set ∇ x H(u, x 0 , x * ) = 0. A short computation gives :

∀i = 1, • • • , k ∂H ∂x i (u, x 0 , x) = u i (x i ) -λ i Az(x 0 , x) • d i .
Therefore the solution x * (u, x 0 ) is implicitly given by the following system :

∀i = 1, • • • , k ∂H ∂x i (u, x 0 , x * ) = u i (x * i ) -λ i Az(x 0 , x * 1 , • • • , x * k ) • d i = 0 . ( 4
∀i = 1, • • • , k u i (x * i ) = λ i λ 0 Ax 0 • d i + k p=1 α i,p x * p ,
where we have set α

i,p = λ p (Ad p • d i ) for i, p = 1, • • • , k. Setting A = (a i,p ) i,p=1,••• ,k gives that x * (u, x 0 ) is solution of the following system ∀i = 1, • • • , k u i (x * i ) = λ 0 Ax 0 • (λ i d i ) + (Ax * ) i . (4.5) Once x * (u, x 0 ) is computed, the cost functional in problem (P * m ) reads Φ(u) = k i=1 R u i π i - R d H(u, x 0 , x * (u, x 0 ))ρ 0 (dx 0 ) .
To use a numerical method to minimize Φ, we have to compute ∇Φ(u). Let be ϕ : R → R and i

∈ {1, • • • , k}. ∂Φ ∂u i (u) • ϕ = R ϕπ i - R d ∂H ∂u i ((u, x 0 , x * (u, x 0 )) • ϕ ρ 0 (dx 0 ) . The computation of ∂H ∂u i ((u, x 0 , x * ) • ϕ gives ∂H ∂u i (u, x 0 , x * ) • ϕ = ϕ(x * i ) + k j=1 ∂H ∂x j (u, x 0 , x * ) ∂x * j ∂u i (u, x 0 , x * ) • ϕ . Therefore ∀i = 1, • • • , k ∂Φ ∂u i (u) • ϕ = R ϕπ i - R d ϕ(x * i (u, x 0 ))ρ 0 (dx 0 ) , (4.6)
where x * (u, x 0 ) satisfies (4.5). We decided to use a Galerkin type method to approximate the solution. More precisely, we choose a suitable basis (FEM, spectral or spline) to write the function u. Here, we decided to use a spline basis, so that u is described by very few scalar coefficients. In addition, such an approach allows to compute the integral quantities once at the beginning of the process. The algorithm writes : The method is promising but preliminary tests show a great lack of numerical stability and the numerical realization needs further investigation. Moreover, the example in Figure 4.2 shows that the model we propose has to be improved to avoid the diffusion effect we observe, due to the transportation of mass that should not be transported. It seems important to add geometric features that allow transport while preserving topology.

Conclusion

We proposed an original model based on optimal transport theory that allows to perform tomography reconstruction of an object once a prior is given, in the case there are few radiographs. The main novelty lies both in the use of optimal transport to model the problem and the fact that marginal data belong to different spaces.

The numerical realization is not straightforward and has to be further investigated. Let us mention that the entropic regularization of the problem has been explored recently in [START_REF] Benamou | Iterative Bregman projections for regularized transportation problems[END_REF]. There is still a lot of challenging modelling and numerical analysis of potential interest (3D tomography, second-order methods ...) left for future research.

Figure 1 . 1 :

 11 Figure 1.1: Tomography experiment

Figure 1 . 3 :

 13 Figure 1.3: Parallel X-rays : the information along a detector segment depends on a planar slice of the object.

. 9 )

 9 Definition 2.4. A probability measure µ on R d is said to vanish on small sets if and only if µ(A) = 0 for every Borel set A of R d , having Hausdorff dimension less than or equal to d -1.

  and z(x) are defined by equations (3.3) and (3.4).

. 4 )

 4 With (3.4) relation(4.4) writes:

  (a) Groundtruth (desired object) (b) Prior ρ 0 : the lower left square is located at the same place as the desired disk. The upper right one is not. (c) Computed object : the squares have been moved at the right place (the centers of the disk and square are the same). However, the shapes do not fit well. (d) Computed object with the standard backfiltered projection algorithm

Figure 4 . 1 :

 41 Figure 4.1: Example 1: no mass outside the two disks.

  (a) Groundtruth (desired object) (b) Prior ρ 0 (c) Computed object: the whole band containing the square has been transported and not the square only. So, the upper right square is not located at it should be. (d) Computed object with the standard backfiltered projection algorithm

Figure 4 . 2 :

 42 Figure 4.2: Example 2 : there is mass outside the two disks.

Algorithm 1

Given λ i , i = 0, • • • , k, d i , i = 1, • • • , k. Compute integrals (x 0 and ϕ are known ), A and A.

We present here below two academic examples obtained with three views with directions

In both cases λ i = 1, i = 1, 2, 3 and λ = 10 -4 . These examples seem similar. The main difference is that the material density is not zero in example 2. So the induced mass will be transported as well : this is an undesirable effect that we see on Figure 4.2.


Pak Sedang 朴世堂 (1629-1703) KIM Daeyeol Institut National des Langues et Civilisations Orientales (Paris) In the 17 th century, Korean orthodox of Zhu Xi's school, which was confined to overly theoretical or metaphysical thoughts and debates, began to disclose its limitations and some scholars found a way to base their thinking on reality and to make their thought carry in it practicality. Their thought paved the way for further development in the 18 th century. Pak Sedang was part of this new current. In his commentaries to the Classics, he looked for understanding and interpretation true to the original texts but at the same time he was independent and open-minded vis-à-vis the orthodox. In the end of the 17th century and the beginning of the 18th century, during the rage of faction between namin 南人 and sŏin 西人, split and conflict even inside the latter between noron 老論 and soron 少論 were intense around the issue of the relation with Qing China. Pak Sedang was indifferent to the ritual debates between namin and sŏin and, on the diplomatic issues he pursued practical interest over rationale. On the ritual debates, in particular, he pointed out that the rite justified by a principle doesn't affect the fact of transmission of the throne and therefore he didn't fully acknowledge the worth of the ritual debates. In other words, he didn't intend to implement the ritual ideas from Zhu Xi's school in a doctrinaire way. He laid stress on the fact that Confucianism is a system of thought that essentially values the practicality. The scholarly effort he made to renovate Confucianism of his time inside Confucian tradition crystallized into his work Sabyŏnnok 思辨錄 (or T'ongsŏl 通說) that interprets Six Classics, and his search for this renovation outside the tradition, into his commentaries to the Laozi 老子 and the Zhuangzi 莊子.

1.

As to the studies on Confucian Classics, Pak Sedang, being unsatisfied with Zhu Xi's commentaries which were recognized as authentic, pursued faithful interpretation in his own way, tried to recover original meanings in ruminating on the sense of letters and contexts and giving detailed analyses. In this reason, he sometimes did neither accept Zhu Xi's commentaries nor hesitate to indicate doubtful or unclear points in his eyes. In this sense, he was free from Zhu Xi's authority. This attitude of Pak Sedang reveals itself in his commentary to the Great Learning (Taehak 大學) in particular. He underlined that most of the text of the work contain contents that even the beginners can easily understand and put into action. According to him, however, Zhu Xi commits, in his commentary to the opening chapter of the Great Learning, a contradiction in describing the highest stage of the attainment of self-perfection while saying that the work is for the first learner the door to enter to the learning. Pak Sedang glosses the kyŏk 格 in kyŏngmul (格物) as "rule" or "correct" and understands kyŏngmul ch'iji (格物致知) as setting right the object of practice by acquiring the appropriate reference of action in practicing. In other works, these phrases indicate, not any profound theory by which one's knowledge attains the fullest realization of the world of things as Zhu Xi's teaching, but the practical awareness of the correct thing to do. His argument is based on the position that regards as important practice and experience advancing stage by stage, from close proximity to distant place, from lower to higher. Pak Sedang underlines the fact that this is the original spirit of the Classics and therefore he criticizes Zhu Xi's teaching for failing their real meaning. Thus his thought differs in orientation from Zhu Xi's school and takes another turn.

His Chungyong Sabyŏnnok 中庸思辨錄 or the Critical thinking on the Chungyong, starts with a study on the definition of chungyong. Unlike Zhu Xi's commentary reading yong in an ordinary sense, he interprets chungyong as getting the middle way and keeping it permanently. His understanding of the term doesn't restrict it to the awareness of the usual nature of the middle way but puts the emphasis on continual and steady practice. On the grounds that the work is written to teach about human being and not about things, he rejects Zhu Xi's theory that doesn't make a great discrimination between human being and no human being in their original nature.

2.

In criticizing the speculative nature of Neo-Confucianism of Zhu Xi's school, he repudiates its principal concepts and theses. In the development of Neo-Confucianism, the rise of philosophical tendency to understand all formations and changes through principles and the thinking that considers the 'li' 理 (principle) as a reality in the meaning of so yi yŏn 所以然 (the reason why it is so) and so tang yŏn 所當然 (the reason why it must be so), these two factors had worked to come up with the idea of "the ch'ŏn 天 (heaven) is 'li'". Hereby, the idea of 'Lord on High' (sangje 上帝) as a supreme being was eclipsed and the 'li' as principle replaced 'Lord on High'. The Heaven being reduced to 'li' was understood as sŏng 性 (nature) inherent in human being. The li, as Supreme Ultimate regarded as the first cause of reality, is one as a whole; at the same time it is omnipresent. As to this thesis, Pas Sedang considered the 'heaven' as 'Lord on High' irreducible to the li. His understanding about the concept of sŏng (nature) was also different from that of Zhu Xi. The sŏng was for him the perspicacity endowed from Lord on High, corresponding to one's reason capable to distinguish between right and wrong and use perception ability. According to him the sŏng is no other than 'talent' (chae 才) which contains it to shape in accordance with the form of each one after the latter is endowed his form to exist. For this reason he considered also sŏng as having a form ('below form', hyŏng i ha 形而下). He had interest in heterogeneity of the sŏng endowed to each individual more than its essential homogeneity with li which establishes the thesis "nature is principle" (sŏng chŭk li 性則理).

Thus, more than to the general principle the 'original human nature' has, Pak Sedang paid attention to its significance of self-conscious subject having in one's mind innate insight.

And the fulfillment of the latter depends on ordinary practice such as putting filial piety into action. For him, the li (principle) provides the reference in order that good sense or moral judgment is possible and, being endowed this li as criteria that is sŏng combined with the ki 氣 (vital force), human being merely does his best in relation with things and society. Pak Sedang tried to emphasize the necessity of practice in reality and the acquisition of the moral virtue through endeavor in the course of life more than the metaphysical understanding or belief about moral original nature or innate integrity. This thought appears later in Chŏng Yagyong 丁若鏞.

3.

In addition to the Cheng and Zhu's Neo-Confucian school, philosophical thought was relatively varied in Pak Sedang's time. This landscape was shaped by the diversity of Chosŏn scholars' attitudes toward indictments of contradictions and limits of Zhu Xi's school's ruling principle that disclosed themselves during wars and invasions. Pak Sedang's open-minded way of thinking and study can be seen in his attitudes towards Yangming's school, Lao-Zhuang thoughts and Buddhism. In the Laozi and the Zhuangzi not only he points out extensively those which correspond to self-perfection and state administration, fundamentals of Confucianism, but also he explains through his Neo-Confucian eye such concepts as 'way' (to 道), 'virtue' (tŏk 德), 'having name' (yumyŏng 有名), 'not having name' (mumyŏng 無名) or 'putting things in order' (chemul 齊物). This can be regarded at the same time as a 'Confucianization of the Lao-Zhuang's thoughts' and a renovation of Confucianism.

One of the points that are worthy of notice in his commentaries to the Laozi and the Zhuangzi is that he has fundamentally Confucian worldview and value system, that he centers his thinking upon human conditions and actions. He turns the Lao-Zhuang's thoughts on the being transcending human conditions into all interest in human dimension. He affirms man's ethical judgment and attaches importance to the contribution to society through traditionalism, that is, by transmission of values of the past, while being critical against Lao-Zhuang's skeptical attitude toward moral value and their thought pleading for cultural relativity and individual enlightenment. And he pursues applicability in reality of problem solving.

Meanwhile, toward Lao-Zhuang's thought and Buddhism, he shows inclusive attitude, that is, rational and selective adoption of other traditions with the idea that "truth also can partially be found in other traditions". In his search for Confucian truth in Buddhist or Lao-Zhuang's texts, he reads therein the Confucian ideology such as 'self-perfection and social administration' or 'inner sage, outer king'. In particular, he seeks therein an alternative thought to remedy noron's rigid dogmatism of his time.

This inclusive attitude also can be seen in his acknowledgement of ideal being and society thinkable beyond every tradition. For example, toward those who reach an ideal state or a high level of moral attainment, even though they belong to Daoist or Buddhist tradition, he shows them respect by using such appellation as talja 達者, t'ongin 通人, sangin 上人.

According to his thought, there can be no distinction between inside and outside of a tradition at the highest level of the teaching; Dao is in the center that all things and disputes surround and there are lots of ways to approach the center. Hence, no matter how innumerable are disputes, grasping this center one can have plenty of ways to respond to them. He rejects selfrighteousness too. He argues that the ways to pursue the common good can be different from one to another, and that other's searching for good helps my seeking virtue and in this case it is necessary to tolerate and encourage other's pursuit of good. Thereby he regards as model of government the being lenient and fond of doing good in the 'Great Centre' (hwanggŭk 皇極) and 'Perfect Equilibrium' (chungjŏng 中正).

Sources

"六經之書,皆記堯舜以來群聖之言,其理精而其義備,其意深而其旨遠,蓋論其精 也,毫忽之不可亂,語其備也,纖微之無或闕,欲測其深,莫得其所底,欲窮其遠, 不見其所極,固非世之曲士拘儒淺量陋識所可明也,(…) 傳,曰行遠必自邇,此何謂也,非所以提誨昏蔽使其能自省悟乎,誠使世之學者,有 得乎此,向所謂遠者,卽可知自邇而達之,(…) 今之所求於六經,率皆躐其淺邇而深遠是馳,忽其粗略而精備是規,無怪乎其眩무迷 亂沈溺顚躓而莫之有得,彼非但不得乎其深遠精備而已,倂與其淺邇粗略而盡失之矣 ,噫嘻悲夫,其亦惑之甚乎,夫邇者易及淺者易測略者易得粗者易識,因其所及而稍 遠之,遠之又遠,可以極其遠矣,因其所測而稍深之,深之又深,可以極其深矣,因 其所得而漸加備,因其所識而漸加精,使精者益精備者益備,可以極其備極其精矣, 又何有眩무迷亂沈溺顚躓之患哉,夫聾則不聞乎雷霆之聲,瞽則不覩乎日月之光,彼 呑其舌而不敢再有所言,聞者亦搖首而去之,此常衆人之失而天下之善所以伏也,夫 一人之智不如聚天下之智,一人之善不如合天下之善,彼徒恐善之不出於己不知擧天 下之善畢歸於己之爲美,此惑之大也,而罕能改之,其或距人之甚者,雖有絶人之智 ,尙足以亡國敗家,況於下者乎。" (孟子思辨錄,

  (尙書思辨錄, 洪範 11 章). "老子當衰周之時 老於守藏 不用於世 至其將 隱 猶著書以明其所守之道用 見其志 其道 雖不合聖人之法 其意亦欲修身治人 盖其言約 其旨深 自漢以前 尊用其術 上而爲君 能 行恭默之化 下而爲臣 能爲 淸靜之治 及晉之世 士之狂誕者 託爲玄虛無實之談 渺茫不 可涯之說 以飾其僞 以欺一世 天下翕然同趣 而風俗大亂 晉室遂傾 老子之道 夫豈然哉 其遺風餘 烈 歷世猶存 是以後之說老子者 多宗晉人 以爲微言妙義 訛而又訛 益可悲也"( 新註道德經, 序) "夫禮者忠信之薄而亂之首, 前識者道之華而愚之始" (朴世堂 註) "文勝質衰而刑辟多. … 多識前古以爲禮, 而不知非道之實, 旣以自愚, 又愚後人, 故曰愚之始." (新註道德經, 38 章註) (原文) "故有儒墨之是非 以是其所非而非其所是 欲是其所非而非其所 是 則莫若以明" (朴世堂 註) "儒之所非 墨以爲是 墨之所是 儒以爲非 皆由乎大全破於小成 實理蔽於榮 華 而各自爲是非 若眞欲是人之所非 非人之 所是 而不失是非之正 則莫若照之以天理之 明" (南華經註解刪補, 齊物論) "道之樞要在乎是矣. 樞者, 環中之物. 得道之樞以環中而應是非之無窮, 則是非誰無窮而其所以應之者沛乎, 其有餘矣." (南華經註解刪補, 齊物論) "按言 魚各造乎水而已, 無問流之大小; 人各造乎道而已, 無問方之內外. … 遊道術者, 忘彼此." (南華經註解刪補, 大宗師) "天下之善己不獨有, 必與人而共之, 所謂公而不私者是也. 盖天下事一致同歸而殊道百慮. … 天下之人將無不各自以其善而來爭進之於我, 助我爲善." (孟子思辨錄, 公孫추(上)). "聖人待人之厚, 而與人爲善之意, 本自如此, 何嘗如今人迫隘偏狹, 視若怨敵之爲也" (西溪集, 書, 答申監司翼相書)


Kailiang Ji
email: kailiang.ji@inria.fr

CTL Model Checking in Deduction Modulo

Keywords: Model Checking, Deduction Modulo, Resolution Modulo

come

Introduction

In this paper, we express Branching-time temporal logic (CTL) [START_REF] Clarke | Model Checking[END_REF] for a given finite transition system in Deduction Modulo [START_REF] Dowek | Polarized Resolution Modulo[END_REF][START_REF] Dowek | Theorem Proving Modulo[END_REF]. This way, the proof-search algorithms designed for Deduction Modulo, such as Resolution Modulo [START_REF] Burel | Embedding Deduction Modulo into a Prover[END_REF] or Tableaux Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo[END_REF], can be used to build proofs in CTL. Deduction Modulo is a reformulation of Predicate Logic where some axioms-possibly all-are replaced by rewrite rules. For example, the axiom P ⇔ (Q ∨ R) can be replaced by the rewrite rule P → (Q ∨ R), meaning that during the proof, P can be replaced by Q ∨ R at any time.

The idea of translating CTL to another framework, for instance (quantified) boolean formulae [START_REF] Biere | Symbolic Model Checking without BDDs[END_REF], [START_REF] Zhang | Bounded Semantics of CTL and SAT-Based Verification[END_REF], [START_REF] Zhang | QBF Encoding of Temporal Properties and QBF-based Verification[END_REF], higher-order logic [START_REF] Rajan | An Integration of Model Checking with Automated Proof Checking[END_REF], etc., is not new. But using rewrite rules permits to avoid the explosion of the size of formulae during translation, because rewrite rules can be used on demand to unfold defined symbols. So, one of the advantages of this method is that it can express complicated verification problems succinctly. Gilles Dowek and Ying Jiang had given a way to build an axiomatic theory for a given finite model [START_REF] Dowek | Axiomatizing Truth in a Finite Model[END_REF]. In this theory, the formulae are provable if and only if they are valid in the model. In [START_REF] Dowek | A Logical Approach to CTL[END_REF], they gave a slight extension of CTL, named SCTL, where the predicates may have arbitrary arities. And they defined a special sequent calculus to write proofs in SCTL. This sequent calculus is special because it is tailored to each specific finite model M . In this way, a formula is provable in this sequent calculus if and only if it is valid in the model M . In our method, we characterize a finite model in the same way as [START_REF] Dowek | Axiomatizing Truth in a Finite Model[END_REF], but instead of building a deduction system, the CTL formulae are taken as terms, and the logical equivalence between different CTL formulae are expressed by rewrite rules. This way, the existing automated theorem modulo provers, for instance iProver Modulo [START_REF] Burel | Experimenting with Deduction Modulo[END_REF], can be used to do model checking directly. The experimental evaluation shows that the resolution based proof-search algorithms is feasible, and sometimes performs better than the existing solving techniques. The rest of this paper is organized as follows. In Section 2 a new variant of Deduction Modulo for one-sided sequents is presented. In Section 3, the usual semantics of Computation Tree Logic (CTL) is presented. Sections 4 and 5 present the new results of this paper: in Section 4, an alternative new semantics for CTL on finite structures is given; in Section 5, the rewrite rules for each CTL operator are given and the soundness and completeness of this presentation of CTL is proved, using the semantics presented in the previous section. Finally in Section 7, experimental evaluation for the feasibility of rewrite rules using resolution modulo is presented.

Deduction Modulo

One-sided Sequents In this work, instead of using usual sequents of the form A 1 , ..., A n B 1 , ..., B p , we use one-sided sequents [START_REF] Troelstra | Basic Proof Theory[END_REF], where all the propositions are put on the right hand side of the sequent sign and the sequent above is transformed into ¬A 1 , ..., ¬A n , B 1 , ..., B p . Moreover, implication is defined from disjunction and negation (A ⇒ B is just an abbreviation for ¬A ∨ B), and negation is pushed inside the propositions using De Morgan's laws. For each atomic proposition P we also have a dual atomic proposition P ⊥ corresponding to its negation, and the operator ⊥ extends to all the propositions. So that the axiom rule can be formulated as axiom P, P ⊥ Deduction Modulo A rewrite system is a set R of term rewrite rules and proposition rewrite rules. In this paper, only proposition rewrite rules are considered. A proposition rewrite rule is a pair of propositions l → r, in which l is an atomic proposition and r an arbitrary proposition. For instance, P → Q ∨ R. Such a system defines a congruence → and the relation * → is defined, as usual, as the reflexive-transitive closure of →. Deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] is an extension of first-order logic where axioms are replaced by rewrite rules and in a proof, a proposition can be reduced at any time. This possibility is taken into account in the formulation of Sequent Calculus Modulo in Fig. 1.

axiom if A * → P, B * → P ⊥ R A, B R A, ∆ R B, ∆ cut if A * → C, B * → C ⊥ R ∆ R ∆ weak R A, ∆ R B, C, ∆ contr if A * → B, A * → C R A, ∆ A * → R A, ∆ R B, ∆ R C, ∆ ∧ if A * → B ∧ C R A, ∆ R B, ∆ ∨1 if A * → B ∨ C R A, ∆ R C, ∆ ∨2 if A * → B ∨ C R A, ∆ R C, ∆ ∃ if A * → ∃xB,(t/x)B * → C R A, ∆ R B, ∆ ∀ if A * → ∀xB, x / ∈ F V (∆) R A, ∆ Fig. 1. One-sided Sequent Calculus Modulo
For example, with the axiom (Q ⇒ R) ⇒ P we can prove the sequent R P . This axiom is replaced by the rules P → Q ⊥ and P → R and the sequent R P is expressed as the one-sided sequent R ⊥ , P . This sequent has the proof axiom R ⊥ , P

Computation Tree Logic

Properties of a transition system can be specified by temporal logic propositions. Computation tree logic is a propositional branching-time temporal logic introduced by Emerson and Clarke [START_REF] Clarke | Model Checking[END_REF] for finite state systems. Let AP be a set of atomic propositions and p ranges over AP . The set of CTL propositions Φ over AP is defined as follows:

Φ ::= p | ¬Φ | Φ ∧ Φ | Φ ∨ Φ | AXΦ | EXΦ | AF Φ | EF Φ | AGΦ | EGΦ | AU (Φ, Φ) | EU (Φ, Φ) | AR(Φ, Φ) | ER(Φ, Φ)
The semantics of CTL can be given using Kripke structure, which is used in model checking to represent the behavior of a system. Definition 1 (Kripke Structure). Let AP be a set of atomic propositions. A Kripke structure M over AP is a three tuple M = (S, next, L) where -S is a finite (non-empty) set of states.

next : S → P + (S) is a function that gives each state a (non-empty) set of successors.

-L : S → P(AP ) is a function that labels each state with a subset of AP .

An infinite path is an infinite sequence of states

π = π 0 π 1 • • • s.t. ∀i ≥ 0, π i+1 ∈ next(π i ). Note that the sequence π i π i+1 • • • π j is denoted as π j
i and the path π with π 0 = s is denoted as π(s).

Definition 2 (Semantics of CTL). Let p be an atomic proposition. Let ϕ, ϕ 1 , ϕ 2 be CTL propositions. M, s |= ϕ is defined inductively on the structure of ϕ as follows.

M, s |= p ⇔ p ∈ L(s) M, s |= ¬ϕ 1 ⇔ M, s | = ϕ 1 M, s |= ϕ 1 ∧ ϕ 2 ⇔ M, s |= ϕ 1 and M, s |= ϕ 2 M, s |= ϕ 1 ∨ ϕ 2 ⇔ M, s |= ϕ 1 or M, s |= ϕ 2 M, s |= AXϕ 1 ⇔ ∀s ∈ next(s), M, s |= ϕ 1 M, s |= EXϕ 1 ⇔ ∃s ∈ next(s), M, s |= ϕ 1 M, s |= AGϕ 1 ⇔ ∀π(s), ∀i ≥ 0, M, π i |= ϕ 1 M, s |= EGϕ 1 ⇔ ∃π(s) s.t. ∀i ≥ 0, M, π i |= ϕ 1 M, s |= AF ϕ 1 ⇔ ∀π(s), ∃i ≥ 0 s.t. M, π i |= ϕ 1 M, s |= EF ϕ 1 ⇔ ∃π(s), ∃i ≥ 0 s.t. M, π i |= ϕ 1 M, s |= AU (ϕ 1 , ϕ 2 ) ⇔ ∀π(s), ∃j ≥ 0 s.t. M, π j |= ϕ 2 and ∀0 ≤ i < j, M, π i |= ϕ 1 M, s |= EU (ϕ 1 , ϕ 2 ) ⇔ ∃π(s), ∃j ≥ 0 s.t. M, π j |= ϕ 2 and ∀0 ≤ i < j, M, π i |= ϕ 1 M, s |= AR(ϕ 1 , ϕ 2 ) ⇔ ∀π(s), ∀j ≥ 0, either M, π j |= ϕ 2 or ∃0 ≤ i < j s.t. M, π i |= ϕ 1 M, s |= ER(ϕ 1 , ϕ 2 ) ⇔ ∃π(s), ∀j ≥ 0, either M, π j |= ϕ 2 or ∃0 ≤ i < j s.t. M, π i |= ϕ 1 Example 1.
Let M be the Kripke structure in Fig. 2. M, s 1 EGp holds because there exists an infinite path, for instance s 1 , s 2 , s 1 , s 2 . . ., such that p holds on each state. In this section we present an alternative semantics of CTL using finite paths only.

Paths with the Last State Repeated (lsr-paths) A finite path is a lsr-path if and only if the last state on the path occurs twice. For instance s 0 , s 1 , s 0 is a lsr-path. Note that we use ρ = ρ 0 ρ 1 . . . ρ j to denote a lsr-path. A lsr-path ρ with ρ 0 = s is denoted as ρ(s), with ρ i = ρ j is denoted as ρ(i, j). The length of a path l is expressed by len(l) and the concatenation of two paths l 1 , l 2 is l 1 ˆl2 .

Lemma 1 (From infinite paths to lsr-paths and vice-versa). Let M be a Kripke structure.

1. If π is an infinite path of M , then ∃i ≥ 0 such that π i 0 is a lsr-path. 2. If ρ(i, j) is a lsr-path of M , then ρ i 0 ˆ(ρ j i+1 ) ω is an infinite path. Proof. For the first case, as M is finite, there exists at least one state in π which occurs twice. If π i is the first state which occurs twice, then π i 0 is a lsr-path. The second case is trivial. Lemma 2. Let M be a Kripke structure.

1. For the path l = s 0 , s 1 , . . . , s k , there exists a finite path l = s 0 , s 1 , . . . , s i without repeating states s.t. s 0 = s 0 , s i = s k , and ∀0 < j < i, s j is on l. 2. If there is a path from s to s , then there exists a lsr-path ρ(s) s.t. s is on ρ.

Proof. For the first case, l can be built by deleting the cycles from l. The second case is straightforward by the first case and Lemma 1.

Definition 3 (Alternative Semantics of CTL). Let p be an atomic proposition. Let ϕ, ϕ 1 , ϕ 2 be CTL propositions. M, s |= a ϕ is defined inductively on the structure of ϕ as follows.

M, s |=a p ⇔ p ∈ L(s) M, s |=a ¬ϕ1 ⇔ M, s | =a ϕ1 M, s |=a ϕ1 ∧ ϕ2 ⇔ M, s |=a ϕ1 and M, s |=a ϕ2 M, s |=a ϕ1 ∨ ϕ2 ⇔ M, s |=a ϕ1 or M, s |=a ϕ2 M, s |=a AXϕ1 ⇔ ∀s ∈ next(s), M, s |=a ϕ1 M, s |=a EXϕ1 ⇔ ∃s ∈ next(s), M, s |=a ϕ1 M, s |=a AF ϕ1 ⇔ ∀ρ(s), ∃0 ≤ i < len(ρ) -1 s.t. M, ρi |=a ϕ1 M, s |=a EF ϕ1 ⇔ ∃ρ(s), ∃0 ≤ i < len(ρ) -1 s.t. M, ρi |=a ϕ1 M, s |=a AGϕ1 ⇔ ∀ρ(s), ∀0 ≤ i < len(ρ) -1, M, ρi |=a ϕ1 M, s |=a EGϕ1 ⇔ ∃ρ(s), ∀0 ≤ i < len(ρ) -1, M, ρi |=a ϕ1 M, s |=a AU (ϕ1, ϕ2) ⇔ ∀ρ(s), ∃0 ≤ i < len(ρ) -1 s.t. M, ρi |=a ϕ2 and ∀0 ≤ j < i, M, ρj |=a ϕ1 M, s |=a EU (ϕ1, ϕ2) ⇔ ∃ρ(s), ∃0 ≤ i < len(ρ) -1 s.t. M, ρi |=a ϕ2 and ∀0 ≤ j < i, M, ρj |=a ϕ1 M, s |=a AR(ϕ1, ϕ2) ⇔ ∀ρ(s), ∀0 ≤ i < len(ρ) -1, either M, ρi |=a ϕ2 or ∃0 ≤ j < i s.t. M, ρj |=a ϕ1 M, s |=a ER(ϕ1, ϕ2) ⇔ ∃ρ(s), ∀0 ≤ i < len(ρ) -1, either M, ρi |=a ϕ2 or ∃0 ≤ j ≤ i s.t. M, ρj |=a ϕ1
We now prove the equivalence of the two semantics, that is, M, s |= ϕ if and only if M, s |= a ϕ. To simplify the proofs, we use a normal form of the CTL propositions, in which all the negations appear only in front of the atomic propositions.

Negation Normal Form. A CTL proposition is in negation normal form (NNF), if the negation ¬ is applied only to atomic propositions. Every CTL proposition can be transformed into an equivalent proposition of NNF using the following equivalences.

¬¬ϕ ≡ ϕ ¬(ϕ ∨ ψ) ≡ ¬ϕ ∧ ¬ψ ¬AF ϕ ≡ EG¬ϕ ¬AU (ϕ, ψ) ≡ ER(¬ϕ, ¬ψ) ¬(ϕ ∧ ψ) ≡ ¬ϕ ∨ ¬ψ ¬EF ϕ ≡ AG¬ϕ ¬EU (ϕ, ψ) ≡ AR(¬ϕ, ¬ψ) ¬AXϕ ≡ EX¬ϕ ¬AGϕ ≡ EF ¬ϕ ¬AR(ϕ, ψ) ≡ EU (¬ϕ, ¬ψ) ¬EXϕ ≡ AX¬ϕ ¬EGϕ ≡ AF ¬ϕ ¬ER(ϕ, ψ) ≡ AU (¬ϕ, ¬ψ) Lemma 3. Let ϕ be a CTL proposition of NNF. If M, s |= ϕ, then M, s |= a ϕ.
Proof. By induction on the structure of ϕ. The cases ϕ = p, ¬p,

ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ ϕ 2 , AXϕ 1 , EXϕ 1 are trivial.
For the other cases, the proof is as follows.

-Let ϕ = AF ϕ 1 . We prove the contraposition. If there is a lsr-path ρ(s

)(j, k) s.t. ∀0 ≤ i < k, M, ρ i | = ϕ 1 , then by Lemma 1, there exists an infinite path ρ j 0 ˆ(ρ k j+1 ) ω , which is a counterexample of M, s |= AF ϕ 1 . Thus for each lsr-path ρ(s), ∃0 ≤ i < len(ρ)-1 s.t. M, ρ i |= ϕ 1 holds.
Then by induction hypothesis (IH), for each lsr-path ρ(s), ∃0 ≤ i < len(ρ) -1 s.t. M, ρ i |= a ϕ 1 holds, and thus M, s |= a AF ϕ 1 holds.

-Let ϕ = EF ϕ 1 . By the semantics of CTL, there exists an infinite path π(s) and ∃i ≥ 0 s.t.

M, π i |= ϕ 1 holds, and M, π i |= a ϕ 1 holds by IH. Then by Lemma 2, there exists a lsr-path ρ(s) s.t. π i is on ρ, and thus M, s |= a EF ϕ 1 holds. -Let ϕ = AU (ϕ 1 , ϕ 2 ). We prove the contraposition. Assume that there exists a lsr-path

-Let ϕ = AGϕ 1 . We prove the contraposition. If there is a lsr-path ρ(s)(j, k) and ∃0 ≤ i < k s.t. M, ρ i | = ϕ 1 , then by Lemma 1, there exists an infinite path ρ j 0 ˆ(ρ k j+1 ) ω , which is a counterexample of M, s |= AGϕ 1 . Thus for each lsr-path ρ(s)(j, k) and ∀0 ≤ i < k, M, ρ i |= ϕ 1 holds. Then by IH, for each lsr-path ρ(s)(j, k) and ∀0 ≤ i < k, M, ρ i |= a ϕ
ρ(s)(l, k) s.t. ∀0 ≤ i < k, M, ρ i | = ϕ 2 or ∀0 ≤ i < k, if M, ρ i |= ϕ 2 holds, then ∃0 ≤ j < i, M, ρ j | = ϕ 1 .
Then by Lemma 1, there exists an infinite path

ρ l 0 ˆ(ρ k l+1 ) ω , which is a counterexample of M, s |= AU (ϕ 1 , ϕ 2 ). Thus for each lsr-path ρ(s), ∃0 ≤ i < len(ρ) -1 s.t. M, ρ i |= ϕ 2 holds and ∀0 ≤ j < i, M, ρ j |= ϕ 1 holds. Then by IH, for each lsr-path ρ(s), ∃0 ≤ i < len(ρ) -1 s.t. M, ρ i |= a ϕ 2 holds and ∀0 ≤ j < i, M, ρ j |= a ϕ 1 holds. Thus M, s |= a AU (ϕ 1 , ϕ 2 ) holds. -Let ϕ = EU (ϕ 1 , ϕ 2 )
. By the semantics of CTL, there exists an infinite path π(s) and ∃i ≥ 0 s.t. M, π i |= ϕ 2 and ∀0 ≤ j < i, M, π j |= ϕ 1 . From the path π i 0 , by Lemma 2, there exists a path π m 0 without repeating states s.t.

π 0 = π 0 , π m = π i , and ∀0 < n < m, π n is on π i 0 . Then by IH, M, π m |= a ϕ 2 and ∀0 ≤ n < m, M, π n |= a ϕ 1 . Thus M, s |= a EU (ϕ 1 , ϕ 2 ) holds. -Let ϕ = AR(ϕ 1 , ϕ 2 ).
We prove the contraposition. If there exists a lsr-path ρ(s) and

∃0 ≤ i < len(ρ) -1 s.t. M, ρ i | = ϕ 2 and ∀0 ≤ j < i, M, ρ j | = ϕ 1 . Then ρ i 0 is a counterexample of M, s |= AR(ϕ 1 , ϕ 2 ). Thus for each lsr-path ρ(s) and ∀0 ≤ i < len -1, either M, ρ i |= ϕ 2 or ∃0 ≤ j < i s.t. M, ρ j |= ϕ 1 . By IH, for each ρ(s) and ∀0 ≤ i < len -1, either M, ρ i |= a ϕ 2 or ∃0 ≤ j < i s.t. M, ρ j |= a ϕ 1 . Thus M, s |= a AR(ϕ 1 , ϕ 2 ) holds. -Let ϕ = ER(ϕ 1 , ϕ 2 )
. By the semantics of CTL, there exists an infinite path π(s)

s.t. ∀j ≥ 0, either M, π j |= ϕ 2 holds or ∃0 ≤ i < j s.t. M, π i |= ϕ 1 holds. By Lemma 1, ∃k ≤ 0 s.t. π k 0 is a lsr-path and by IH, ∀0 ≤ m < k, either M, π m |= a ϕ 2 holds or ∃0 ≤ n < m s.t. M, π n |= a ϕ 1 holds. Thus M, s |= a ER(ϕ 1 , ϕ 2 ) holds. Lemma 4. Let ϕ be a CTL proposition of NNF. If M, s |= a ϕ, then M, s |= ϕ.
Proof. By induction on the structure of the proposition ϕ. The cases ϕ = p, ¬p, ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ ϕ 2 , AXϕ 1 , EXϕ 1 are trivial. For the other cases, the proof is as follows.

-Let ϕ = AF ϕ 1 . If there is an infinite path π(s) s.t. ∀j ≥ 0, M, π j | = a ϕ 1 , then by Lemma -Let ϕ = AU (ϕ 1 , ϕ 2 ). Assume that there exists an infinite path π(s) and ∀j ≥ 0, either

M, π j | = a ϕ 2 or ∃0 ≤ i < j s.t. M, π i | = a ϕ 1 . Then by Lemma 1, ∃k ≥ 0 s.t. π k 0 is a lsr-path, which is a counterexample of M, s |= a AU (ϕ 1 , ϕ 2 ). Thus for each infinite path π(s), ∃i ≥ 0 s.t. M, π i |= a ϕ 2 and ∀0 ≤ m < i, M, π m |= a ϕ 1 . Then by IH, for each infinite path π(s), ∃i ≥ 0 s.t. M, π i |= ϕ 2 and ∀0 ≤ m < i, M, π m |= ϕ 1 . Thus M, s |= AU (ϕ 1 , ϕ 2 ) holds. -Let ϕ = EU (ϕ 1 , ϕ 2 )
. By the alternative semantics of CTL, there exists a lsr-path ρ(s) and

∃0 ≤ i < len(ρ) -1 s.t. M, ρ i |= a ϕ 2 and ∀0 ≤ j < i, M, ρ j |= a ϕ 1 . Then by IH, M, ρ i |= ϕ 2 holds and ∀0 ≤ j < i, M, ρ j |= ϕ 1 holds. Thus M, s |= EU (ϕ 1 , ϕ 2 ) holds. -Let ϕ = AR(ϕ 1 , ϕ 2 ).
Assume that there exists a path π(s) and ∃j ≥ 0 s.t. M, π j | = a ϕ 2 and ∀0 ≤ i < j, M, π i | = a ϕ 1 . By Lemma 2, there exists a finite path π m 0 without repeating states s.t. π 0 = π 0 , π m = π j , and ∀0 < n < m, π n is on π j 0 . By the alternative semantics of CTL, π m 0 is a counterexample of M, s |= a AR(ϕ 1 , ϕ 2 ). Thus for each infinite path π(s), by IH, ∀j ≥ 0, either M, π j |= ϕ 2 or ∃0 ≤ i < j s.t. M, π i |= ϕ 1 . By the semantics of CTL, M, s |= AR(ϕ 1 , ϕ 2 ) holds.

-Let ϕ = ER(ϕ 1 , ϕ 2 ). By the alternative semantics of CTL, there exists a lsr-path ρ(s)(j, k)

s.t. ∀0 ≤ i < k, either M, ρ i |= a ϕ 2 or ∃0 ≤ m < i s.t. M, ρ m |= a ϕ 1 . Then by IH, either M, ρ i |= ϕ 2 or ∃0 ≤ m < i s.t. M, ρ m |= ϕ 1 . By Lemma 1, ρ j 0 ˆ(ρ k j+1
) ω is an infinite path, thus by the semantics of CTL, M, s |= ER(ϕ 1 , ϕ 2 ) holds.

Theorem 1. Let ϕ be a CTL proposition. M, s |= ϕ iff M, s |= a ϕ.

Rewrite Rules for CTL

The work in this section is to express CTL propositions in Deduction Modulo and prove that for a CTL proposition ϕ, the translation of M, s |= a ϕ is provable if and only if M, s |= a ϕ holds. So we fix such a model M = (S, next, L). As in [START_REF] Dowek | Axiomatizing Truth in a Finite Model[END_REF], we consider a two sorted language L, which contains constants s 1 , . . . , s n for each state of M .

predicate symbols ε 0 , ε 0 , ε 0 , ε 1 , ε 1 , ε 1 , in which the binary predicates ε 0 , ε 0 and ε 0 apply to all the CTL propositions, while the ternary predicates ε 1 , ε 1 and ε 1 only apply to the CTL propositions starting with the temporal connectives AG, EG, AR and ER. binary predicate symbols mem for the membership, r for the next-notation.

a constant nil and a binary function symbol con.

We use x, y, z to denote the variables of the state terms, X, Y, Z to denote the class variables. A class is in fact a set of states, here we use the class theory, rather than the (monadic) second order logic, is to emphasis that this formalism is a theory and not a logic. Note that we use Φ, Ψ to denote the variables of the CTL terms. Both finite sets and finite paths are represented with the symbols con and nil. For the set S = {s i , . . . , s j }, we use [S ] to denote its term form con(s i , con(. . . , con(s j , nil) . . .)). For the finite path s j i = s i , . . . , s j , we use [s j i ] to denote the term con(s j , con(. . . , con(s i , nil) . . .)). And then the proposition ϕ holds on s is expressed as ε 0 (|ϕ|, s).

To express CTL in

Definition 5 (Semantics of L). Semantics of the propositions in the language L is as follows.

M |= ε 0 (|ϕ|, s) ⇔ M, s |= a ϕ M |= ε 0 (|ϕ|, [S ]) ⇔ ∀s ∈ S , M, s |= a ϕ M |= ε 0 (|ϕ|, [S ]) ⇔ ∃s ∈ S s.t. M, s |= a ϕ M |= ε 1 (ag(|ϕ 1 |), s, [s i 0 ]) ⇔ ∀ lsr-path s i 0 ˆsk i+1 (s i+1 = s), and ∀i < j < k, M, s j |= a ϕ 1 M |= ε 1 (eg(|ϕ 1 |), s, [s i 0 ]) ⇔ ∃ lsr-path s i 0 ˆsk i+1 (s i+1 = s), and ∀i < j < k, M, s j |= a ϕ 1 M |= ε 1 (ar(|ϕ 1 |, |ϕ 2 |), s, [s i 0 ]) ⇔ ∀ lsr-path s i 0 ˆsk i+1 (s i+1 = s), and ∀i < j < k, either M, s j |= a ϕ 2 or ∃i < m < j s.t. M, s m |= a ϕ 1 M |= ε 1 (er(|ϕ 1 |, |ϕ 2 |), s, [s i 0 ]) ⇔ ∃ lsr-path s i 0 ˆsk i+1 (s i+1 = s), and ∀i < j < k, either M, s j |= a ϕ 2 or ∃i < m < j s.t. M, s m |= a ϕ 1 M |= ε 1 (ag(|ϕ 1 |), [S ], [s i 0 ]) ⇔ ∀s ∈ S , M |= ε 1 (ag(|ϕ 1 |), s, [s i 0 ]) M |= ε 1 (ar(|ϕ 1 |, |ϕ 2 |), [S ], [s i 0 ]) ⇔ ∀s ∈ S , M |= ε 1 (ar(|ϕ 1 |, |ϕ 2 |), s, [s i 0 ]) M |= ε 1 (eg(|ϕ 1 |), [S ], [s i 0 ]) ⇔ ∃s ∈ S s.t. M |= ε 1 (eg(|ϕ 1 |), s, [s i 0 ]) M |= ε 1 (er(|ϕ 1 |, |ϕ 2 |), [S ], [s i 0 ]) ⇔ ∃s ∈ S s.t. M |= ε 1 (er(|ϕ 1 |, |ϕ 2 |), s, [s i 0 ]) M |= r(s, [S ]) ⇔ S = next(s) M |= mem(s, [s i 0 ]) ⇔ s is on the path s i 0 Example 2.
For the Kripke structure M in Fig. 3, we have M |= ε 1 (eg(p), s 3 , con(s 2 , con(s 1 , nil))) because there exists a lsr-path, for instance s 1 , s 2 , s 3 , s 4 , s 2 such that p holds on s 3 and s 4 .

Note that when a proposition ε 1 (|ϕ|, s, [s j i ]) is valid in M , for instance M |= ε 1 (eg(|ϕ|), s, [s j i ]), EGϕ may not hold on the state s. The Rewrite System R The rewrite system has three components, 1. rules for the Kripke structure M (denoted as R M ), 2. rules for the class variables (denoted as R c ), 3. rules for the semantics encoding of the CTL operators (denoted as R CT L ).

The Rules of R M The rules of R M are as follows:

for each atomic proposition p ∈ AP and each state s ∈ S, if p ∈ L(s), then ε 0 (p, s) → is in R M , otherwise take ε 0 (not(p), s) → as a rewrite rule of R M . for each state s ∈ S, take r(s, [next(s)]) → as a rewrite rule of R M .

The Rules of R c For the class variables, as the domain of the model is finite, there exists two axioms [START_REF] Dowek | Axiomatizing Truth in a Finite Model[END_REF], ∀x(x = x), ∀x∀y∀Z((x = y ∨ mem(x, Z)) ⇒ mem(x, con(y, Z))).

The rewrite rules for these axioms are x = x → and mem(x, con(y, Z)) → x = y ∨ mem(x, Z).

To delete the predicate "=" introduced by the rules, we use the set of rules (R c ) mem(x, con(x, Z)) → , mem(x, con(y, Z)) → mem(x, Z) instead. The Rules of R CT L The rewrite rules for the predicates carrying the semantic definition of the CTL propositions, are in Fig. 4. For example, the rule

ε 1 (eg(|ϕ|), s, [s j i ]) → mem(s, [s j i ]) ∨ (ε 0 (|ϕ|, s) ∧ ∃X(r(s, X) ∧ ε 1 (eg(|ϕ|), X, con(s, [s j i ]))))
means that M |= ε 1 (eg(|ϕ|), s, [s j i ]) holds, if and only if s j i ˆs is a lsr-path, that is s occurs in s j i , or M |= ε 0 (|ϕ|, s) and M |= ε 1 (eg(|ϕ|), [next(s)], con(s, [s j i ])) holds.

Now we are ready to prove the main theorem. Our goal is to prove that M |= ε 0 (|ϕ|, s) holds if and only if ε 0 (|ϕ|, s) is provable in Deduction Modulo.

Lemma 5 (Soundness). For a CTL formula ϕ of NNF, if the sequent cf R ε 0 (|ϕ|, s) has a proof, then M |= ε 0 (|ϕ|, s).

Proof. More generally, we prove that for any CTL proposition ϕ of NNF,

-if cf R ε 0 (|ϕ|, s) has a proof, then M |= ε 0 (|ϕ|, s). -if cf R ε 0 (|ϕ|, [S ]) has a proof, then M |= ε 0 (|ϕ|, [S ]). -if cf R ε 0 (|ϕ|, [S ]) has a proof, then M |= ε 0 (|ϕ|, [S ]). -if cf R ε 1 (|ϕ|, s, [s j i ]) has a proof, in which ϕ is either of the form AGϕ 1 , EGϕ 1 , AR(ϕ 1 , ϕ 2 ), ER(ϕ 1 , ϕ 2 ), then M |= ε 1 (|ϕ|, s, [s j i ]). ε0(or(Φ, Ψ ), x) → ε0(Φ, x) ∨ ε0(Ψ, x) ε0(and(Φ, Ψ ), x) → ε0(Φ, x) ∧ ε0(Ψ, x) ε0(ax(Φ), x) → ∃X(r(x, X) ∧ ε 0 (Φ, X)) ε0(ex(Φ), x) → ∃X(r(x, X) ∧ ε 0 (Φ, X)) ε0(af(Φ), x)) → ε0(Φ, x) ∨ ∃X(r(x, X) ∧ ε 0 (af(Φ), X)) ε0(ef(Φ), x)) → ε0(Φ, x) ∨ ∃X(r(x, X) ∧ ε 0 (ef(Φ), X)) ε0(ag(Φ), x) → ε1(ag(Φ), x, nil) ε0(eg(Φ), x) → ε1(eg(Φ), x, nil) ε0(au(Φ, Ψ ), x) → ε0(Ψ, x) ∨ (ε0(Φ, x) ∧ ∃X(r(x, X) ∧ ε 0 (au(Φ, Ψ ), X))) ε0(eu(Φ, Ψ ), x) → ε0(Ψ, x) ∨ (ε0(Φ, x) ∧ ∃X(r(x, X) ∧ ε 0 (eu(Φ, Ψ ), X))) ε0(ar(Φ, Ψ ), x) → ε1(ar(Φ, Ψ ), x, nil) ε0(er(Φ, Ψ ), x) → ε1(er(Φ, Ψ ), x, nil) ε 0 (Φ, con(x, X)) → ε0(Φ, x) ∧ ε 0 (Φ, X) ε 0 (Φ, nil) → ε 0 (Φ, con(x, X)) → ε0(Φ, x) ∨ ε 0 (Φ, X) ε1(ag(Φ), x, Y ) → mem(x, Y ) ∨ (ε0(Φ, x) ∧ ∃X(r(x, X) ∧ ε 1 (ag(Φ), X, con(x, Y )))) ε1(eg(Φ), x, Y ) → mem(x, Y ) ∨ (ε0(Φ, x) ∧ ∃X(r(x, X) ∧ ε 1 (eg(Φ), X, con(x, Y )))) ε1(ar(Φ, Ψ ), x, Y ) → mem(x, Y ) ∨ (ε0(Ψ, x) ∧ (ε0(Φ, x) ∨ ∃X(r(x, X) ∧ ε 1 (ar(Φ, Ψ ), X, con(x, Y ))))) ε1(er(Φ, Ψ ), x, Y ) → mem(x, Y ) ∨ (ε0(Ψ, x) ∧ (ε0(Φ, x) ∨ ∃X(r(x, X) ∧ ε 1 (er(Φ, Ψ ), X, con(x, Y ))))) ε 1 (Φ, con(x, X), Y ) → ε1(Φ, x, Y ) ∧ ε 1 (Φ, X, Y ) ε 1 (Φ, nil, Y ) → ε 1 (Φ, con(x, X), Y ) → ε1(Φ, x, Y ) ∨ ε 1 (Φ, X, Y ) Fig. 4. Rewrite Rules for CTL Connectives (RCT L) -if cf R ε 1 (|ϕ|, [S ], [s j i ]) has a proof, in which ϕ is either of the form AGϕ 1 , AR(ϕ 1 , ϕ 2 ), then M |= ε 1 (|ϕ|, [S ], [s j i ]). -if cf R ε 1 (|ϕ|, [S ], [s j i ]) has a proof, in which ϕ is either of the form EGϕ 1 , ER(ϕ 1 , ϕ 2 ), then M |= ε 1 (|ϕ|, [S ], [s j i ]).
By induction on the size of the proof. Consider the different case for ϕ, we have 18 cases (2 cases for the atomic proposition and its negation, 2 cases for and and or, 10 cases for the temporal connectives ax, ex, af, ef, ag, eg, au, eu, ar, er, 4 cases for the predicate symbols ε 0 , ε 0 , ε 1 , ε 0 ), but each case is easy. For brevity, we just prove some of the cases. The full proof is in [START_REF] Ji | CTL Model Checking in Deduction Modulo[END_REF].

-Suppose cf R ε 0 (ex(|ϕ|), s) has a proof. As ε 0 (ex(|ϕ|), s) → ∃X(r(s, X) ∧ ε 0 (|ϕ|, X)), the last rule of the proof is ∃. By induction hypothesis(IH), there exists S s.t. M |= r(s, [S ]) ∧ ε 0 (|ϕ|, [S ]), thus S = next(s) and there exists a state s in S s.t. M |= ε 0 (|ϕ|, s ) holds. Then M, s |= ε 0 (ex(|ϕ|), s) holds by its semantic definition. Proof. By induction on the structure of ϕ. For brevity, here we just prove some of the cases. The full proof is in [START_REF] Ji | CTL Model Checking in Deduction Modulo[END_REF].

-Suppose cf R ε 1 (eg(|ϕ|), s, [s j i ]) has a proof. As ε 1 (eg(|ϕ|), s, [s j i ]) → mem(s, [s j i ])∨(ε 0 (|ϕ|, s)∧ ∃X(r(s, X)∧ε 1 (eg(|ϕ|), X, con(s, [s j i ])))), the last rule in the proof is ∨ 1 or ∨ 2 . For ∨ 1 , M |= mem(s, [s j i ])
-Suppose cf R ε 0 (eu(|ϕ 1 |, |ϕ 2 |), s) has a proof. As ε 0 (eu(|ϕ 1 |, |ϕ 2 |), s) → ε 0 (|ϕ 2 |, s)∨(ε 0 (|ϕ 1 |, s)∧ ∃X(r(s, X) ∧ ε 0 (eu(|ϕ 1 |, |ϕ 2 |), X))), the last rule in the proof is ∨ 1 or ∨ 2 . For ∨ 1 , M |=
≤ n < m, M |= ε 0 (|ϕ 1 |, ρ n ) holds. For the path ρ (j, k), • if ∀0 ≤ i < k, ρ i = s, then sˆρ (j, k) is a lsr-path, in which M |= ε 0 (|ϕ 2 |, ρ m ) holds and ∀0 ≤ n < m, M |= ε 0 (|ϕ 1 |, ρ n ) holds, • if ∃m < i < k s.t. ρ i = s, then sˆρ i 0 is a lsr-path, in which M |= ε 0 (|ϕ 2 |, ρ m ) holds and ∀0 ≤ n < m, M |= ε 0 (|ϕ 1 |, ρ n ) holds, • if ∃0 ≤ i < m s.t. ρ i = s and i ≤ j, then ρ k i is a lsr-path, in which M |= ε 0 (|ϕ 2 |, ρ m ) holds and ∀i ≤ n < m M |= ε 0 (|ϕ 1 |, ρ n ) holds, • if ∃0 ≤ i < m s.t. ρ i = s and i > j, then ρ k i ˆρ i j+1 is a lsr-path, in which M |= ε 0 (|ϕ 2 |, ρ m ) holds and ∀i ≤ n < m, M |= ε 0 (|ϕ 1 |, ρ n ) holds. Thus M |= ε 0 (eu(|ϕ 1 |, |ϕ 2 |), s) holds by its semantic definition. -Suppose cf R ε 0 (|ϕ|, con(s, [S ])) has a proof. As ε 0 (|ϕ|, con(s, [S ])) → ε 0 (|ϕ|, s)∨ε 0 (|ϕ|, [S ]), the last rule in the proof is ∨ 1 or ∨ 2 . For ∨ 1 , M |= ε 0 (|ϕ|,
-Suppose M |= ε 0 (ag(|ϕ 1 |), s) holds. By the semantics of L, for each state s on each lsr-path starting from s, M |= ε 0 (|ϕ 1 |, s ) holds. Thus there exists a finite tree T such that • T has root s,

• for each internal node s in T , the children of s are labelled by the elements of next(s ),

• the branch starting from s to each leaf is a lsr-path,

• for each internal node s in T , M |= ε 0 (|ϕ 1 |, s ) holds and by IH, there exists a proof

Π (ϕ1,s ) for the sequent cf R ε 0 (|ϕ 1 |, s ). Then, to each subtree T of T , we associate a proof |T | of the sequent cf R ε 1 (ag(|ϕ 1 |), s , [s k-1 0 ]
) where s is the root of T and s k 0 (s k = s ) is the branch from s to s , by induction, as follows, • if T contains a single node s , then s k 0 is a lsr-path and the proof is as follows

: cf R mem(s , [s k-1 0 ]) ∨1 cf R ε1(ag(|ϕ1|), s , [s k-1 0 ]) • if T = s (T 0 , . . . , T n ) 1
, the proof is as follows:

Π s cf R ε0(|ϕ1|, s ) cf R r(s , [next(s )]) |T0| . . . |Tn| ∧ n cf R ε 1 (ag(|ϕ1|), [next(s )], [s k 0 ]) ∧ cf R r(s , [next(s )]) ∧ ε 1 (ag(|ϕ1|), [next(s )], [s k 0 ]) ∃ cf R ∃X(r(s , X) ∧ ε 1 (ag(|ϕ1|), X, [s k 0 ])) ∧ cf R ε0(|ϕ1|, s ) ∧ ∃X(r(s , X) ∧ ε 1 (ag(|ϕ1|), X, [s k 0 ])) ∨2 cf R ε1(ag(|ϕ1|), s , [s k-1 0 ])
1 s (T0, . . . , Tn) is a tree, in which s is the root, T0, . . . , Tn are the sub-trees.

This way, as ε 0 (ag(|ϕ 1 |), s) can be rewritten into ε

1 (ag(|ϕ 1 |), s, nil), |T | is a proof for the sequent cf R ε 0 (ag(|ϕ 1 |), s). -Suppose M |= ε 0 (ef(|ϕ 1 |), s) holds.
By the semantics of L, there exists a lsr-path s k 0 starting from s and ∃0 ≤ j < k s.t. M |= ε 0 (ef(|ϕ 1 |), s j ) and by IH, there exists a proof Π (ϕ1,sj ) for the sequent cf R ε 0 (|ϕ 1 |, s j ). To each subpath s j i of s j 0 , we associate a proof |s j i | for the sequent cf R ε 0 (ef(|ϕ 1 |), s i ), by induction, as follows, • if s j i contains a single node s j , then the proof |s j i | is as follows:

Π (ϕ 1 ,s j ) ∨1 cf R ε0(ef(|ϕ1|), sj)
• Otherwise, assume next(s i ) = {s 0 , . . . , s n } and s i+1 = s m , the proof

|s j i | is as follows: cf R r(si, [next(si)]) |s j i+1 | ∨1 cf R ε 0 (ef(|ϕ1|), con(s m , [S ])) ∨ m 2 cf R ε 0 (ef(|ϕ1|), [next(si)]) ∧ cf R r(si, [next(si)]) ∧ ε 0 (ef(|ϕ1|), [next(si)]) ∃ cf R ∃X(r(si, X) ∧ ε 0 (ef(|ϕ1|), X)) ∨2 cf R ε0(ef(|ϕ1|), si)
This way, • if s j i contains a single node s j , then the proof is as follows:

|s j 0 | is a proof of the sequent cf R ε 0 (ef(|ϕ 1 |), s). -Suppose M |= ε 0 (eu(|ϕ 1 |, |ϕ 2 |),
Π (ϕ 2 ,s j ) ∨1 cf R ε0(eu(|ϕ1|, |ϕ2|), sj)
• Otherwise, assume next(s i ) = {s 0 , . . . , s n } and s i+1 = s m , the proof |s j i | is as follows:

Π (ϕ 1 ,s i ) cf R r(si, [next(si)]) |s j i+1 | ∨1 cf R ε 0 (eu(|ϕ1|, |ϕ2|), con(s m , [S ])) ∨ m 2 cf R ε 0 (eu(|ϕ1|, |ϕ2|), [next(si)]) ∧ cf R r(si, [next(si)]) ∧ ε 0 (eu(|ϕ1|, |ϕ2|), [next(si)]) ∃ cf R ∃X(r(si, X) ∧ ε 0 (eu(|ϕ1|, |ϕ2|), X)) ∧ cf R ε0(|ϕ1|, si) ∧ ∃X(r(si, X) ∧ ε 0 (eu(|ϕ1|, |ϕ2|), X)) ∨2 cf R ε0(eu(|ϕ1|, |ϕ2|), si)
This way, 6 Automated Theorem Proving Modulo

|s j 0 | is a proof of the sequent cf R ε 0 (eu(|ϕ 1 |, |ϕ 2 |), s).

Polarized Resolution Modulo

In Polarized Resolution Modulo, the polarized rewrite rules are taken as one-way clauses [START_REF] Dowek | Polarized Resolution Modulo[END_REF]. For example, the rewrite rule

ε 1 (eg(Φ), x, Y ) → + mem(x, Y ) ∨ (ε 0 (Φ, x) ∧ ∃X(r(x, X) ∧ ε 1 (eg(Φ), X, con(x, Y ))))
is translated into two one-way clauses

ε 1 (eg(Φ), x, Y ) ∨ mem(x, Y ) ⊥ ε 1 (eg(Φ), x, Y ) ∨ ε 0 (Φ, x) ⊥ ∨ r(x, X) ⊥ ∨ ε 1 (eg(Φ), X, con(x, Y )) ⊥
in which the underlined literals have the priority to do resolution. Example 3. For the transition system M in Fig. 5, we prove that M, s 1 |= a EXEGp.

The one-way clauses for the system are: ε 0 (not(p), s 1 ), ε 0 (p, s 2 ), ε 0 (p, s 3 ), r(s 1 , con(s 2 , nil)), r(s 2 , con(s 3 , nil)), r(s 3 , con(s 2 , nil)).

The translation of M, s 1 |= a EXEGp is ε 0 (ex(eg(p)), s 1 ) and the resolution steps start from ε 0 (ex(eg(p)), s 1 ) ⊥ .

First apply resolution with one-way clause ε 0 (ex(Φ), x) ∨ r(x, X) ⊥ ∨ ε 0 (Φ, X) ⊥ , with x = s 1 and Φ = eg(p), this yields r(s 1 , X) ⊥ ∨ ε 0 (eg(p), X) ⊥ .

Then apply resolution with one-way clause r(s 1 , con(s 2 , nil)), with X = con(s 2 , nil), this yields ε 0 (eg(p), con(s 2 , nil)) ⊥ .

Then apply resolution with one-way clause ε 0 (Φ, con(x, X)) ∨ ε 0 (Φ, x) ⊥ , with x = s 2 , X = nil and Φ = eg(p), this yields ε 0 (eg(p), s 2 ) ⊥

Then apply resolution with one-way clause ε 0 (eg(Φ), x) ∨ ε 1 (eg(Φ), x, nil) ⊥ , with Φ = p and x = s 2 , this yields ε 1 (eg(p), s 2 , nil) ⊥

Then apply resolution with one-way clause ( ‡ 2 ), with Φ = p, x = s 2 and Y = nil, this yields

ε 0 (p, s 2 ) ⊥ ∨ r(s 2 , X) ⊥ ∨ ε 1 (eg(p), X, con(s 2 , nil)) ⊥ .
Then apply resolution with one-way clause ε 0 (p, s 2 ), this yields

r(s 2 , X) ⊥ ∨ ε 1 (eg(p), X, con(s 2 , nil)) ⊥ .
Then apply resolution with one-way clause r(s 2 , con(s 3 , nil)), with X = con(s 3 , nil), this yields ε 1 (eg(p), con(s 3 , nil), con(s 2 , nil)) ⊥

Then apply resolution with one-way clause ε

1 (Φ, con(x, X), Y ) ∨ ε 1 (Φ, x, Y ) ⊥ , with Φ = eg(p), x = s 3 , X = nil and Y = con(s 2 , nil), this yields 2 ‡ is ε1(eg(Φ), x, Y ) ∨ ε0(Φ, x) ⊥ ∨ r(x, X) ⊥ ∨ ε 1 (eg(Φ), X, con(x, Y )) ⊥ ε 1 (eg(p), s 3 , con(s 2 , nil)) ⊥
Then apply resolution with one-way clause ( ‡), with Φ = p, x = s 3 and Y = con(s 2 , nil), this yields ε 0 (p, s 3 ) ⊥ ∨ r(s 3 , X) ⊥ ∨ ε 1 (eg(p), X, con(s 3 , con(s 2 , nil))) ⊥ .

Then apply resolution with one-way clause ε 0 (p, s 3 ), this yields r(s 3 , X) ⊥ ∨ ε 1 (eg(p), X, con(s 3 , con(s 2 , nil))) ⊥ .

Then apply resolution with one-way clause r(s 3 , con(s 2 , nil)), with X = con(s 2 , nil), this yields ε 1 (eg(p), con(s 2 , nil), con(s 3 , con(s 2 , nil))) ⊥

Then apply resolution with one-way clause ε

1 (Φ, con(x, X), Y ) ∨ ε 1 (Φ, x, Y ) ⊥ , with Φ = eg(p), x = s 3 , X = nil and Y = con(s 2 , nil), this yields ε 1 (eg(p), s 2 , con(s 3 , con(s 2 , nil))) ⊥
Then apply resolution with one-way clause ε 1 (eg(Φ), x, Y ) ∨ mem(x, Y ) ⊥ , with x = s 2 and Y = con(s 3 , con(s 2 , nil)), this yields mem(s 2 , con(s 3 , con(s 2 , nil))) ⊥

Then apply resolution with one-way clause mem(x, con(y, Z))∨mem(x, Z) ⊥ , with x = s 2 , y = s 3 and Z = con(s 2 , nil), this yields mem(s 2 , con(s 2 , nil)) ⊥

Then apply resolution with one-way clause mem(x, con(x, Z)), with x = s 2 and Z = nil, this yields the empty clause. Thus M, s 1 |= a EXEGp holds.

Experimental Evaluation

In this Section, we give a comparison between Resolution-based and QBF-based verification, that are implemented in iProver Modulo and VERDS [START_REF] Zhang | VERDS Modeling Language[END_REF] respectively. iProver Modulo is a prover by intergate Polarized Resolution Modulo into iProver [START_REF] Korovin | iProver-An Instantiation-Based Theorem Prover for First-Order Logic (System Description)[END_REF]. The comparison is based on 24 CTL properties and two kinds of programs: Programs with Concurrent Processes and Programs with Concurrent Sequential Processes. The programs and CTL properties refer to [START_REF] Zhang | QBF Encoding of Temporal Properties and QBF-based Verification[END_REF].

For the programs with concurrent processes, each testing case contains 12/24 variables and 3 processes. For the programs with concurrent sequential processes, each testing case contains 12/16 variables and 2 processes. All the cases are tested on Intel Core TM i5-2400 CPU @ 3.10GHz × 4 with Linux and the testing time of each case is limited to 20 minutes. The experimental data is presented in Table 1 and2. The comparison is based on two aspects: the number of testing cases that can be proved, and the time used if a problem can be proved in both.

-As can be seen in Table 1, among the 960 testing cases of the concurrent processes, 94 of them are timeout in iProver, while the number in VERDS is 99. For the concurrent sequential processes, among the 960 testing cases, 173 of them are timeout in iProver, while in VERDS, the number is 260. -Table 2 shows that, among the 818 testing cases of the programs of concurrent processes, that are both proved in iProver and VERDS, iProver performs better in 272 of them and among the 678 testing cases of the programs of concurrent sequential processes, 412 of them run faster in iProver.

In summary, for the 1920 testing cases, 1653 (86%) of them are solved by iProver, while 1561 (81%) are solved by VERDS. For all the 1496 testing cases that are both proved, 684 (45.8%) testing cases run faster in iProver.

Conclusion and Future Work

In this paper, we defined an alternative semantics for CTL, which is bounded to lsr-paths. Based on the alternative semantics, a way to embed model checking problems into Deduction Modulo has been presented. Thus this work has given a method to solve model checking problems in automated theorem provers, without losing the advantages of model checking approaches. An experimental evaluation of this approach using resolution modulo has been presented. The comparison with the QBF-based verification showed that automated theorem proving modulo, which performed as well as QBF-based method, can be considered as a new way to quickly determine whether a property is violated in transition system models.

The proof-search method does not work well on proving some temporal propositions, such as the propositions start with AG. One of the reasons is during the search steps, it may visit the same state repeatedly. To design new rewrite rules for the encoding of temporal connectives or new elimination rules to avoid this problem remains as future work.

Fig. 2 .

 2 Fig. 2. Example of CTL

  1 holds, and thus M, s |= a AGϕ 1 holds. -Let ϕ = EGϕ 1 . By the semantics of CTL, there exists an infinite path π(s) s.t. ∀i ≥ 0, M, π i |= ϕ 1 holds. Then by Lemma 1, ∃k ≥ 0 s.t. π k 0 is a lsr-path and by IH, ∀0 ≤ i < k, M, π i |= a ϕ 1 holds. Thus M, s |= a EGϕ 1 holds.

  Deduction Modulo, firstly, we translate the CTL proposition ϕ into a term |ϕ| (called CTL term). Definition 4 (CTL Term). The term form of a CTL proposition is defined as follows: |p| = p, p ∈ AP |EXϕ| = ex(|ϕ|) |AU (ϕ, ψ)| = au(|ϕ|, |ψ|) |¬ϕ| = not(|ϕ|) |AF ϕ| = af(|ϕ|) |EU (ϕ, ψ)| = eu(|ϕ|, |ψ|) |ϕ ∧ ψ| = and(|ϕ|, |ψ|) |EF ϕ| = ef(|ϕ|) |AR(ϕ, ψ)| = ar(|ϕ|, |ψ|) |ϕ ∨ ψ| = or(|ϕ|, |ψ|) |AGϕ| = ag(|ϕ|) |ER(ϕ, ψ)| = er(|ϕ|, |ψ|) |AXϕ| = ax(|ϕ|) |EGϕ| = eg(|ϕ|)

Fig. 3 .

 3 Fig. 3. Example of L

  holds by IH, thus s j i ˆs is a lsr-path andM |= ε 1 (eg(|ϕ|), s, [s j i ]) holds by its semantic definition. For ∨ 2 , M |= ε 0 (|ϕ|, s) and M |= ∃X(r(s, X) ∧ ε 1 (eg(|ϕ|), X, con(s, [s] j i )))holds by IH. Thus there exists S s.t. M |= r(s, [S ]) and M |= ε 1 (eg(|ϕ|), [S ], con(s, [s j i ])) holds. Then S = next(s) and there exists a state s ∈ S s.t. M |= ε 1 (eg(|ϕ|), s , con(s, [s j i ])) holds. Thus M |= ε 1 (eg(|ϕ|), s, [s j i ]) holds by its semantic definition.

ε 0 (

 0 |ϕ 2 |, s) holds by IH, thus M |= ε 0 (eu(|ϕ 1 |, |ϕ 2 |), s) holds by its semantic definition. For ∨ 2 , M |= ε 0 (|ϕ 1 |, s) and M |= ∃X(r(s, X) ∧ ε 0 (eu(|ϕ 1 |, |ϕ 2 |), X)) holds by IH. Thus there exists S s.t. M |= r(s, [S ]) and M |= ε 0 (eu(|ϕ 1 |, |ϕ 2 |), [S ])) holds. Then we get S = next(s) and there exists a state s in S s.t. M |= ε 0 (eu(|ϕ 1 |, |ϕ 2 |), s ) holds. Thus there exists a lsr-path ρ (s )(j, k) and ∃1 ≤ m < k s.t. M |= ε 0 (|ϕ 2 |, ρ m ) holds and ∀0

  s) holds by IH, then M |= ε 0 (|ϕ|, con(s, [S ])) holds by its semantic definition. For ∨ 2 , M |= ε 0 (|ϕ|, [S ]) holds by IH, then we exists a state s ∈ S s.t. M |= ε 0 (|ϕ|, s ) holds, thus M |= ε 0 (|ϕ|, con(s, [S ])) holds by its semantic definition. Lemma 6 (Completeness). For a CTL formula ϕ of NNF, if M |= ε 0 (|ϕ|, s), then the sequent cf R ε 0 (|ϕ|, s) has a proof.

Theorem 2 (

 2 Soundness and Completeness). For a CTL proposition ϕ of NNF, the sequent cf R ε 0 (|ϕ|, s) has a proof iff M |= ε 0 (|ϕ|, s) holds.

Fig. 5 .

 5 Fig. 5. Resolution Example

  1, there exists k ≥ 0 s.t. π k 0 is a lsr-path, which is a counterexample of M, s |= a AF ϕ 1 . Thus for each infinite path π(s), ∃j ≥ 0 s.t. M, π j |= a ϕ 1 holds. Then by IH, for each infinite path π(s), ∃j ≥ 0 s.t. M, π j |= ϕ 1 holds and thus M, s |= AF ϕ 1 holds. -Let ϕ = EF ϕ 1 . By the alternative semantics of CTL, there exists a lsr-path ρ(s) and ∃0 ≤ i < len(ρ) -1 s.t. M, s i |= a ϕ 1 holds and by IH, M, s i |= ϕ 1 holds. As there exists a path from s to s i , we get M, s |= EF ϕ 1 holds. -Let ϕ = AGϕ 1 . Assume that there exists an infinite path π(s) and ∃i ≥ 0, M, π i | = a ϕ 1 . By Lemma 2, there exists a lsr-path ρ(s) s.t. π i is on ρ, which is a counterexample of M, s |= a AGϕ 1 . Thus for each infinite path π(s) and ∀i ≥ 0, M, π i |= a ϕ 1 holds. Then by IH, for each infinite path π(s) and ∀i ≥ 0, M, π i |= ϕ 1 holds and thus M, s |= AGϕ 1 holds. -Let ϕ = EGϕ 1 . By the alternative semantics of CTL, there exists a lsr-path ρ(s)(i, k) s.t. ∀0 ≤ j < k, M, ρ j |= a ϕ 1 and by IH, M, ρ j |= ϕ 1 . As ρ i 0 ˆ(ρ k i+1 ) ω is an infinite path, thus M, s |= EGϕ 1 holds.

  s) holds. By the semantics of L, there exists a lsr-path s k 0 starting from s and ∃0 ≤ j < k, s.t.M |= ε 0 (|ϕ 2 |, s j ) and ∀0 ≤ i < j, M |= ε 0 (|ϕ 1 |, s i ). By IH, for each state s , if M |= ε 0 (|ϕ 1 |, s ), then there exists a proof Π (ϕ1,s ) for the sequent cf R ε 0 (|ϕ 1 |, s ) and if M |= ε 0 (|ϕ 2 |, s ),then there exists a proof Π (ϕ2,s ) for the sequent cf R ε 0 (|ϕ 2 |, s ). To each subpath s j i of s j 0 , we associate a proof |s j i | for the sequent cf R ε 0 (eu(|ϕ 1 |, |ϕ 2 |), s), by induction, as follows,

Table 1 .

 1 Experimental Results

	iProver/Verds	Con. Processes		Con. Seq. Processes
	Prop Num	True	False >20m	True	False >20m
	p01	40	-	40/40	-	23/-	5/4	12/36
	p02	40	40/40	-	-	40/40	-	-
	p03	40	2/-	37/37	1/3	-	25/15	15/25
	p04	40	17/-	-23/40	-	-	40/40
	p05	40	25/34	6/5	9/1	24/24	8/2	8/14
	p06	40	31/40	-	9/-	36/31	-	4/9
	p07	40	40/40	-	-	40/40	-	-
	p08	40	40/40	-	-	40/40	-	-
	p09	40	32/32	8/8	-	35/29	5/1	-/10
	p10	40	40/40	-	-	40/40	-	-
	p11	40	10/10	30/30	-	27/23	8/4	5/13
	p12	40	40/40	-	-	40/35	-	-/5
	p13	40	-	40/40	-	-	40/40	-
	p14	40	3/3	37/37	-	3/3	37/33	-/4
	p15	40	5/-	33/33	2/7	-	23/15	17/25
	p16	40	19/-	-21/40	-	-	40/40
	p17	40	28/37	3/2	9/1	25/26	5/1	10/13
	p18	40	32/40	-	8/-	37/31	-	3/9
	p19	40	5/5	35/35	-	6/6	34/34	-
	p20	40	15/17	21/21	4/2	12/11	18/22	10/7
	p21	40	3/3	37/37	-	3/3	37/37	-
	p22	40	3/3	37/37	-	3/3	37/37	-
	p23	40	-	40/40	-	-	40/40	-
	p24	40	20/25	12/10	8/5	8/8	23/22	9/10
	Sum	960 450/449 416/412 94/99 442/393 345/307 173/260

Table 2 .

 2 Speed Comparisons a adv/T(F): have advantage in the speed when both return T(F). O(iP/Ver): only solved by iProver/Verds.

			Con. Processes	Con. Seq. Processes
	Prop Num adv/T adv/F O(iP/Ver) adv/T adv/F O(iP/Ver)
	p01	40	-	0/40	-	-	0/3	25/1
	p02	40	40/40	-	-	40/40	-	-
	p03	40	-	1/37	2/-	-	11/15	10/-
	p04	40	-	-	17/-	-	-	-
	p05	40	0/25	3/5	1/9	6/20	2/2	10/4
	p06	40	0/31	-	-/9	10/28	-	8/3
	p07	40	33/40	-	-	37/40	-	-
	p08	40	35/40	-	-	38/40	-	-
	p09	40	19/32	0/8	-	22/29	0/1	10/-
	p10	40	19/40	-	-	18/40	-	-
	p11	40	0/10	0/30	-	9/23	3/4	8/-
	p12	40	3/40	-	-	7/35	-	5/-
	p13	40	-	38/40	-	-	40/40	-
	p14	40	2/3	0/37	-	3/3	23/33	4/-
	p15	40	-	0/33	5/-	-	10/14	9/1
	p16	40	-	-	19/-	-	-	-
	p17	40	0/28	1/2	1/9	8/22	1/1	7/4
	p18	40	0/32	-	-/8	11/29	-	8/2
	p19	40	2/5	9/35	-	6/6	12/34	-
	p20	40	1/15	7/20	1/3	6/11	9/17	2/5
	p21	40	2/3	18/37	-	3/3	23/37	-
	p22	40	2/3	19/37	-	2/3	22/37	-
	p23	40	-	17/40	-	-	25/40	-
	p24	40	0/20	1/10	2/5	1/7	4/21	3/2
	Sum	960 158/407 114/411	48/43 227/379 185/299	109/22

a

Acknowledgements. I am grateful to Gilles Dowek, for his careful reading and comments.

This work is supported by the ANR-NSFC project LOCALI (NSFC 61161130530 and ANR 11 IS02 002 01) as P *