Mnacho Echenim
email: mnacho.echenim@imag.fr

Nicolas Peltier
email: nicolas.peltier@imag.fr

A Calculus for Generating Ground Explanations ⋆

We present a modification of the superposition calculus that is meant to generate explanations why a set of clauses is satisfiable. This process is related to abductive reasoning, and the explanations generated are clauses constructed over so-called abductive constants. We prove the correctness and completeness of the calculus in the presence of redundancy elimination rules, and develop a sufficient condition guaranteeing its termination; this sufficient condition is then used to prove that all possible explanations can be generated in finite time for several classes of clause sets, including many of interest to the SMT community. We propose a procedure that generates a set of explanations that should be useful to a human user and conclude by suggesting several extensions to this novel approach.

Introduction

The verification of complex systems is generally based on proving the validity, or, dually, the satisfiability of a logical formula. The standard practice consists in translating the behavior of the system to be verified into a logical formula, and proving that the negation of the formula is unsatisfiable. These formulas may be domain-specific, so that it is only necessary to test the satisfiability of the formula modulo some background theory, whence the name Satisfiability Modulo Theories problems, or SMT problems. If the formula is actually satisfiable, this means the system is not error-free, and any model can be viewed as a trace that generates an error. The models of a satisfiable formula can therefore help the designers of the system guess the origin of the errors and deduce how they can be corrected. Yet, this still requires some work. Indeed, there are generally many interpretations on different domains that satisfy the formula, and it is necessary to further analyze these models to understand where the error(s) may come from.

We present what is, to the best of our knowledge, a novel approach to this debugging problem: we argue that rather than studying one model of a formula, more valuable information can be extracted from the properties that hold in all the models of the formula. For instance, consider the theory of arrays, which is axiomatized as follows (as introduced by [START_REF] Mccarthy | Computer programs for checking mathematical proofs[END_REF]): ∀x, z, v. select(store(x, z, v), z) ≃ v,

(1) ∀x, z, w, v. z ≃ w ∨ select(store(x, z, v), w) ≃ select(x, w).

(

) 2
These axioms state that if element v is inserted into array x at position z, then the resulting array contains v at position z, and the same elements as in x elsewhere. Assume that to verify that the order in which elements are inserted into a given array does not matter, the satisfiability of the following formula is tested (see also Figure 1): select(store(store(a, i, b), j, c), k) ≃ select(store(store(a, j, c), i, b), k).

This formula asserts that there is a position k that holds different values in the array obtained from a by first inserting element b at position i and then element c at position j, and in the array obtained from a by first inserting element c at position j and then element b at position i. It turns out that this formula is actually satisfiable, which in this case means that some hypotheses are missing. State of the art SMT solvers such as Yices [16] can help find out what hypotheses are missing by outputting a model of the formula. In this case, Yices outputs (= b 1) (= c 3) (= i 2) (= k 2) (= j 2), and for this simple example, such a model may be sufficient to quickly understand where the error comes from. However, a simpler and more natural way to determine what hypotheses are missing would be to have a tool that, when fed the formula above, outputs i ≃ j ∧ b ≃ c, stating that the formula can only be true when elements b and c are distinct, and are inserted at the same position in a. This information permits to know immediately what additional hypotheses must be made for the formula to be unsatisfiable. In this example, there are two possible hypotheses that can be added: i ≃ j or b ≃ c.

In this paper, we investigate what information should be provided to the user and how it can be obtained, by distinguishing a set of constants on which additional hypotheses are allowed to be made. These constants are called abducible constants or simply abducibles, and the problem boils down to determining what ground clauses containing only abducibles are logically entailed by the formula under consideration, since the negation of any of these clauses can be viewed as a set of additional hypotheses that make the formula unsatisfiable.

Outline. This paper begins by summarizing all necessary background, and then a calculus specially designed for abductive reasoning is defined. This calculus is closely related to the superposition calculus SP, and we rely on completeness and termination results for SP to prove similar results for the new calculus. We also propose a method for generating clauses containing only abducible constants, that can help a user quickly detect where an error comes from, and decide what additional hypotheses should be added to fix the faulty formula.

Due to the space restrictions, several intermediate results and proofs are omitted. A full version of this work containing all proofs is available in [START_REF] Echenim | A calculus for generating ground explanations[END_REF].

Preliminaries

The general framework of this paper is first-order logic with equality. Most of the presentation in this section is standard, and we refer the reader to [START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF] for details. Given a finite signature Σ and an integer i ≥ 0, Σ i stands for the set of function symbols in Σ of arity i. In particular, Σ 0 denotes the set of constants in Σ. We assume the standard definitions of terms, predicates, literals and clauses, all of which are constructed over a set of variables X . Interpretations are defined as usual, |= stands for logical entailment and ≡ stands for logical equivalence. We also consider the standard definitions of positions in terms, predicates, literals or clauses. A term, predicate, literal or clause containing no variable is ground. As usual, clauses are assumed to be variable-disjoint. The symbol ≃ stands for unordered equality, ⊲⊳ is either ≃ or ≃. If L is a literal, then L c denotes the complementary literal of L, i.e., (t ≃ s) c def = (t ≃ s) and (t ≃ s) c def = (t ≃ s). A literal is flat if it only contains constants or variables1 , and a clause is flat if it only contains flat literals. The letters l, r, s, u, v and t denote terms, w, x, y, z variables, and all other lower-case letters denote constants or function symbols. Definition 1. Given a ground clause C, we denote by ¬C the following set of literals:

¬C def = {L c | L ∈ C}.
A substitution is a function mapping variables to terms. Given a substitution σ, the set of variables x such that xσ = x is called the domain of σ and denoted by dom(σ). If σ is a substitution and V is a set of variables, then σ |V is the substitution with domain dom(σ) ∩ V , that matches σ on this domain. As usual, a substitution can be extended into a homomorphism on terms, atoms, literals and clauses. The image of an expression E by a substitution σ will be denoted by Eσ. If E is a set of expressions, then Eσ denotes the set {Eσ | E ∈ E}. The composition of two substitutions σ and θ is denoted by σθ. A substitution σ is more general than θ if there exists a substitution η such that θ = ση. The substitution σ is a renaming if it is injective and ∀x ∈ dom(σ), xσ ∈ X ; and it is a unifier of two terms t, s if tσ = sσ. Any unifiable pair of terms (t, s) has a most general unifier, unique up to a renaming, and denoted by mgu(t, s). A substitution σ is ground if xσ is ground, for every variable x in its domain.

Superposition C ∨ l[u ′ ] ≃ r D ∨ u ≃ t (C ∨ D ∨ l[t] ≃ r)σ (i), (ii), (iii), (iv) Paramodulation C ∨ l[u ′ ] ≃ r D ∨ u ≃ t (C ∨ D ∨ l[t] ≃ r)σ (i), (ii), (iii), (iv) Reflection C ∨ u ′ ≃ u Cσ (v) Equational Factoring C ∨ u ≃ t ∨ u ′ ≃ t ′ (C ∨ t ≃ t ′ ∨ u ≃ t ′ )σ (i), (vi)
where the notation l[u ′ ] means that u ′ appears as a subterm in l, σ is the most general unifier (mgu) of u and u ′ , u ′ is not a variable in Superposition and Paramodulation, and the following abbreviations hold: A simplification ordering ≺ is an ordering that is stable under substitutions, monotonic, and contains the subterm ordering: if s ≺ t, then c[s]σ ≺ c[t]σ for any context c and substitution σ, and if s is a strict subterm of t then s ≺ t. A complete simplification ordering, or CSO, is a simplification ordering that is total on ground terms. Similarly to [START_REF] Bonacina | Theory decision by decomposition[END_REF], in the sequel, we shall assume that any CSO under consideration is good : Definition 2. A CSO ≺ is good if for all ground compound terms t and constants c, we have c ≺ t.

(i): uσ ≺ tσ; (ii): ∀L ∈ D : (u ≃ t)σ ≺ Lσ; (iii): l[u ′ ]σ ≺ rσ; (iv): ∀L ∈ C : (l[u ′ ] ⊲⊳ r)σ ≺ Lσ; (v): ∀L ∈ C : (u ′ ≃ u)σ ≺ Lσ; (vi): ∀L ∈ {u ′ ≃ t ′ } ∪ C : (u ≃ t)σ ≺ Lσ.
The superposition calculus, or SP (see, e.g., [START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF]), is a refutationally complete rewrite-based inference system for first-order logic with equality. It consists of the inference rules summarized in Fig. 2: each rule contains premises which are above the inference line, and generates a conclusion, which is below the inference line. If a clause D is generated from premises C, C ′ , then we write C, C ′ ⊢ D. The superposition calculus is based on a CSO on terms, which is extended to literals and clauses in a standard way (see, e.g., [START_REF] Baader | Term Rewriting and All That[END_REF]), and we may write SP ≺ and ⊢ ≺ to specify the ordering. A ground clause C is ≺-redundant in S, or simply redundant, if there exists a set of ground clauses S ′ such that S ′ |= C, and for every D ∈ S ′ , D is an instance of a clause in S and D ≺ C. A non-ground clause C is ≺-redundant in S if all its instances are ≺-redundant in S. In particular, every strictly subsumed clause and every tautological clause is redundant. A set of clauses S is saturated if every clause C / ∈ S generated from premises in S is redundant in S. A saturated set of clauses that does not contain is satisfiable [START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF]. In practice, it is necessary to use a decidable approximation of this notion of redundancy: for example, a clause is redundant if it can be reduced by some demodulation steps to either a tautology or to a subsumed clause.

In the sequel, it will be necessary to forbid the occurrence of clauses containing maximal literals of the form x ≃ t, where x t: Definition 3. A clause is variable-eligible w.r.t. ≺ if it contains a maximal literal of the form x ≃ t, where x t. A set of clauses is variable-inactive (see [START_REF] Armando | New results on rewritebased satisfiability procedures[END_REF]) if no non-redundant clause generated from S is variable-eligible.

For technical reasons we have chosen to present a slightly relaxed version of the superposition calculus, in which the standard strict maximality conditions have been replaced by non-strict maximality conditions. For instance in Condition (i), uσ tσ is replaced by uσ ≺ tσ: it is not forbidden for u and t to be identical in Paramodulation and Superposition inferences. It is clear that the clauses generated in the case where there is an equality actually turn out to be redundant.

A calculus for handling abducible constants

As explained in the Introduction, the aim of this paper is to start with a formula F and a set of axioms A, and generate a formula H which logically entails F modulo A, i.e., such that H, A |= F (where H ∧ A is satisfiable). As usual in abductive reasoning (see for instance [START_REF] Eiter | The complexity of logic-based abduction[END_REF]), we actually consider the contrapositive: since H, A |= F is equivalent to ¬F, A |= ¬H, the original problem can be solved by generating logical consequences of the formula ¬F ∧ A. For the sake of simplicity, the formula ¬F is added to the axioms which are assumed to be in clausal form, and we have the following definition:

Definition 4. A clause C is an implicate of a set of clauses S iff S |= C.
It is clear that after its generation, it is necessary to verify that H is satisfiable modulo A. For instance, if a is some constant, then an explanation such as a ≃ 0 ∧ a ≃ 1 or even 0 ≃ 1 does not provide any information since it contradicts the axioms of Presburger arithmetic. Testing this satisfiability can be done using standard decision procedures. There are many possible candidate sets of implicates, which may be more or less informative. For instance, it is possible to take C ∈ S, but this is obviously of no use. Thus it is necessary to provide additional information in order to restrict the class of formulas that are searched for. In (propositional) abductive reasoning, this is usually done by considering clauses built on a given set of literals: the abducible literals. A more natural possibility in the context of this paper is to consider clauses built on a given set of ground terms. We may assume with no loss of generality that each of these terms is replaced by a constant symbol, by applying the usual flattening operation, see, e.g., [START_REF] Armando | A rewriting approach to satisfiability procedures[END_REF][START_REF] Bonacina | Theory decision by decomposition[END_REF]. For example, the term select(store(a, i, b), j) may be replaced by a new constant d, along with the axioms:

d ≃ select(d ′ , j) ∧ d ′ ≃ store(a, i, b)).
We thus consider a distinguished set of constants A ⊆ Σ 0 , called the set of abducible constants, and restrict ourselves to explanations that are conjunctions of literals built upon abducible constants. This is formalized with the following definition of an A-implicate:

Definition 5. Let S be a set of clauses. A clause C is an A-implicate of S iff every term occurring in C is also in A and S |= C.
As in propositional abductive reasoning, the set A must be provided by the user. Given a set of clauses S containing both the axioms A and the clauses corresponding to the conjunctive normal form of ¬F , we investigate how to generate the set of flat ground clauses C built on A, that are logical consequences of S. Since SP is only refutationally complete, this cannot be done directly using this calculus (except in some very particular cases, see for instance [START_REF] Tran | Combination of convex theories: Modularity, deduction completeness, and explanation[END_REF]). For example, it is clear that f (a) ≃ f (b) |= a ≃ b, but a ≃ b cannot be generated from the antecedent clause. In principle, it is possible to enumerate all possible clauses C built on A and then use the superposition calculus to check whether S ∪¬C is unsatisfiable, however, this yields a very inefficient procedure. An alternate method consists in replacing the superposition calculus by a less restrictive calculus, such as the Resolution calculus [START_REF] Leitsch | The resolution calculus[END_REF] together with the equality axioms. For instance in the previous case, the clause f (a) ≃ f (b) and the substitutivity axiom x ≃ y ∨ f (x) ≃ f (y) permit to generate by the Resolution rule: a ≃ b. However, again, this calculus is not efficient, and in particular all the termination properties of the superposition calculus on many interesting subclasses of first-order logic [4, 2, 1] are lost In this section, we provide a variant of the superposition calculus which is able to directly generate, from a set of clauses S, a set of logical consequences of S that are built on a given set of constant symbols A. The calculus is thus parameterized both by the term ordering ≺ and by the set of abducible constants A. We shall show that the calculus is complete, in the sense that if S |= C and if C is an A-implicate of S, then C is a logical consequence of other clauses built on A that are generated from S. We will also prove that the calculus terminates on many classes of interest in the SMT community.

We will thus consider clauses of a particular form and a slight variation of the superposition calculus in order to be able to reason on abducible constants. The principle behind this calculus is similar to that of [START_REF] Bachmair | Refutational theorem proving for hierachic first-order theories[END_REF] for the combination of hierarchic theories, with the difference that in this framework, abducible constants can potentially interact with other terms, whereas in the framework of [START_REF] Bachmair | Refutational theorem proving for hierachic first-order theories[END_REF], such an interaction is prevented by sortedness. In both settings however, a same abstraction principle is used to delay the reasoning on the objects of interest (in this case, the abducible constants).

From now on we assume that the set of variables X is of the form X = V ⊎V A . The elements in V are ordinary variables and the elements in V A are called abducible variables, and they will serve as placeholders for abducible constants in terms and clauses. In the sequel, when we mention standard terms, literals or clauses, we assume that all the variables they contain are in V. Definition 6. An A-literal is a literal of the form t ⊲⊳ s, where t, s ∈ V A ∪ A. A first step towards reasoning on abducible constants will consist in extracting them from the terms in which they occur, and replacing them by abducible variables. Then, to ensure that such a property is preserved by inferences, every substitution mapping an abducible variable to anything other than an abducible variable will be discarded. More formally: Definition 7. A term is abstracted if it contains no abducible constant. A literal t ⊲⊳ s is abstracted if t and s are both abstracted. A clause is abstracted if all non-abstracted literals in C are A-literals.

If t is an abstracted term, then not every instance of t is also abstracted. We define a condition on substitutions that guarantees such a stability result. Definition 8. A substitution σ is A-compliant if for all x ∈ dom(σ), xσ is abstracted, and for all x ∈ dom(σ) ∩ V A , xσ ∈ V A . Two abstracted terms are A-unifiable if they are unifiable and admit an A-compliant mgu.

In the sequel, every time abstracted terms are A-unifiable, we will assume the corresponding mgu is A-compliant. Definition 9. Let < A be a total ordering on A and a 0 denote the smallest abducible in A. Given a term t, we denote by t ↓A the term obtained by replacing every abducible constant occurring in t by a 0 . The term t is A-reduced if t ↓A = t. The previous notation and this definition extend to literals, clauses and sets of clauses. It is clear that if all abducible constants are replaced by abducible variables in a standard clause, then the resulting abstracted clause is not equivalent to the former one. However, equivalence can be regained by adding so-called V Aconstraint literals to the resulting abstracted clause. Definition 10. A V A -constraint literal is a literal of the form x ≃ a, where x ∈ V A and a ∈ A. For all clauses C, we denote by

Γ (C) the disjunction of V A - constraint literals in C. A V A -constraint clause is a disjunction of V A -constraint literals. Given a V A -constraint clause A = k i=1
x i ≃ a i , the substitution associated to A is denoted by ν A and defined as follows: dom(ν A ) = {x 1 , . . . , x k }, and for all x ∈ dom(ν A ),

xν A = min < A {a i | x i = x}.
For readability, if B is a clause then we will write ν B instead of ν Γ (B) . If S is a set of abstracted clauses, then S ν is the set

S ν = {Cν C | C ∈ S}.
A = x ≃ a ∨ x ≃ c ∨ y ≃ b ∨ z ≃ a ∨ y ≃ c. Then νA = {x → a, y → b, z → a}.
Note that by definition, C ≡ Cν C and S ≡ S ν . As mentioned earlier, abducible variables are meant to be placeholders for abducible constants. In general, it will be necessary to keep some information permitting to know what abducible constants an abducible variable could be replaced by. Such a requirement is satisfied by imposing that every abducible variable occurs in at least one V A -constraint literal, which intuitively specifies its value.

Definition 11. A clause C is V A -stable if Var A (C) ⊆ Var A (Γ (C)). A set of clauses is V A -stable if every clause it contains is V A -stable.
Given a set of standard clauses, it is easy to construct an equivalent set of abstracted and V A -stable clauses. It suffices to replace every abducible a occurring in a non-A-literal by a fresh variable x ∈ V A , and to add the literal x ≃ a to the clause. For instance, if

A = {a, b} then the clause a ≃ b ∨ a ≃ c ∨ f (b, d, x) ≃ g(b, y) is replaced by x 1 ≃ a ∨ x 2 ≃ b ∨ x 3 ≃ b ∨ a ≃ b ∨ x 1 ≃ c ∨ f (x 2 , d, x) ≃ g(x 3 , y).
Definition of the calculus. We introduce a calculus for generating Aimplicates. It is a modified version of the superposition calculus, and consists of inference rules that are meant to be applied to abstracted clauses. In particular, it is based on orderings that are suitable for abstracted terms, literals and clauses: the order between two terms t and s should not depend on the abducible constants occurring in t and s, and maximal terms and literals in abstracted clauses should be related to maximal terms and literals in standard clauses, in a sense that will be made precise later. We thus define particular orderings for standard clauses, from which we define suitable orderings for abstracted clauses. Definition 12. We consider a good CSO ≺ such that2 :

1. for all a, b ∈ A, a ≺ b if and only if a < A b; 2. for all a ∈ A and for all non-variable terms t ∈ A, a ≺ t; 3. for all ground terms t, s not in A, if t ≺ s then t ↓A s ↓A , and if t ↓A ≺ s ↓A then t ≺ s.

We let γ 0 denote the ground substitution of domain V A such that for all x ∈ V A , xγ 0 = a 0 . Given abstracted terms t, s, we define ≺ A as follows: t ≺ A s iff tγ 0 ≺ sγ 0 . This definition extends to literals and clauses in a standard way. A term is A-maximal if it is maximal for ≺ A ; this definition also extends to literals and clauses.

Definition 13. We denote by SP A the calculus such that for all clause sets S, we have S ⊢ A D if S ⊢ ≺ A D and the mgu involved in the SP-inference is A-compliant.

By construction, SP and SP A coincide on ground A-clauses. We define a particular notion of redundancy for abstracted clauses, that is related to redundancy for standard clauses. The main difference with the standard definition is that the redundancy test is performed modulo the substitution ν C that replaces the abstracted variables in C by the abducible constants they denote.

Definition 14. Consider a set of abstracted clauses S and an abstracted clause

C such that Var(C) ⊆ V A . The clause C is A-redundant in S if:
-C is an A-clause, ν C = id and Cν C either occurs or is A-redundant in S, -or there exists a set of ground clauses S ′ such that S ′ |= C, every D ∈ S ′ is an instance of a clause in S ν and D ≺ Cν C .

If C is an abstracted clause such that Var(C) ⊆ V A , then C is A-redundant in S if for all ground substitutions σ with a domain in V, Cσ is A-redundant in S.

The set S is A-saturated if every clause C / ∈ S generated by an SP A -inference with premises in S is A-redundant in S.

This notion of redundancy permits to add the standard contraction rules of the superposition calculus to SP A (subsumption, simplification, elimination of tautologies, etc). The following contraction inference rule is also added to SP A :

A-reduction : C Cν C if C is an A-clause and ν C = id.
After any application of the A-reduction rule, the premise becomes A-redundant and can be deleted.

Theorem 1. If S is a variable-inactive (w.r.t. ≺ A ) set of abstracted clauses that are V A -stable, then every non-redundant clause generated from S by SP A is abstracted and V A -stable. Also, if one of the premises of a binary SP A -inference is an A-clause, then the other premise is also an A-clause.

The variable-inactive condition, which ensures that all generated clauses are variable-eligible, prevents non-abstracted clauses from being generated from abstracted ones. For example, if S contains the unit clauses {a ≃ b, x ≃ y} with {a, b} ∈ A and {x, y} ∈ V, then S ⊢ A y ≃ b, and the latter is not abstracted. In what follows, we will prove completeness and termination results for SP A . The completeness result guarantees that SP A generates the required information about existing abducibles for any abstracted set of clauses, while the termination result relies on termination results for SP, and will be used to verify without any additional effort that our technique can be used as a decision procedure for reasoning about abducibles in SMT problems with several theories of interest.

Completeness of the calculus

This section is devoted to showing that if S is an unsatisfiable set of abstracted clauses that is A-saturated, then ∈ S (due to space restrictions, we only provide a sketch of the proof, see [START_REF] Echenim | A calculus for generating ground explanations[END_REF] for details). Note that this result does not follow from the refutational completeness of the superposition calculus: indeed, the ordering ≺ A is not a simplification ordering (it is not stable by substitution), and all inferences in which non-A-compliant unifiers are involved are ignored. However, the proof is based on the refutational completeness of SP, and requires determining relationships between SP-inferences and SP A -inferences.

Let S be a V A -stable and A-saturated set of clauses, with no variable-eligible clause. We will show that S is satisfiable by constructing a set of standard clauses whose satisfiability will entail that of S. The set we construct will be saturated under SP ≺ -inferences, and it will not contain the empty clause; we will conclude that it must be satisfiable, and hence that so must S.

Let T be the set of A-clauses in S. Since S is V A -stable and A-saturated by hypothesis, T can only contain ground A-clauses, because if a non-ground clause occurs in T then A-reduction applies. Since SP and SP A coincide on ground A-clauses, T must also be saturated under SP ≺ -inferences and cannot contain ; this set is therefore satisfiable. We consider a fixed interpretation I that is a model of T . Definition 15. We define the ground set

U I = a ≃ b | a, b ∈ A, a I = b I ∪ a ≃ b | a, b ∈ A, a I = b I .
We inductively define the notion of an I-reduction:

-For all a ∈ A,

a I = min ≺ b ∈ A | b I = a I . -f (t 1 , . . . , t n ) I = f (t 1 I , . . . , t n I ).
This definition extends to standard literals and clauses.

The I-reduction procedure is used to define a set whose satisfiability entails that of S, and that turns out to be saturated:

Definition 16. Let S I = U I ∪ ∆(C I ) | C ∈ S ν ∧ U I |= ¬∆(C) .
Proposition 1. If S I is satisfiable then so is S ν , and therefore so is S. Lemma 1. S I is saturated for SP ≺ .

Since S I is saturated for the standard superposition calculus SP ≺ and contains no occurrence of the empty clause, we deduce that it is satisfiable. Theorem 2. Let S be a set of abstracted clauses that is V A -stable and contains no variable-eligible clause. If S is A-saturated and does not contain the empty clause, then S is satisfiable.

This theorem proves the refutational completeness of SP A together with contraction rules that eliminate A-redundant clauses, for those sets of abstracted clauses S whose saturation is guaranteed to meet the requirements of the theorem. The first two requirements are not restrictive: the abstraction of a set of standard clauses described right before Section 3 produces a set of abstracted and V A -stable clauses, and the saturation of this set is guaranteed to only contain abstracted and V A -stable clauses by Theorem 1. The fact that S contains no variable-eligible clause cannot be imposed that easily, but such a condition is guaranteed if S is variable-inactive, which is the case for many classes of clause sets of interest [START_REF] Armando | A rewriting approach to satisfiability procedures[END_REF][START_REF] Armando | New results on rewritebased satisfiability procedures[END_REF].

Note that this completeness result is not -by itself -sufficient for our purpose, since our goal is not merely to test the satisfiability of clause sets but rather to generate flat consequences they logically entail. The next section shows how the calculus SP A can be employed to reach this goal.

We return to the problem of explaining why a set of clauses is satisfiable, and show how SP A can be used to generate explanations relating abducibles to one another. Given a satisfiable set of clauses S ′ , we denote by I A (S ′ ) the set of all A-implicates of S ′ : I

A (S ′ ) def = {C an A-clause | C is ground and S ′ |= C} .
It is clear that all the information about abducible constants that is entailed by S ′ is contained in I A ( ′ S). However this set can be very large and it contains a lot of non-pertinent information, for example all logical tautologies, or all instances of the equality axioms. It therefore does not seem reasonable to return this entire set to a user. Another solution could be to return a subset T ⊆ I A (S ′ ) such that T ⊢ I A (S ′ ), but again, such a set might be large and contain unnecessary information. The solution we choose is to return a minimal subset T ′ ⊆ I A (S ′ ) satisfying the following property: for all C ∈ I A (S ′ ) that is not a tautology, there exists a clause C ′ ∈ T ′ such that C ′ |= C. The clauses in T ′ are the prime implicates of S ′ . The notion of prime implicates plays a central rôle in many applications of computer science and artificial intelligence, and several approaches have been proposed for computing the prime implicates of a given propositional formula (see, e.g., [START_REF] Jackson | Computing prime implicates[END_REF]). Some extensions to first-order logic have also been considered, such as, e.g., [START_REF] Marquis | Extending abduction from propositional to first-order logic[END_REF]. In what follows, we define an algorithm that computes prime implicates for sets of flat equational clauses.

It turns out that SP A cannot be used to determine the set T ′ . For instance, if S ′ = {a ≃ b, c ≃ d}, then the clause a ≃ c ∨ b ≃ d must be in I A (S ′ ). Since it is subsumed by no clause in I A (S ′ ) but itself, it must also be in T ′ , but no SP A -inference rule (or SP-inference rule for that matter) can be applied to S ′ to generate such a clause. In the sequel, we will show how, starting with a set of A-clauses that logically entails I A (S ′ ), it is possible to generate a set T ′ using the Resolution calculus, denoted by R (we refer the reader to [START_REF] Leitsch | The resolution calculus[END_REF] for details on the Resolution calculus). From now on, S ′ denotes a satisfiable set of standard clauses, and S is a set of abstracted clauses such that S ν = S ′ . Thus, S and S ′ are equivalent. The first step towards this construction is the definition of a set of A-clauses that logically entails I A (S ′ ). The (finite) set of all A-clauses in the saturated set generated from S using SP A will satisfy this requirement.

Definition 17. We denote by T ∞ the set of A-clauses in the A-saturated set generated from S by SP A .

The key result that makes the generation of A-implicates possible is that all the A-clauses that are entailed by S are actually logical consequences of T ∞ :

Proposition 2. T ∞ |= I A (S ′ ).
Let Eq be the set of axioms stating that ≃ is an equivalence relation3 : Eq = {x ≃ x, x ≃ y ∨ y ≃ x, x ≃ y ∨ y ≃ z ∨ x ≃ z}, and let Eq A be the set consisting of all instantiations of the axioms in Eq by the elements in A. The result we show is that the R-closure of the set T ∞ ∪ Eq A satisfies the requirements for the set of A-clauses that is searched for.

Theorem 3. Let T = T ∞ ∪ Eq A , and let C be a non-tautological ground clause in I A (S). Then there is a derivation from T of a clause C ′ such that C ′ |= C.

To summarize, given a set of clauses S ′ that is satisfiable and a set of abducible constants A, the simple algorithm in pseudo-code described in Figure 3 returns a set of clauses constructed over A that can be viewed as explanations why S ′ is satisfiable. Note that R-saturation can be performed on the fly: it is clear that it is not necessary to wait until SP A -saturation(S) is computed to start generating the clauses in R-saturation(T ∞ ∪ Eq A ). Thus even in case of non-termination, all the prime implicates can eventually be generated. After the set R-saturation(T ∞ ∪ Eq A ) is computed, it is possible to remove from this set all the clauses that can be inferred from other prime implicates. This solution yields a more compact representation. However, this is possible only in case of termination, since the deleted clauses may be involved in the generation of other prime implicates. A termination result for SP A will be presented in the following section. By putting all the previous results together, we obtain the following theorem, stating the soundness and completeness of the procedure Explain.

1 select(store(x, z, v), z) ≃ v 4 d2 ≃ store(d1, j, c) 2 z ≃ w ∨ select(store(x, z, v), w) ≃ select(x, w) 5 d3 ≃ store(a, j, c) 3 d1 ≃ store(a, i, b) 6 d4 ≃ store(d3, i, b) 7 select(d2, k) ≃ select(d4, k)
Assume that A = {i, j, b, c}. Then Clauses 3, 4, 5, 6 are abstracted as follows:

3 ′ x ′ ≃ i ∨ y ′ ≃ b ∨ d1 ≃ store(a, x ′ , y ′ ) 4 ′ x ′′ ≃ j ∨ y ′′ ≃ c ∨ d2 ≃ store(d1, x ′′ , y ′′ ) 5 ′ x ′′ ≃ j ∨ y ′′ ≃ c ∨ d3 ≃ store(a, x ′′ , y ′′ ) 6 ′ x ′ ≃ i ∨ y ′ ≃ b ∨ d4 ≃ store(d3, x ′ , y ′ )
SPA generates the following clauses4 :

x ′ ≃ i ∨ w ≃ x ′ ∨ select(d1, w) ≃ select(a, w) (3 ′ ,2) 9 x ′′ ≃ j ∨ w ≃ x ′′ ∨ select(d2, w) ≃ select(d1, w) (4 ′ ,2) 10 x ′′ ≃ j ∨ w ≃ x ′′ ∨ select(d3, w) ≃ select(a, w) (5 ′ ,2) 11 x ′ ≃ i ∨ w ≃ x ′ ∨ select(d4, w) ≃ select(d3, w) (6 ′ ,2) 12 x ′ ≃ i ∨ y ′ ≃ b ∨ select(d1, x ′ ) ≃ y ′ (3 ′ ,1) 13
x ′′ ≃ j ∨ y ′′ ≃ c ∨ select(d2, x ′′ ) ≃ y ′′ (4 ′ ,1) 14

x ′′ ≃ j ∨ y ′′ ≃ c ∨ select(d3, x ′′ ) ≃ y ′′ (5 ′ ,1) 16

x

′ ≃ i ∨ y ′ ≃ b ∨ select(d4, x ′ ) ≃ y ′ (6 ′ ,1) 17 x ′ ≃ i ∨ k ≃ x ′ ∨ select(d2, k) ≃ select(d3, k) (11, 7) 18 x ′ ≃ i ∨ k ≃ x ′ ∨ x ′′ ≃ j ∨ k ≃ x ′′ ∨ select(d2, k) ≃ select(a, k) (10, 17) 19 x ′ ≃ i ∨ k ≃ x ′ ∨ x ′′ ≃ j ∨ k ≃ x ′′ ∨ select(d1, k) ≃ select(a, k) (9, 18) 20 x ′ ≃ i ∨ x ′′ ≃ j ∨ k ≃ x ′ ∨ k ≃ x ′′ (8,19) 21 x ′ ≃ i ∨ x ′′ ≃ j ∨ k ≃ x ′ ∨ select(d2, k) ≃ select(d4, x ′′ ) (20,7) 22 x ′ ≃ i ∨ x ′′ ≃ j ∨ k ≃ x ′ ∨ x ′′ ≃ x ′ ∨ select(d2, k) ≃ select(d3, x ′′ ) (11,21) 23 x ′ ≃ i ∨ x ′′ ≃ j ∨ y ′′ ≃ c ∨ k ≃ x ′ ∨ x ′′ ≃ x ′ ∨ select(d2, k) ≃ y ′′ (14,22) 24 x ′ ≃ i ∨ x ′′ ≃ j ∨ y ′′ ≃ c ∨ k ≃ x ′ ∨ x ′′ ≃ x ′ ∨ select(d2, x ′′ ) ≃ y ′′ (20,23) 25 x ′ ≃ i ∨ x ′′ ≃ j ∨ k ≃ x ′ ∨ x ′′ ≃ x ′ (13,24) 26 x ′ ≃ i ∨ x ′′ ≃ j ∨ x ′′ ≃ x ′ ∨ select(d2, k) ≃ select(d4, x ′ ) (25,7) 27 x ′ ≃ i ∨ x ′′ ≃ j ∨ y ′ ≃ b ∨ x ′′ ≃ x ′ ∨ select(d2, k) ≃ y ′ (16,26) 28 x ′ ≃ i ∨ x ′′ ≃ j ∨ y ′ ≃ b ∨ x ′′ ≃ x ′ ∨ select(d2, x ′ ) ≃ y ′ (25,27) 29 x ′ ≃ i ∨ x ′′ ≃ j ∨ y ′ ≃ b ∨ x ′′ ≃ x ′ ∨ select(d1, x ′ ) ≃ y ′ (9,28) 30 i ≃ j (12,29) 31 x ′ ≃ i ∨ x ′′ ≃ j ∨ x ′ ≃ x ′′ ∨ k ≃ x ′ (20) 33 x ′ ≃ i ∨ x ′′ ≃ j ∨ x ′ ≃ x ′′ ∨ select(d2, k) ≃ select(d4, x ′ ) (31,7) 34 x ′ ≃ i ∨ x ′′ ≃ j ∨ x ′ ≃ x ′′ ∨ y ′ ≃ b ∨ select(d2, k) ≃ y ′ (16,34) 35 x ′ ≃ i ∨ x ′′ ≃ j ∨ x ′ ≃ x ′′ ∨ y ′ ≃ b ∨ select(d2, x ′ ) ≃ y ′ (31,34) 36 i ≃ j ∨ b ≃ c (13,35)
By Resolution, from 30 and 36, we get c ≃ b, which subsumes 36. We obtain the A-implicates {i ≃ j, b ≃ c}, yielding the explanation i ≃ j ∨ b ≃ c.

A termination result for SP A

We now prove a result that relates the termination of SP on a set of standard clauses S to the termination of SP A on an abstracted version of S. This shows that many existing results about the termination of the superposition calculus for subclasses of first-order logic carry over to SP A . We relate standard and abstracted terms by defining a so-called relation of A-relaxation. This relation will be used afterwards to relate the forms of the clauses generated by SPinferences and those generated by SP A -inferences in a more precise manner.

Definition 18. The relation of A-relaxation relates an abstracted term t to a standard one t ′ and is defined as follows: t A t ′ if and only if tγ 0 = t ′ ↓A . Given an abstracted clause C and a standard clause C ′ , we write

C A C ′ if and only if ∆(Cγ 0 ) = ∆(C ′ ↓A )
. This relation is extended to sets of clauses in a straightforward manner.

4. Assume A = {a, b}, let C = x ≃ a ∨ a ≃ b ∨ f (x, x, d) ≃ g(y) ∨ g(y) ≃ d and C ′ = a ≃ b ∨ f (a, b, d) ≃ g(b) ∨ g(a) ≃ d. Then C A C ′ .
We define a notion of redundancy that is meant to hold no matter what abducible constants occur in the clause under consideration. Definition 19. An A-reduced clause C ′ is p-redundant in an A-reduced set of clauses S ′ if for all sets of abstracted clauses S such that (S ν ) ↓A ≡ S ′ and for every abstracted clause D such that (Dν D ) ↓A ≡ C ′ , clause D is A-redundant in S. An A-reduced set of clauses S ′ is p-saturated if every clause generated with premises in S ′ either occurs in S ′ or is p-redundant in S ′ . This notion permits to eliminate clauses that are redundant in the usual sense and do not contain any abducible constant. Notice, however, that p-redundant clauses can possibly contain abducible constants. For example if A = {a, b} and

S ′ = {f (c) ≃ f (d)}, then C ′ = g(a, c) ≃ h(a) ∨ f (c) ≃ f (d) is p-redundant in S ′ .
Theorem 5. Let S ′ be a set of A-reduced clauses, and let T be the p-saturated set of clauses generated from S ′ . If T is finite and S is a set of abstracted clauses that is V A -stable, variable-inactive and such that S A S ′ , then the set of nonredundant clauses generated from S is finite.

Theorem 5 guarantees that SP A (and thus Explain) terminates on several classes of clause sets, in particular for clause sets related to SMT problems. The authors of [START_REF] Armando | A rewriting approach to satisfiability procedures[END_REF] and [START_REF] Armando | New results on rewritebased satisfiability procedures[END_REF] prove that sets of the form T ∪ U , where T is a theory and U a set of ground unit clauses, generate finite saturated sets. This result is extended to clause sets of the form T ∪ U ′ , where U ′ is an arbitrary set of ground clauses, in [START_REF] Bonacina | On variable-inactivity and polynomial Tsatisfiability procedures[END_REF]. An inspection of the finiteness results of [START_REF] Armando | A rewriting approach to satisfiability procedures[END_REF][START_REF] Armando | New results on rewritebased satisfiability procedures[END_REF][START_REF] Bonacina | On variable-inactivity and polynomial Tsatisfiability procedures[END_REF] shows that they hold not only for saturated sets but also for p-saturated sets, since the redundant clauses that are deleted are actually p-redundant: they do not contain any constant at all. Thus, SP A terminates for clause sets of the form T ∪ U ′ , where U ′ is the abstraction of a set of ground clauses, and T is the axiomatization of any of the following theories: records, integer offsets, possibly empty lists, arrays...

Discussion

We have presented a calculus that permits to reason on the relations involving abducible constants, that are logical consequences of a satisfiable set of clauses. These relations can be viewed as explanations of why the set is satisfiable, since any of their negations, when added to the original clause set, renders the latter unsatisfiable. We proved a completeness result for the calculus, along with a sufficient condition guaranteeing its termination on classes of clause sets, among which SMT problems in several theories of interest. To the best of our knowledge, this approach is novel and there are many interesting directions to explore. One first direction is to investigate what set of clauses can be considered as a good set of explanations, and determine what a good trade-off might be between a small set of explanations that may hide too many details, and a large set of explanations that may carry too much unnecessary information. Another line of work that is currently under investigation is the search for a more efficient way to generate explanations. Indeed, the saturation with the Resolution calculus in the presence of the equality axioms is not entirely satisfactory as far as efficiency is concerned, and it would be interesting to see how the calculus SP A can be enhanced to directly produce the required set of explanations. As far as other extensions are concerned, we plan to investigate how to extend these results to abducible terms and not only abducible constants, by allowing the occurrence of function symbols in A. This would allow the derivation of non-ground explanations. Another possibility is to consider mixed literals, containing both abducible and non-abducible symbols. It would then be possible to generate explanations of the form a ≃ 0 without having to declare 0 as an abducible constant. We also plan on devising a calculus capable of efficiently generating explanations with abducibles interpreted in a particular theory, such as, e.g., arithmetic.

Fig. 1 .

 1 Fig. 1. Insertion into array a of element b at position i and element c at position j.

Fig. 2 .

 2 Fig. 2. Inference rules of SP: the clause below the inference line is added to the clause set containing the clauses above the inference line.

  An A-clause is a disjunction of A-literals. Given a clause C, we denote by ∆(C) the disjunction of A-literals in C and by ∆(C) the disjunction of non-A-literals in C. We define Var A (C) def = Var(C) ∩ V A .

Example 1 .

 1 Let C = f (b, c) ≃ g(d) ∨ x ≃ b ∨ f (a, b) ≃ f (c, d), where A = {a, b, c} and a ≺ b ≺ c. Then C ↓A = f (a, a) ≃ g(d) ∨ x ≃ a ∨ f (a, a) ≃ f (a, d), and this clause is an A-reduced clause.

Example 2 .

 2 Assume A = {a, b, c}, where a <A b <A c, and let

Fig. 3 .

 3 Fig. 3. Generation of a set of explanations

Theorem 4 .

 4 Let S be a set of clauses. Every clause C ∈ Explain(S ′ , A) is an A-implicate of S, and for every A-implicate C of S that is not a tautology, there exists a clause C ′ ∈ Explain(S ′ , A) such that C ′ |= C.

Example 3 .

 3 We return to the problem mentioned in the Introduction. After flattening, we get the following set of clauses:

Example

Note that we depart from the terminology in[START_REF] Armando | A rewriting approach to satisfiability procedures[END_REF][START_REF] Armando | New results on rewritebased satisfiability procedures[END_REF], where flat positive literals can contain a term of depth 1.

It is not difficult to see that there exist orderings fulfilling these properties (see[START_REF] Echenim | A calculus for generating ground explanations[END_REF]).

There will be no need to consider the congruence axiom, since all the clauses in T∞ only contain constants.

For readability we simply drop irrelevant disequations, i.e. x ≃ a ∨ C is replaced byC if x does not occur in C and x ≃ a ∨ x ′ ≃ a ∨ C is replaced by x ≃ a ∨ C{x ′ → x}.

⋆ This work has been partly funded by the project ASAP of the French Agence Nationale de la Recherche (ANR-09-BLAN-0407-01).


Sabine Ploux
email: sploux@isc.cnrs.fr

Armelle Boussidan
email: armelle.boussidan@isc.cnrs.fr

Hyungsuk Ji
email: jihyungsuk@skku.edu

The Semantic Atlas: an Interactive Model of Lexical Representation

In this paper we describe two geometrical models of meaning representation, the Semantic Atlas (SA) and the Automatic Contexonym Organizing Model (ACOM). The SA provides maps of meaning generated through correspondence factor analysis. The models can handle different types of word relations: synonymy in the SA and co-occurrence in ACOM. Their originality relies on an artifact called 'cliques' -a fine grained infra linguistic sub-unit of meaning. The SA is composed of several dictionaries and thesauri enhanced with a process of symmetrisation. It is currently available for French and English in monolingual versions as well as in a bilingual translation version. Other languages are under development and testing. ACOM deals with unannotated corpora. The models are used by research teams worldwide that investigate synonymy, translation processes, genre comparison, psycholinguistics and polysemy modeling. Both models can be consulted online via a flexible interface allowing for interactive navigation on http://dico.isc.cnrs.fr. This site is the most consulted address of the French National Center for Scientific Research's domain (CNRS), one of the major research bodies in France. The international interest it has triggered led us to initiate the process of going open source. In the meantime, all our databases are freely available on request.

The model

The originality of the model relies on the concept of 'cliques' [START_REF] Ploux | Modélisation et traitement informatique de la synonymie[END_REF]. Conceptually, a clique is a minimal unit of meaning, at a very fine grained level. In the SA cliques are lists of words which are related to each other by synonymy (in the broad sense). Mathematically, a clique is an object that designates a maximal, complete and connected subgraph. The graph here is a set of words (the nodes) and relations (the arcs) that link up words. Cliques differ from 'synsets' in Wordnet [START_REF] Fellbaum | Wordnet, an electronic lexical database[END_REF], representations offered by LSA [START_REF] Landauer | Handbook of latent semantic analysis[END_REF], HAL [START_REF] Burgess | Modelling parsing constraints with high-dimensional context space[END_REF], or other word vector space models [START_REF] Sahlgren | The Word Space Model. Using distributional analysis to represent syntagmatic and paradigmatic relations between words in high-dimensional vector spaces[END_REF]. These models differ in their treatment of meaning, whether or not they use context relations, whether they use hierarchical links between words or proximity (distance within a vector model) and whether they are generated manually versus automatically and statistically. The SA offers a treatment of meaning at the level of relationships between words in the lexicon and ACOM at the level of co-occurrence in text (contexonyms). This treatment does not rely on a subjective hierarchical classification but on a geometrical model generated automatically and statistically which assigns vectors to cliques rather than words and therefore provides representation of word meaning based on units smaller than words. Unlike synsets, cliques are not units of language or metalanguage but rather an infra-linguistic tool. They allow for a very precise treatment of polysemy, which is the main aspect most word vector space models have trouble modeling since these models associate a single vector per word. Cliques provide a representation of meaning going beyond the lexical unit and thus also allow for sense navigation inside and outside the word boundary. In this respect cliques represent a conceptual level of meaning almost independent from words. They reflect the internal complexity and organization of the semantic structure of a word as well as the structural relationship of the word with others words (either within a lexicon, across lexicons or within a corpus).This makes the model a unique tool for translators who are well aware that words are not in a one to one correspondence. For a given word there is an underlying topology to the set of associated cliques that allows us to navigate from a semantic value to another in a continuous paradigm. Cliques organize meanings into value types, such as physical, emotional or perceptual aspects. Since each clique is connected to the next one by one synonym in common, a progressive transition from a meaning to another at subtle semantic levels is made possible. As an example, here are three pairs of cliques for the word mind, taken from the SA: 16: brain, head, mind, nous, psyche 17: brain, intellect, mentality, mind, wit . 38: intention, mind, object, purpose, reason 39: intention, mind, spirit . 43: mark, mind, note, notice, see 44: mark, mind, note, see, watch On the basis of the list of cliques, a matrix composed of cliques as lines and words as columns is created. Then a semantic space is generated from the matrix. This method differs from other word space models that work with word/document matrices or word/paragraph matrices which soon encounter a problem of size limitation. Our model, however, has no size limits regarding corpora. With these matrices we calculate the coordinates of cliques with correspondence factor analysis [START_REF] Benzécri | L'analyse des données : l'analyse des correspondances[END_REF]. Unlike models that assign a vector or a node to a word, geometrical modeling associates a delimited space with a word in a continuous fashion. 2 distance is used between words rather than Euclidean distance as it renders geometrical organization more accurately. Words are represented by the envelopes containing cliques. This way, word envelopes may overlap or not, which provides a very instantaneous visual tool for definition or translation purposes. Finally a hierarchical classification algorithm generates clusters that organize senses. The number of clusters may be defined by the user to shed light on the specific aspects they wish to look at.

The model's parameters and graphical output 1 .2.1 SA parameters and output

The current online version of the model allows users to set a number of parameters at the query level and at the graphical output level. The model is set on default parameters to make all queries manageable at an optimal speed, but can be set to better serve specific querying. Online, up to five words at a time may be queried, using the + sign. This limit was set to better handle the numerous queries the site receives (up to 200.000 a day) but there is no limit as regards the number of words the model can handle as long as the output is decipherable. For a given search word the user can set a number of parameters before calculation and after calculation.

Query parameters (before calculation)

Users may: -Set the search type for English words as standard (narrow synonymy) or enriched (broad synonymy). In the default search uses broad synonymy since there is no distinction between narrow and broad synonymy in French lexicography.

-Choose the number of clusters they wish to visualize, calculated either on the basis of a number of cliques or words. Numerical options are optimal, maximal, or zero. The optimal setting adapts the output to the given input, while the maximal setting integrates all the results and the zero clique option only keeps the envelopes of words. This allows for highlighting one or many specific sub-meanings of a given word.

-Set the number of dimensions to be visualized (up to 15). The model will show core meanings in the first two dimensions; however minor meanings may be contained in the other dimensions. The former can be made to appear directly on the graphical interface by choosing the axes to bring to the fore.

Output parameters (after calculation)

The output is a flexible graphical map. Users can reorganize elements on the map in terms of axes, clusters, and the way lists of items are organized. The number of clusters is set to 3 by default but can be reset to any number via the 'class' option. 'Class 1' clusters elements on the basis of the center of gravity of words (envelopes) whereas 'class 2' clusters elements on the basis of clique sets. Three levels of conceptual organization may be chosen from the list window: the clique, word or cluster. Items may also be organized in alphabetical order, cluster order or geometrical order (from closest to the center to peripheral).

ACOM's parameters and results

Many of the above parameters are valid for ACOM too. However some query options are specific to ACOM as regards co-occurrence settings. The corpus on which the calculations are made may be chosen from a list of available corpora. Then one may set the number of most frequent words to be removed from the output (from 0 to 1000) and set the number of contexonyms shown. Three other parameters allow for selecting the number of words or the percentage of words the calculation should be applied on. The first one (α) applies to search words, the second to their children (β) for second order co-occurrence and the third (γ) to cliques. ACOM's results closely mirror human word association patterns as shown in [START_REF] Ji | Testing the cognitive relevance of a geometric model on a word-association task: A comparison of humans, ACOM, and LSA[END_REF]. The authors show that subject's responses in word association tasks matches ACOM's results well, therefore validating the model's cognitive relevance. On this task ACOM performed better than LSA.

Corpora and databases

All the databases listed below are accessible online and available on request. The model handles a synonym database, a translation database and a 'contexonym' (ACOM's co-occurrence) database. The synonym database contains, for each entry word, a list of its synonyms, each indexed by the number of cliques it contains and a list of cliques that contain the entry word. The databases are complete for English and French and in progress for Spanish, Portuguese and Korean. The initial French database was made of seven synonym dictionaries which were compiled with a process of symmetrisation. 1 In English the database was extracted from several thesauri (including the Roget's thesaurus). To compile the databases the relationships between words were kept but not the thesauri's structure. The data was entirely restructured, merged and symmetrised automatically with the help of the model. The translation databases contain for each entry word its equivalent in the target language and a list of cliques in both languages associated with it. The English-French, French-English as well as Spanish-French databases are complete, while Portuguese-French, Portuguese-English, Spanish-English, Korean-French, Korean-English, Korean-Spanish and Korean-Portuguese databases are in progress. Synonym and translation databases are available for consultation online on http://dico.isc.cnrs.fr and http://dico.nv.isc.cnrs.fr. The contexonym databases associate for each English or French token its frequency count from the corpus and a list of its sentence or paragraph co-occurrences each indexed with co-occurrence frequencies. At the moment the corpora available online are the BNC and Project Gutenberg in English and five years of French newspapers' corpus (including "Le Monde"). However, other corpora may be dealt with by the model.

Examples

Several linguistic indicators come out in the representations produced by the SA and ACOM: Prototypicality and productivity may be evaluated at a glance by looking at the position of elements relative to the origin of axes, the number of cliques produced as well as the size, position and complexity of the space attributed to words. Below, we illustrate the model with queries on a sample word -mind-, using an English synonym query, an English-French translation query and with ACOM, in that order.2

Monolingual Synonymy representations with the SA

The monolingual representation of mind when set to three clusters clearly shows one verbal and two nominal clusters that do not overlap but are linked up by weaker clusters (fig. 1).

The meaning of idea is connected to the one of will via disposition, and idea is connected to being careful through marking. Meanings closer to the origin of axes are closer to a generic or core value determined by the model. Homonymous words will appear completely separate from this generic value. With cliques being organized in a continuous fashion, it is possible to navigate conceptually from verbal to nominal meanings and see which sub-meaning sets are shared or isolated. For instance the first verbal clique lists "1: attend, attend to, look after, mind" whereas no nominal clique retains the affective aspect found in 'to look after'. However the following conceptual path : to look after -to look -to watch -to seeto notice -to note -to mark -to bear in mind -to remember -memory shows how one may navigate from a verbal value to a nominal one in a continuous fashion. This type of path may be explored graphically by moving the cursor over the map to make cliques appear, so that spatial organization may guide the understanding of semantic organization. The path may also be explored in more detail by looking at the cliques' list in the 'query information' link.

Translation (English-French) representations with the SA

The model can also be used in translation to distinguish values and determine which lexical unit is relevant (Ploux & Ji, 2003). The representation shows which senses are linked by a continuous conceptual path across the two languages and which ones are completely disconnected and do not overlap. On fig. 2 the envelope for memory is isolated and not connected to the others, as well as further away from the origin. This sense is the oldest etymological definition of the word mind and is obsolete (cf. Oxford English Dictionary). On the contrary, the two other sets show different sizes and relative strength in the two languages and a connecting concept between the two meaning areas.

The example of mind is particularly challenging since there is no straightforward translation of this word in the target language. The closest translation of mind is esprit; however esprit also means spirit. Where traditional MT systems might fail at choosing the best candidate, the graphical representation provides a tool to sort the possible candidates to translation. The map shows that esprit only represents a small space within mind and therefore is not a satisfactory translation in many cases. It is however very close to the origin, and therefore very close to mind's core meaning (as determined by the model for this specific calculus). The number of cliques generated in each language is a first indicator of the extent to which lexical units match each other and how productive each sub-meaning is. For instance here we obtain 73 terms and 55 cliques for mind versus 104 terms and 156 cliques for esprit. This discrepancy highlights the number of senses Figure 2: Illustration of a translation query for mind with the SA. English clusters are in blue, French ones in green. Esprit, in red, is the most probable candidate for translation. covered by esprit but not by mind. This partly explains why esprit may not be a good candidate since it carries a lot of meaning not included at all in mind. However both share the first most productive conceptual sub-group (alike to a semantic field) that may be defined as a set related to [intelligence], but differ at the level of the second most productive element, respectively [character] for mind and [belief] for esprit.

ACOM representations

The SA deals with synonymy but does not provide insight regarding word use in context. Paradigmatic relations may be sufficient in some types of research, but for a more complete approach syntagmatic relations are also necessary. Some words are weakly represented by synonymy, such as referential words (nouns of objects such as notebook) that may have a high frequency in a corpus but very few synonyms. In these cases, syntagmatic relations provide more information as to the word's semantics than paradigmatic ones. ACOM focuses mainly on syntagmatic relations as it exploits word co-occurrences in corpus. In includes some paradigmatic information as well since it incorporates second-order relations and uses broad co-occurrence windows. ACOM relies on cliques which are maximal sets of words in co-occurrence and selects words that co-occur in a homogeneous stylistic environment, giving information regarding genre, by default, whereas the SA provides a means to navigate the scale of genres independently of text. In this aspect the two models show complementary uses at the level of language and at the level of text. In the following illustration (fig. 3) we show how ACOM can be used to deal with the idiomatic aspect of language. The graph is not a default result but an example of a user's choice of visualization:

The collocations frame of mind, peace of mind, mind (your) business and change (my) mind are highlighted on top of the other meanings (knowledge, thought…). These collocations show and classify word use in context.

Clusters

As illustrated in the above examples, clusters: -Separate values within a monolingual representation on scales such as perception, action, emotion, etc.

-Detect overlapping and non-overlapping values across two languages.

-Separate values of a word's meaning according to its context of use. Furthermore, as clusters allow for overlap detection, they may be used to analyse other types of linguistic data. For instance, clustering contributes to evaluating the impact of several factors over word meaning as shown in (Boussidan et al., 2009a). In this case historical data -here etymological roots -was confronted with sound-form data -here phonaesthemes. Clustering is purposefully customizable so various linguistic needs may be met.

Current uses of the model and future perspectives

Currently, the model is used for the automatic treatment of polysemy and semantic disambiguation [START_REF] Venant | Utiliser des classes de sélection distributionnelle pour désambiguïser les adjectifs[END_REF], and in two question answering projects relying on the synonym database to expand queries in order to cover the possible spectrum of senses more accurately [START_REF] Grau | FRASQUES: A Question-Answering System in the EQueR Evaluation Campaign* LREC[END_REF], and Project TCAN-CNRS 2003[START_REF] Lachaud | La prégnance perceptive des mots parlés : une réponse au problème de la segmentation lexicale[END_REF]. It has also been used in psycholinguistics research at the University of Geneva [START_REF] Lachaud | La prégnance perceptive des mots parlés : une réponse au problème de la segmentation lexicale[END_REF] in a survey to define the age of word acquisition in French as well as degrees of familiarity of words. Semi-automatic metaphor extraction and analysis may also be conducted with the model as shown in Oliveira & Ploux (to be published). Furthermore, various avenues of research are being explored to enrich and expand the model: Several languages are added to the translation databases. EEG studies in online word processing use the model's clustering tool for data analysis. Graphic research on meaning representation and structural properties of geometrical forms is conducted in a perspective of functional visualisation. Dynamic diachronic modelling to assess semantic change is in progress while specific phenomena such as neology is investigated as described in [START_REF] Boussidan | La malbouffe : un cas de néologie et de glissement sémantique fulgurants. Atelier "Du thème au terme, émergence et lexicalisation des connaissances[END_REF]. The ACOM model also proved to be an excellent candidate for experimental cognitive tasks since it provides a good simulation of human responses as shown in [START_REF] Ji | Testing the cognitive relevance of a geometric model on a word-association task: A comparison of humans, ACOM, and LSA[END_REF].

Outside of the academic world, translators, journalists, writers and artists also use the model to guide their linguistic creativity.

We now aim at making the model open source, at easing its manageability as well as enhancing the availability of resources for all users to further profit the NLP, translation and psycholinguistics communities. We plan to make new corpus use more straightforward and to open the model to international multilingual collaborations in order to develop a collaborative semantic platform.

Conclusion

The AS and ACOM provide extremely fine-grained tools to detect and analyse linguistic patterns in corpora at the syntagmatic and paradigmatic level as well as across languages. The models offer many possibilities in NLP, MT, psycholinguistics and cognitive science as well as outside the academic world. They are now evolving towards a more participative and dynamic format to allow several avenues of research to merge, and welcome collaborations in different sectors.

Figure 1 :

 1 Figure 1: Illustration of a synonym query for mind with the SA. The main clusters are in blue, and the connecting clusters in red.Figure2: Illustration of a translation query for mind with the SA. English clusters are in blue, French ones in green. Esprit, in red, is the most probable candidate for translation.

Figure 3 :

 3 Figure 3: Illustration of an ACOM query for mind

These dictionaries are the Bailly, Benac, Du Chazeaud, Guizot, Lafaye, Larousse and Robert. Once compiled they provided

The settings in the examples differ depending on what aspect of meaning is highlighted.

Acknowledgements

Thanks to Charlotte Franco, Masters student in Cognitive Science, and to all the people who participated in the model and databases (listed on http://dico.isc.cnrs.fr/en/membres.html)


Armelle Boussidan
email: armelle.boussidan@isc.cnrs.fr

Sabine Ploux
email: sploux@isc.cnrs.fr

Using Topic Salience and Connotational Drifts to Detect Candidates to Semantic Change

Semantic change has mostly been studied by historical linguists and typically at the scale of centuries. Here we study semantic change at a finer-grained level, the decade, making use of recent newspaper corpora. We detect semantic change candidates by observing context shifts which can be triggered by topic salience or may be independent from it. To discriminate these phenomena with accuracy, we combine variation filters with a series of indices which enable building a coherent and flexible semantic change detection model. The indices include widely adaptable tools such as frequency counts, co-occurrence patterns and networks, ranks, as well as model-specific items such as a variability and cohesion measure and graphical representations. The research uses ACOM, a co-occurrence based geometrical model, which is an extension of the Semantic Atlas. Compared to other models of semantic representation, it allows for extremely detailed analysis and provides insight as to how connotational drift processes unfold.

Introduction

Semantic change has long been analyzed and theorized upon in historical linguistics. Its abstract and ungraspable nature made its detection a difficult task for computational semantics, despite the many tools available from various models of lexical treatment. Most extant theories are based on manual analysis of century long semantic drifts. From these works we inherit various typologies and repertories of causes of change (e.g., [START_REF] Bloomfield | Language[END_REF]). However these types of analyses may not be suited to the large scale production of text in our societies. Not only has the quantity of produced text rocketed but its diffusion and speed of transmission has radically increased. In this context, recent studies have yielded promising results, showing that computational models of semantics can deal with assessed semantic change examples as well as detect candidates in corpora. Among them, some include topic salience as an index and others do not, as they rather try to quantify semantic change with reliable measures. In an era of information overflow, topic change takes on a new linguistic value, as it may be responsible for extremely quick paced semantic change, which can be ephemeral or become fixed. Topic salience might as well be a sociologically induced or press phenomenon with no semantic impact at all. However when both topic salience and connotational drift take place, a semantic phenomenon may be at stake. Our analysis is anchored in this process. We shall briefly introduce other approaches, explain our methods and the structure of our detection prototype (in progress) as well as give preliminary results before concluding with a discussion.

Measuring semantic change : previous work

To measure semantic change, one has to evaluate the semantics of a lexical item at a given point. To do so, semantic similarity measures in vector spaces or geometrical spaces may be used to compare the item with its own occurrences at later points. This method has been applied in [START_REF] Sagi | Semantic density analysis: Comparing word meaning across time and phonetic space[END_REF], where semantic density was calculated as the average angle between vectors in a semantic space. The variability of that density was observed for the same lexical item at different points in time. Density measures were applied to a series of acknowledged semantic change cases, in the Project Gutenberg Corpus, a historical corpus of English organized by documents. Results mostly include broadening and narrowing cases. The same method yielded results on the difference between nominal and verbal types of change, showing that verbs were more likely to change than nouns [START_REF] Sagi | Nouns are more stable than verbs: Patterns of semantic change in 19th century english[END_REF]). [START_REF] Cook | Automatically identifying changes in the semantic orientation of words[END_REF] also used assessed cases from the historical linguistics literature. They detected changes in the semantic orientation of words (or polarity shifts) namely amelioration and pejoration. They then applied this methodology to detect possible un-assessed candidates. They used three English corpora as corpus slices, covering approximately a four century time-span. Volatility has also been assessed by [START_REF] Holz | Towards automatic detection and tracking of topic change[END_REF], who adapted a measure from econometrics to quantify semantic change in a time sliced corpus. The volatility measure relied on the computation of the rank series for every co-occurent term and on the coefficient of variation of all co-occurrent terms [START_REF] Holz | Towards automatic detection and tracking of topic change[END_REF]). The method was applied to search words in modern corpora in German and English (the Wortschatz and the New York Times). The strong point of this measure is that it is independent from word frequency, however it does not provide detailed analysis about the underlying semantic processes.

Methods

Of the three cited works, our approach is closer to that of [START_REF] Holz | Towards automatic detection and tracking of topic change[END_REF] in that both their work and ours are conducted on very recent corpora. We are currently conducting short diachrony detection, analysis and representation on a modern press corpus in French (the newspapers Le Monde, 1997Monde, -2007)). We use the ACOM model [START_REF] Ji | Lexical knowledge representation with contexonyms[END_REF]) an extension of the Semantic Atlas Model [START_REF] Ploux | The semantic atlas: an interactive model of lexical representation[END_REF]) that uses factor analysis to provide geometrical representations of word co-occurrence in corpus (both models are freely available on http://dico.isc.cnrs.fr/eng/index.html). The model relies on cliques, which are organized subsets of co-occurrent words, from which clustering can be made. To extract co-occurrent words, we apply ACOM on a time-sliced corpus. For each slice t, a word-association table is constructed using all headwords (see [START_REF] Ploux | The semantic atlas: an interactive model of lexical representation[END_REF] for a complete methodological description). Each headword W i t (1≤i≤N , where N is the total number of types in the corpus slice) has children (c j s) that are arranged in descending order of co-occurrence with W i t1 :

W i t : c1; c2; . . . ; cn
We apply two factors to filter this table: α where 0≤α≤1 to eliminate the rarely co-occurring children of W i n :

W i t : c1; c2; . . . ; ck
where k = nα and n is the original number of children of W i t , and β where β(0≤ β ≤1) to cut off rarely co-occurring of children of c j :

(c m j : g1; g2; . . . ; gl(1≤j≤k; l = mβ))

On the basis of that table, cliques are calculated. The notion of clique is taken from graph theory (on graph therory see for ex. [START_REF] Golumbic | Algorithmic graph theory and perfect graphs[END_REF]). Mathematically, cliques are maximum connected subgraphs. In our case, the nodes are contexonyms. Then, correspondence factor analysis is applied [START_REF] Benzécri | L'analyse des données : l'analyse des correspondances[END_REF]) and the χ 2 distance is calculated between pairs of cliques to obtain a multidimensional space. A hierarchical clustering algorithm clusters cliques in thematic sets at several degrees of detail. Clusters show broad topic shifts whereas the cliques show fine-grained sub-organisation. Therefore the model allows for very detailed analysis as well as topical analysis. It also provides a graphic visualization for the semantics of a word. With the time-sliced corpus, we may extract maps for each subpart of the corpus and compare the spaces generated for the same word at different points in time, to complete the analysis.

Structure of the detection prototype

Currently our model is structured as follows: the corpus is transformed into a time-sliced ACOM database, with word frequencies and co-occurence frequencies. We apply an adjustable standard deviation filter to extract significant frequency and co-occurrence frequency variations as well as cooccurrence network variations. (The co-occurrence window is adjustable to the sentence, paragraph or other window sizes). If we only detect frequency variation, there is a suspicion that the headword might undergo context variation later, but it could also be an ephemeral press or fashion phenomenon with no semantic impact. However if we detect both significant frequency variations and co-occurrence variations, there is a higher chance that the context variations are a reflection of semantic variation. At this stage we apply indices based on rank variation, clique analysis and clique-term variation analysis (described in [START_REF] Boussidan | Vers une méthode de visualisation graphique de la diachronie des néologies[END_REF]) as well as manual analysis to determine the nature of the change. The next step to verify that the item has undergone semantic change is its stabilization over time. This detection path highlights short diachronic change. We may also detect significant co-occurence variations with no significant headword frequency variation, in which case we may apply directly the indices to check whether the context shifts reveal an anchored meaning shift. If the indices highlight a meaning shift, the former is necessarily much more subtle than the short diachronic change that we detected previously. It might be the reflection of a longer term process of which the trigger might not be contained in the given corpus.

Preliminary results

Testing examples

To conceive a detection model, we first conducted experiments using attested examples or using words that we selected after manually observing that a shift was taking place. By testing these examples, we could extract data about how the model would render them so as to use it to create detection indices and parameters. Among these was the French word malbouffe (literally "bad grub" or "junk food"), a neology selected from a previously established list of new dictionary entries [START_REF] Martinez | L'évolution de l'orthographe dans les Petit Larousse et les Petit Robert 1997-2008: une approche généalogique du texte lexicographique[END_REF]). The corpus showed how the different spellings of the words alternated before yielding the current one. Analysis of the co-occurrence networks showed that one of the most important co-occurrent words, Bové, the name of a French political actor, had almost the same co-occurrence network as malbouffe. From this observation and after comparing definitions and previous contexts of use, we could infer that this person gave the word malbouffe its new meaning, by superimposing political values on it, on top of its dietetic values. Co-occurrence networks therefore allowed us to analyse the process of meaning shift. The full analysis of this example may be found in [START_REF] Boussidan | La malbouffe : un cas de néologie et de glissement sémantique fulgurants[END_REF]. We also tested a more subtle connotational drift with the word mondialisation ("globalization"), which undergoes clear contextual change in the corpus. The word first appeared in contexts defined by the political, economical and intellectual positions it brings about, with strong co-occurrents such as défi ("challenge"), progrès ("progress") or menace ("threat"). It then drifted into a complete network of words related to one single French political movement of anti-globalization in 2001. Therefore the use of mondialisation gained a new connotation, whereas its synonym globalisation ("globalization") remained quite neutral politically. The analysis of this example revealed that some terms were used as pivots, providing linkage between the existing cliques and the new ones. Pivots therefore provided a good tool to observe meaning re-organisation. The full analysis of this example may be found in [START_REF] Boussidan | Vers une méthode de visualisation graphique de la diachronie des néologies[END_REF] and the corresponding dynamic representation on http://dico.isc.cnrs.fr/ en/diachro.html.

Semantic change detection

On the basis of these preliminary examples, we designed a semantic change detection prototype. Testing examples brought to light the difficulty of discriminating press-related topic salience with no semantic impact from topic salience with a semantic impact. Detection is conducted in three stages. The first stage relies on frequency variation to extract topic variations of context in the corpus. For instance by setting the filter to retain words for which the coefficient of variation2 is higher than 0.5, we obtain a list of words that may be classified into three loose semantic sets and a fourth set grouping all independent items. These semantic sets include words related to:

• war, terrorism and violence

• technology • illness
By adjusting the settings we mayalso include more subtle topic variations if needed or conversely, looser ones. The second stage involves co-occurrence variation so as to extract the changes in semantic networks and thus in connation, for a lexical item. For instance, we detected that the word logiciel ("software") underwent a frequency co-occurrence peak with libre ("free") in January 2001. The expression logiciel libre stands for "freeware" and has been renamed gratuiciel or graticiel (a blending of gratuit, "free" with logiciel, "software") in Quebec. We therefore detect a new compositional expression that coins a French equivalent to the word freeware used until then.

Another example of connotational drift is the word navigation ("navigation") which is only attested in the TLFI3 and the Dictionnaire Historique de la Langue Française [START_REF] Rey | Dictionnaire historique de la langue française : contenant les mots français en usage et quelques autres délaissés, avec leur origine proche et lointaine[END_REF]), under the meaning relating to transport, firstly on seas and rivers and then via plane or spaceship. However, between 1997 and 2001 the word takes on a new major meaning in internet search, meaning "browsing". This is aparent when looking at the co-occurrence patterns of navigation with words related to technology and comparing them with co-occurrences of words related to transport. The technology words show peaks between 1997 and 2001 and then lower frequencies until 2007, whereas the transport words show stable use all the way through the corpus. The new use of navigation, however is almost obsolete now in spoken speech -or at least it has gone out of fashion-but the semantics of navigation have clearly integrated an additional domain and broadened. A simple search of French results on Google provides 5,500,000 documents for navigation internet, among which are a lot of recent ones. However the meaning to search the internet grew from the name of a specific web navigator: the Netscape Navigator which was widespread in the 1990s but is no longer supported nowadays.

Both previous stages provide us with candidates to semantic change. The last stage is the stabilization of a connotational drift, whether it is a broadening, a narrowing, a domain shift or other. We are currently working on this last index. We often find that when a word undergoes semantic change, it goes through a phase of onomasiological competition in which other possible candidates may in turn become the new bearers of certain meanings. For navigation for instance, the word surf was a competitor, however both words now sound obsolete. It may be that none of them wins the competition, in which case the concept has become so deeply anchored in language and society that it does not need naming any more.

Discussion and Future Work

Since semantic phenomena, whether synchronic or diachronic, are very much corpus specific, it is difficult to conceive of a large scale universal detection method for them. However, tools may be built to be highly flexible in order to allow users to adjust settings to adapt to the corpus they deal with. This flexibility may encompass genre and stylistic variations when working with the same language as well as adaptation to a completely different language. We are considering global evaluations of the corpora's stylistics to avoid the detection of corpus specfic phenomena instead of broader language phenomena.

Ideally the model should also be able to deal with timescale differences.The precise adjustment of these settings is part of our future research avenues along with incorporating an index for stabilization. This last filter is particularly difficult to create when dealing with ongoing phenomena. We may sometimes need to wait a few years to be able to establish whether a semantic change has stabilized. To summarize, we are currently developing a filtering tool to extract candidates to semantic change on the basis of topic salience variation in corpus and co-occurrence network variation. Our approach shed light on the emergence of these phenomena at a very detailed level. Preliminary results showed that the tool was succesful at extracting those candidates; however it is not yet advanced enough to discriminate between context changes that affect a word without semantic impact and those that do have a semantic impact. This aspect constitutes our current research perspective.

Children with co-occurrences under a 10,000th of the global frequency of the headword W i t are removed to reduce noise.

The coefficient of variation is the ratio of the standard deviation to the mean

http://atilf.atilf.fr/tlf.htm

Acknowledgements

This research is supported by the Région Rhône-Alpes, via the Cible Project 2009. Many thanks to Sylvain Lupone, previously engineer at the L2c2 for the tools he developed in this research's framework.