Salwa Tabet Gonzalez
email: tabetgonzalez@unistra.fr

Predrag Janičić
email: janicic@matf.bg.ac.rs

Julien Narboux
email: narboux@unistra.fr

Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving

Keywords: synthetic geometry, automated deduction, proofs, constraint solving, abducts

Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach.

Introduction

Automated theorem provers take as input the formal statement of a conjecture in a theory described by axioms and lemmas, and try to generate a proof or a counter-example for this conjecture. In the field of geometry, several efficient automated theorem proving approaches have been developed, including algebraic ones such as Wu's method, Gröbner bases method, and semi-synthetic methods such as the area method. In these approaches, typically, the conjecture and the axioms being considered are fixed. However, in mathematical practice, in the context of education and also in mathematical research, the conjecturing and proving activities are not separated but interleaved. The practitioner may try to prove a statement which is valid only assuming some implicit or unknown assumptions, while the list of lemmas and theorem which can be used may not be complete. In education, for some kind of exercises, a precise formulation of the statement to be proved is also left to the student, with questions such as: "What is the nature of the quadrilateral ABCD?". Hence, the conjecture can contain unknown assumptions called abducts, and the goal may be not completely specified. One may also ask for a proof using a particular theorem or an intermediate fact, i.e., a proof partially specified using constraints specifying some proof steps.

In this paper, we consider the problems of (simultaneously) completing (a) the assumptions of the conjecture; (b) the goal of the conjecture; (c) a proof sketch for the conjecture. The completion process should lead to a proof that is both machine-checkable and human-readable. Because we aim at producing intelligible and readable proofs, with a similar level of granularity as paperand-pencil proofs, our approach is logic-based, uses a fragment of first-order logic called coherent logic, and is focused on synthetic geometry (in contrast to algebraic methods). Our approach for dealing with partial conjectures and partial proofs is implemented as an extension of the automated theorem prover Larus developed previously [START_REF] Janičić | Theorem Proving as Constraint Solving with Coherent Logic[END_REF] . The approach is uniform for all three kinds of completion tasks, flexible and, to our knowledge, unique such approach.

We list five high-school level synthetic geometry problems related to Varignon's theorem (Fig. 1), that we will try to solve using our approach.

Problem 1 (Fully specified statement) Consider a quadrilateral ABCD, let E, F , G and H be the midpoints of AB, BC, CD, DA respectively. Prove that the quadrilateral EF GH is a parallelogram (assuming that there are no two sides that are aligned). Problem 2 (First inverse problem) Consider a quadrilateral ABCD, let E, F , and G be the midpoints of AB, BC and CD respectively. Let H be a point. Under which assumption is the quadrilateral EF GH a parallelogram? Problem 3 (Second inverse problem) Consider a quadrilateral ABCD, let E, F , G and H be the midpoints of AB, BC, CD, DA respectively. Under which assumption is the quadrilateral EF GH a rectangle?

Problem 4 (Partially specified goal) Consider a quadrilateral ABCD, let E, F , G and H be the midpoints of AB, BC, CD, DA respectively. What is the nature of the quadrilateral EF GH? Problem 5 (Partially specified proof ) Consider a quadrilateral ABCD, let E, F , G and H be the midpoints of AB, BC, CD, DA respectively. We have that EG = F H. Prove that EF GH is a rectangle using the axiom "If the diagonals of a parallelogram are congruent, then it's a rectangle".

The above examples are inspired by exercises given in a teacher training session.

A more detailed discussion about how these examples can be used in a didactic context, issues related to the formalization can be found in [START_REF] Durand-Guerrier | Examining the Role of Logic in Teaching Proof[END_REF][START_REF] Narboux | Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education[END_REF] 2 Background

This section provides some necessary background information on a fragment of first-order logic called coherent logic that our approach uses. There are several automated provers for coherent logic, including Larus, which is based on "theorem proving as constraint solver" paradigm.

Coherent Logic

A formula of first-order logic is said to be coherent if it has the following form:

A 0 (⃗ x) ∧ . . . ∧ A n-1 (⃗ x) ⇒ ∃⃗ y(B 0 (⃗ x, ⃗ y) ∨ . . . ∨ B m-1 (⃗ x, ⃗ y))
where universal closure is assumed, and where ⃗ x denotes a sequence of variables x 0 , x 1 , . . . , x k-1 ; A i (for 0 ≤ i ≤ n -1) denotes an atomic formula (involving zero or more variables from ⃗ x); ⃗ y denotes a sequence of variables y 0 , y 1 , . . . , y l-1 ; B j (for 0 ≤ j ≤ m -1) denotes a conjunction of atomic formulae (involving zero or more of the variables from ⃗ x and ⃗ y) [START_REF] Janičić | Theorem Proving as Constraint Solving with Coherent Logic[END_REF]. If there are no formulae A i , then the left-hand side of the implication is assumed to be ⊤. If there are no formulae B j , then the right-hand side of the implication is assumed to be ⊥.

There are no function symbols with arity greater than zero. Coherent formulae do not involve the negation connective. A coherent theory is a set of sentences, axiomatized by coherent formulae, and closed under derivability. A number of theories and theorems can be formulated directly and simply in coherent logic (CL). In addition, any first-order theory can be translated into CL, possibly with additional predicate symbols [START_REF] Dyckhoff | Geometrization of first-order logic[END_REF][START_REF] Polonsky | Proofs, Types and Lambda Calculus[END_REF]. Synthetic geometry can be expressed easily using CL. For example, the central part of axioms system of Euclid (as formalized by Beeson et. al. [START_REF] Beeson | Proof-checking Euclid[END_REF]), or Hilbert (as formalized by Braun et. al [START_REF] Braun | From Tarski to Hilbert[END_REF]), or Tarski [START_REF] Schwabhäuser | Metamathematische Methoden in der Geometrie[END_REF] can be expressed in first-order logic without function symbols, and the axioms are mostly in CL form.

Translation of FOL formulae into CL involves elimination of the negation connectives: negations can be kept in place and new predicates symbols for corresponding sub-formula have to be introduced, or negations can be pushed down to atomic formulae [START_REF] Polonsky | Proofs, Types and Lambda Calculus[END_REF]. In the latter case, for every predicate symbol R (that appears in negated form), a new symbol R is introduced that stands for ¬R, and the following axioms are introduced: ∀⃗ x(R(⃗ x)∧R(⃗ x) ⇒ ⊥), ∀⃗ x(R(⃗ x)∨R(⃗ x)).

In contrast to resolution-based theorem proving, in forward reasoning for CL, the conjecture being proved is kept unchanged and proved without using refutation, Skolemization and clausal form. Thanks to this, CL is suitable for producing human-readable synthetic proofs and also machine verifiable proofs [START_REF] Bezem | Automating Coherent Logic. 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning -LPAR 2005[END_REF][START_REF] Dyckhoff | Geometrization of first-order logic[END_REF]. The problem of provability in CL is semi-decidable. CL admits a simple proof system, a sequent-based variant is as follows [START_REF] Stojanović | A Vernacular for Coherent Logic[END_REF]:

Γ, ax, A 0 (⃗ a), . . . , A n-1 (⃗ a), B 0 (⃗ a, ⃗ b) ∨ . . . ∨ B m-1 (⃗ a, ⃗ b) ⊢ P Γ, ax, A 0 (⃗ a), . . . , A n-1 (⃗ a) ⊢ P MP Γ, B 0 (⃗ c) ⊢ P . . . Γ, B m-1 (⃗ c) ⊢ P Γ, B 0 (⃗ c) ∨ . . . ∨ B m-1 (⃗ c) ⊢ P QEDcs (case split) Γ, B i (⃗ a, ⃗ b) ⊢ ∃⃗ y(B 0 (⃗ a, ⃗ y) ∨ . . . ∨ B m-1 (⃗ a, ⃗ y))
QEDas (assumption)

Γ, ⊥ ⊢ P QEDefq (ex falso quodlibet)

In the rules given above, it is assumed: ax is a formula A 0 (⃗ x) ∧ . . . ∧ A n-1 (⃗ x) ⇒ ∃⃗ y(B 0 (⃗ x, ⃗ y) ∨ . . . ∨ B m-1 (⃗ x, ⃗ y));4 ⃗ a, ⃗ b, ⃗ c denote sequences of constants (possibly of length zero); in the rule MP (extended modus ponens), ⃗ b are fresh constants; ⃗ x and ⃗ y denote sequences of variables (possibly of length zero); A i (⃗ x) (respectively B i (⃗ x, ⃗ y)) have no free variables other than from ⃗ x (respectively ⃗ x and ⃗ y); A i (⃗ a) are ground atomic formulae; B i (⃗ a, ⃗ b) and B i (⃗ c) are conjunctions of ground atomic formulae; Φ denotes the list of conjuncts in Φ if Φ is conjunction, and otherwise Φ itself. In the proving process, the rules are read from bottom to top, i.e., by a rule application one gets the contents (new sub-goals) above the line. For a set of coherent axioms AX and the statement A 0 (⃗ x) ∧ . . . ∧ A n-1 (⃗ x) ⇒ ∃⃗ y(B 0 (⃗ x, ⃗ y) ∨ . . . ∨ B m-1 (⃗ x, ⃗ y)) to be proved, within the above proof system one has to derive the following sequent (where ⃗ a denotes a sequence of new symbols of constants):

AX , A 0 (⃗ a), . . . , A n-1 (⃗ a) ⊢ ∃⃗ y(B 0 (⃗ a, ⃗ y) ∨ . . . ∨ B m-1 (⃗ a, ⃗ y)).
Notice that, in the above proof system, case split may occur only at the end of a (sub)proof. However, it is not a substantial restriction: any proof with unrestricted use of case split can be transformed to such form.

Theorem Proving as Constraint Solving and the Larus System

"Theorem proving as constraint solving" is a paradigm for automated theorem proving recently proposed [START_REF] Janičić | Theorem Proving as Constraint Solving with Coherent Logic[END_REF]. In contrast to common automated theorem proving approaches, in which the search space is a set of some formulae and what is sought is again a (goal) formula, this new approach is based on searching for a proof (of a given length) as a whole. Namely, a proof of a formula in a fixed logical setting can be encoded as a sequence of natural numbers obeying some constraints. A suitable solver can find such a sequence and from that sequence a sought proof can be reconstructed. This approach is implemented in C++, within an open-source prover Larus,5 specialized in proofs in coherent logic and using SAT, SMT, and CSP solvers for solving sets of constraints. Larus can generate readable, human understandable proofs in natural language and also machine-verifiable proofs for the interactive provers Coq, Isabelle, and Mizar.

Each CL proof consists of several proof steps, while each of them has one of the following kinds (with obvious meaning): Assumption, MP, FirstCase, SecondCase, QEDbyCases, QEDbyAssumption, QEDbyEFQ. The information relevant for MP steps include: AxiomApplied, From (the ordinal numbers of proof steps justifying premises of the axiom applied), Instantiation (of the variables in the axiom), Contents (the atoms in formula in the proof step), etc. Nesting denotes the nesting of the proof step (the nesting of the first step is 1).

The proof can be represented by a sequence of numbers, meeting some constraints (that correspond to definitions of inference steps given in Section 2.1). For instance, if the proof step s is of the kind QEDbyEFQ, then the following conditions must hold (given almost in verbatim as in our C++ code): 61. StepKind (s) = QEDbyEFQ; 2. s > 0; 3. Contents (s -1)(0) = ⊥; 4. Goal (s); 5. Nesting (s) =Nesting (s -1).

The above conditions can be understood in the following way: if there is a proof of the given conjecture, the proof step s in that proof is of the kind QEDbyEFQ iff the natural number StepKind (s) equals the unique code for QEDbyEFQ, s > 0 (since there must be a previous step), the contents of the previous proof step is ⊥, the contents of the step is the goal itself, and the nesting of the steps s -1 and s is the same. Each proof step has one of the listed kinds and meet corresponding conditions. There are also some additional, global constraints, like that the last proof step has Nesting equal 1.

Larus works in the following way. If there is a set of axioms, a conjecture, and a proof length, a corresponding proof can be represented as a sequence of natural numbers, still unknown, so they will be represented by variables V . The constraints that have to be met for each proof step and for the proof as a whole can be expressed in terms of these variables V . If a solver can find a model for the constraint, from it the proof in logical terms can be reconstructed. All constraints involved are linear constraints over natural numbers. Since linear arithmetic is decidable, decision procedures for it can decide, for each input constrains, whether or not it has a model. For this purpose, Larus can use SAT, SMT, and CSP solvers. For input, Larus uses axioms and conjectures stored in a file in TPTP/fof format.

Abducts and Completing Assumptions

There are three major types of logical inference: induction, deduction, and abduction. The concept of abduction has been introduced by Peirce [START_REF] Peirce | Collected papers of Charles Sanders Peirce[END_REF]. In deduction, everything inferred is necessarily true, while it is not the case with the remaining two types of inference. Induction tries to infer general rules based on individual instances. The aim of abduction is to produce additional hypotheses to explain observed facts. Abduction has a wide spectrum of implicit or explicit applications -in everyday life, in education, and in scientific reasoning, including in building mathematical theories, or in software verification. One definition of abduct is given below. Definition 1. Given a theory T and a formula G (the goal to be proved), such that T ̸ |= G, an explanations or abduct is a formula A meeting conditions:

T, A |= G and T, A ̸ |= ⊥.
It is clear that some abducts are not interesting, so there are often some additional restrictions given. There is no general agreement about such restrictions, but two types are most usual: syntactical restrictions (abducts should be of a specific syntactical form) and minimality restrictions (for any other abduct A ′ , if T, A |= A ′ then A ≡ A ′ ). It is reasonable to ask that A is not G, as it is trivial. Some authors also add stronger a restriction that A ̸ |= G (i.e., at least one axiom of T has to be used to prove G).

Approaches for Computing Abducts. Various algorithms to produce different kind of abducts have been developed [START_REF] Atocha | Abductive Reasoning[END_REF]. In abductive logic programming, techniques for abductive reasoning are developed in the context of logic programming. Rules are considered to be Horn clauses [START_REF] Denecker | Abduction in Logic Programming. Computational Logic: Logic Programming and Beyond[END_REF]. According to Russo et al. [START_REF] Russo | On The Use Of Logical Abduction In Software Engineering[END_REF], some systems assume that predicate symbols appearing in abducts do not appear in the conclusion of any rule and that negation does not appear in the conclusion of any rule. This restriction is not realistic in the context of geometry. In our example, we want to accept geometric predicate symbols both in abducts, and in the assumptions and conclusion of theorems. Some approaches are based on Robinson's resolution algorithm, extended such that when no more clauses can be produced, the atomic clauses are considered as a potential abduct and consistency if checked [START_REF] Marquis | Extending abduction from propositional to first-order logic[END_REF]. There are also approaches developed for the context of SMT solving, dealing with decidable theories like linear arithmetic [START_REF] Dillig | Explain: A Tool for Performing Abductive Inference[END_REF][START_REF] Reynolds | Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis[END_REF] In the context of geometry, some algebraic algorithms can generate additional assumptions for the statement to be true. For example, Wu's method [START_REF] Wu | On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry[END_REF] can produce non-degeneracy conditions. Algebraic methods can also be used to generate more general abducts [START_REF] Recio | Automatic Discovery of Theorems in Elementary Geometry[END_REF]. These methods are more efficient than ours, but more specific so cannot be used for arbitrary geometric theories. Also, they cannot generate readable proofs. Moreover, expressing algebraic non-degeneracy conditions in simple geometrical terms is not easy and not always possible [START_REF] Chen | The Projection of Quasi Variety and Its Application on Geometric Theorem Proving and Formula Deduction[END_REF].

Abduction in Synthetic Euclidean Geometry. In this paper, the theory T from Definition 1 is a synthetic Euclidean geometry. In this context, automated finding of proofs allowing abducts may have several applications. For instance, an automated system may help a student or a researcher who tries to prove (or formalize) a theorem with a missing assumption. Barbosa et al. have proposed such goal in the context of interactive proof assistants where conjectures are sent to an SMT solver [START_REF] Barbosa | An Interactive SMT Tactic in Coq using Abductive Reasoning[END_REF].

Non-degeneracy conditions are often overlooked and missing in informal geometry statements. Abductive reasoning is also a task which can be asked explicitly to students. The answer expected by the teacher for Problem 2 is that H should be the midpoint of AD.

Finding Abducts using Larus. In this paper, we restrict consideration of abduction only to coherent logic and only to abducts that are conjunctions of ground atomic formulae. Larus was not implemented with abduction in mind, yet implementation of support for abduction turned out to be very simple, almost trivial, and took less than 100 lines of C++ code. In order to find abducts using Larus, we treat them as a special case of proof steps, in the main proof branch, just after assumptions. We have to add constraints on what such an abduct can be:

1. the abduct is treated as an assumption; 2. the nesting of the abduct equals 1; 3. the abduct is an atomic formula (no branching); 4. the predicate symbol is one of the predicate symbols in the signature; 5. the arguments are among existing symbols of constants; 6. the abduct is not the goal itself; 7. the abduct is not ⊥.

The given conditions may be written in the following way, assuming that the abduct is placed in i-th step of the proof:

1. StepKind (i) =Assumption 2. Nesting (i) = 1 3. Cases (i) = false 4. ContentsPredicate (i, 0) < sizeof (Signature) 5.
for each argument j (up to maximal arity): ContentsArgument (i, 0, j) < sizeof (Constants) 6. Goal (i) = false 7. ContentsPredicate (i, 0) ̸ = ⊥ One can also choose a number of abducts, each leading to the constraints given above. With such additional constraints for each abduct (for additional proof steps in specific positions in a proof sought), with a given set of axioms and a conjecture, and with a concrete proof length, we run Larus as usual. The solving/proving process is the same as without abducts: the constraint solver finds a way to specify a full proof, including the abducts, i.e., under-specified assumptions.

In the above list of conditions, the last two do not follow the basic definition of abduct. Like in some other variants of the definition, the abduct may not be equal to the goal atom because such abducts are trivial. Also, the abduct may not be equal to ⊥, since it is inconsistent. It is important to discard other inconsistent abducts early, so we add one more restriction: the proof of T, A |= G should not end with QEDbyEFQ. Some constructed abducts may still be inconsistent with other assumptions, and we use an external, more efficient automatic theorem prover, Vampire [START_REF] Kovács | First-Order Theorem Proving and Vampire[END_REF], to discard such abducts.

Example 1. For the first inverse problem (Problem 2 from Section 1), Larus produces two consistent, symmetric abducts (the proof obtained with the first abduct is presented in Appendix 7.2):

-"H is the midpoint of AD" -"H is the midpoint of DA" Example 2. For the second inverse problem (Problem 3 from Section 1), Larus produces more than 150 consistent abducts, most of which give degenerate cases, hence are less interesting. Apart from such abducts, we obtained the following abducts and their symmetric variants (the proof with the first abduct is presented in Appendix 7.3):

-"the diagonals HF and EG are congruent" -" ̸ F GH is a right angle" -" ̸ EHG is a right angle" -" ̸ HEF is a right angle" -" ̸ EF G is a right angle"

Deducts and Completing Goals

Non-trivial first-order logic theories have infinite number of theorems. Approaches based on refutation cannot be used with under-specified goals and, hence, cannot be used for completing them. In principle, a controlled forward-reasoning (for instance, based on some kind of breadth-first search) can enumerate all theorems of a theory. However, such a systematic approach can be hardly useful for some practical applications, like looking for possible conjectures of a specific form. Our framework allows (but does not require) specifying partially the form of the goal: for instance, one may specify the dominant predicate symbol in the goal atom, or some of its arguments.

Finding Deducts in Synthetic Euclidean Geometry. In the field of geometry, deduct candidates can also be guessed based on an illustration, giving a concrete model. However, these deduct candidates still have to be verified i.e., proved. Potential deducts could also be listed as large disjunctions of atomic formulae, but this method does not scale when the list of potential deducts is too long.

Finding Deducts using Larus. In Larus, if the goal is given i.e., fully specified, corresponding constraints are added to the full constraint representing a proof sought. Let us assume that the final step of the proof is (some fixed) n and, for simplicity, let us assume that the goal is just a single atom. The corresponding constraint then includes:

1. Nesting (n) = 1 2. Cases (n) = false 3. ContentsPredicate (n, 0) = the goal predicate symbol 4. for each argument j (except for existentially quantified variables):

ContentsArgument (n, 0, j) = the argument from the given goal instantiated.

If the goal is under-specified, for instance, if the predicate symbol is not given (it is given as _ in the TPTP file), the third condition is just ignored. The same holds for the arguments. 7 During the solving process, if there is a model, these slots are filled-in by some concrete values, giving a concrete goal. Overall, support for finding under-specified deducts is very simple. The current implementation finds one possible deduct, but it can be extended to list all possible deducts, similarly as for abducts (as explained in Section 3).

Example 3. For Problem 4 from Section 1, Larus produces the deduct "EF ∥ GH". The proof obtained with such deduct is presented in Appendix 7.4.

Hints and Completing Proofs

Informal proofs, for instance from textbooks, are often partial and incomplete. They may even provide only a part of a full proof, or some instructions like for filling gaps by analogy. Reconstructing proofs using such hints is very important task, as discussed by Gowers and Hales [START_REF] Hales | An argument for controlled natural languages in mathematics[END_REF]: "One dream was to develop an automated assistant that would function at the level of a helpful graduate student. The senior mathematician would suggest the main lines of the proof, and the automated grad student would fill in the details."

Completing Proofs in Synthetic Euclidean Geometry. In the context of geometry, completing proofs could be interesting either as a way to render the formalization process simpler (automation would bring in all the details that are overlooked in pen and paper proofs), or as a tool working behind the scene for providing guidance for what could be the next step in the proof. This objective has been studied by Richard et al. [START_REF] Richard | Didactic and theoretical-based perspectives in the experimental development of an intelligent tutorial system for the learning of geometry[END_REF]. In geometry, hints can also be based on some observations from an associated illustration.

Completing Proofs using Larus. Larus can be instructed to look for a proof of a given conjecture (also possibly only partially specified) meeting some conditions (that we call "hints") [START_REF] Janičić | Theorem Proving as Constraint Solving with Coherent Logic[END_REF]. Therefore, Larus can try, for instance, to reconstruct a proof given only in outline (like proofs in textbooks). Larus use hints in a much more general way than just splitting the problem into sub-problems: for instance, some hint may be used in just one proof branch and cannot be proved itself. Hints do not have to be ordered (one can ask for a proof using X and Y in no particular order), they can be vague, imposed only by partial constraints ("find a proof that uses this particular predicate symbol", or "find a proof using some specific axiom", without the way it is instantiated, etc.).

Completing proofs in Larus is supported similarly as for abducts and underspecified goals -by modifying the corresponding constraints. The main difference is that abducts and incomplete goals are under-specified, so some constraints have to be omitted, while partial proof introduce additional constraints, on top of the common constraints that must be met by all proof steps. For expressing hints, we slightly extended the language TPTP/fof to allow a simple but still quite expressible semantics. Some kinds of hints (not all) are illustrated below.

fof(hintname0, hint, r(_,_), _ , _). fof(hintname1, hint, r(_,_), 5 , _). fof(hintname2, hint, _, 5, ax2(_,_)).

The first hint specifies that some proof step will have an atom of the form r(. . . , . . .). The second hint specifies that the 5th proof step will have atom of the form r(. . . , . . .). The third hint specifies that in the 5th proof step the axiom ax2 is applied.

Example 4. For Problem 5 from Section 1, Larus was able to find a proof around 20% faster with a suitable hint presented in Appendix 7.5.

Conclusion and Future Work

In this paper we have shown how a prover using the "theorem proving as constraint solving" paradigm can be extended such that it can complete partially specified conjectures and partially specified proofs. This extension is simple, and the implementation update is very small. The completion algorithm is uniform, since all three completion tasks (completing assumptions, completing goals, completing proofs) are handled in the same spirit -in terms of adding or deleting some constraints. To our knowledge, this approach is new, and we are not aware of other systems that can address all three sorts of completion tasks. The presented approach is flexible as different variations of completion tasks can be supported. The strength of this approach is also that it can generate both proofs that are human-readable and machine-checkable. The proposed framework has two main limitations. First, in current stage, it can deal only with coherent logic, hence the theories cannot involve function symbols, which excludes geometry proof that use (non-trivial) arithmetic. Second, the framework cannot deal with conjectures whose proofs are long (say, longer than 50 proof steps).

To our knowledge, there is only one other approach in which some kind of proof is encoded, and reconstructed from a model for the corresponding set of constraints -the approach in which rigid connection tableaux are encoded as SAT and SMT instances [START_REF] Deshane | Encoding First Order Proofs in SAT[END_REF][START_REF] Bongio | Encoding First Order Proofs in SMT[END_REF][START_REF] Ralph | Automated Theorem Proving Using SAT[END_REF]. However, in this line of research, neither machine verifiable or readable proofs, nor any of completion tasks are considered.

The presented work can be extended in several directions. One of our goals is to use our framework to help transfer geometry knowledge from informal sources to proof assistants and between proof assistants, while keeping its highlevel structure. In informal sources, statements of theorems may be incomplete, while proofs may be given just in outline. Still, using our approach such contents can be, at least in some cases, completed and turned into a verifiable form. For transferring knowledge from a proof assistant, one would need to go into its specifics, but only to grab (some) proof steps and make hints out of them. We are still to explore these ideas on a larger scale, like one geometry textbook. In the same spirit as the work proposed by Jiang et al. [START_REF] Jiang | Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs[END_REF], our approach could be combined with large language models to perform automatic formalization by extracting data from natural language proofs. More specific to abduction, we are planning to make an in-depth comparison (both qualitative and quantitative) of our tool to other tools for generating abducts.

Appendix

In this appendix, we provide a complete list of lemmas and axioms (in coherent logic form) used in our examples, and the results obtained using Larus. The results were obtained on a PC computer with Intel(R) Core(TM) i7-8565U CPU @ 1.80GHz processor running under Linux (the time spent should give just a general picture of the efficiency of the system).

Problem 1: Varignon's Theorem

The TPTP file used for Problem 1 is the following: If Larus is invoked as: ./larus -l100 -m8 (-l100 means the time limit is 100s, -m8 means that we look for a proof with 8 or fewer steps), it produces the following human-readable proof in 2. It should be proved that pG(e, f, g, h). 5. par(e, f, g, h) (by MP, from par(a, c, e, f ), par(a, c, h, g), ¬col(e, f, g) using axiom lemma par trans; instantiation:

A → e, B → f , C → a, D → c, E → g, F → h)
6. par(f, g, h, e) (by MP, from par(b, d, f, g), par(b, d, e, h), par(e, f, g, h) using axiom lemma par trans; instantiation:

A → f , B → g, C → d, D → b, E → h, F → e)
7. pG(e, f, g, h) (by MP, from par(e, f, g, h), par(f, g, h, e) using axiom defparallelogram2;

instantiation: A → e, B → f , C → g, D → h)
8. Proved by assumption! (by QEDas)

Problem 2: First Inverse Problem

The list of axioms used for the first inverse problem (Problem 2) is the same as in Section 7.1. Only the conjecture is different -the assumption midpoint(A,H,D) is ommitted: ,conjecture,(! [A,B,C,D,E,F,G,H] : (( (~(col(B,D,A)

fof(th_varignon
)) & (~(col(B,D,C))) & (~(col(A,C,B))) & (~(col(A,C,D))) & (( col(E,F,G))) & (B != D) & (A != C) & midpoint(A,E,B) & midpoint(B,F,C) & midpoint(C,G,D)) => pG(E,F,G,H) ))).
If Larus is invoked as: ./larus -l100 -m8 -b1 (-l100 means the time limit is 100s, -m8 means that we look for a proof with 8 or fewer steps, -b1 means that we look for one atomic formula as an abduct), it finds a first consistent abduct (after two inconsistent ones) and produces the following human-readable proof in 3.26 seconds (the abduct found is highlighted):

Consider arbitrary a, b, c, d, e, f , g, h such that:

-¬col(b, d, a), -¬col(b, d, c), -¬col(a, c, b), -¬col(a, c, d), -¬col(e, f, g), -b ̸ = d, -a ̸ = c, -midpoint(a, e, b), -midpoint(b, f, c), -midpoint(c, g, d).
It should be proved that pG(e, f, g, h).

Abducts found:

midpoint(d, h, a)

Problem 3: Second Inverse Problem

The list of axioms used for the second inverse problem (Problem 3) is the same as in section 7.1, extended with the following axioms. It should be proved that rectangle(e, f, g, h).

Abducts found:

cong(e, g, h, f ) If Larus is invoked as ./larus -l100 -m8, it produces the following humanreadable proof (for the goal par(e, f, g, h), highlighted in the proof) in 2.15 seconds:

Consider arbitrary a, b, c, d, e, f , g, h such that:

- It should be proved that (e, f, g, h). The list of axioms used for Problem 5 is the same as presented in Section 7.3 (with the axiom defrectangle3a deleted). The conjecture is the same plus the abduct as an assumption, but we add the following hint:

fof(hint1,hint,_,_,defrectangle4b(4,5,6,7)).

If Larus is invoked as ./larus -l100 -m8, it produces the same proof as in Section 7.3 in 4 seconds, but if the hint is omitted, it takes 5 seconds.

Fig. 1 :

 1 Fig. 1: Illustrations for five problems related to Varignon's theorem, respectively: Problem 1; Problem 2; Problem 3.

  fof(triangle_mid_par_strict, axiom, (! [A, B, C, P, Q] : ( ((~col (A,B,C)) & midpoint(B,P,C) & midpoint(A,Q,C)) => par(A,B,Q,P)) )). fof(lemma_par_trans, axiom, (! [A, B, C, D, E, F] : ((par(A,B,C,D) & par(C,D,E,F) & (~col(A,B,E))) => par(A,B,E,F)))). fof(defparallelogram2,axiom, (! [A,B,C,D] : ((par(A,B,C,D) & par(A ,D,B,C)) => ((pG(A,B,C,D)))))). fof(lemma_parallelNC,axiom, (! [A,B,C,D] : ((par(A,B,C,D)) => ((( col(A,B,C)) & ~(col(A,C,D)) & ~(col(B,C,D)) & ~(col(A,B,D) )))))). fof(lemma_parallelflip,axiom, (! [A,B,C,D] : ((par(A,B,C,D)) => (( par(B,A,C,D) & par(A,B,D,C) & par(B,A,D,C)))))). fof(lemma_parallelsymmetric,axiom, (! [A,B,C,D] : ((par(A,B,C,D)) => ((par(C,D,A,B)))))). fof(midpoint_sym, axiom, (! [A, B, I] : (midpoint(A,I,B) => midpoint(B,I,A)))). fof(lemma_tP_trans, axiom, (! [A, B, C, D, E, F] : ((tP(A,B,C,D) & tP(C,D,E,F)) => tP(A,B,E,F)))). fof(th_varignon,conjecture,(! [A,B,C,D,E,F,G,H] : (( (~(col(B,D,A) )) & (~(col(B,D,C))) & (~(col(A,C,B))) & (~(col(A,C,D))) & (( col(E,F,G))) & midpoint(A,E,B) & midpoint(B,F,C) & midpoint(C ,G,D) & midpoint(A,H,D)) => pG(E,F,G,H) ))).

  00 seconds: Consider arbitrary a, b, c, d, e, f , g, h such that: -¬col(b, d, a), -¬col(b, d, c), -¬col(a, c, b), -¬col(a, c, d), -¬col(e, f, g), b ̸ = d, a ̸ = c, midpoint(a, e, b), midpoint(b, f, c), midpoint(c, g, d), midpoint(a, h, d).

1 .

 1 par(a, c, h, g) (by MP, from ¬col(a, c, d), midpoint(c, g, d), midpoint(a, h, d) using axiom triangle mid par strict; instantiation:A → a, B → c, C → d, P → g, Q → h)2. par(b, d, f, g) (by MP, from ¬col(b, d, c), midpoint(c, g, d), midpoint(b, f, c) using axiom triangle mid par strict; instantiation: A → b, B → d, C → c, P → g, Q → f ) 3. par(a, c, e, f ) (by MP, from ¬col(a, c, b), midpoint(b, f, c), midpoint(a, e, b) using axiom triangle mid par strict; instantiation: A → a, B → c, C → b, P → f , Q → e) 4. par(b, d, e, h) (by MP, from ¬col(b, d, a), midpoint(a, h, d), midpoint(a, e, b) using axiom triangle mid par strict; instantiation: A → b, B → d, C → a, P → h, Q → e)

1 .

 1 par(a, c, e, f ) (by MP, from ¬col(a, c, b), midpoint(b, f, c), midpoint(a, e, b) using axiom triangle mid par strict; instantiation:A → a, B → c, C → b, P → f , Q → e)2. par(b, d, f, g) (by MP, from ¬col(b, d, c), midpoint(c, g, d), midpoint(b, f, c) using axiom triangle mid par strict; instantiation:A → b, B → d, C → c, P → g, Q → f ) 3. par(b, d, e, h) (by MP, from ¬col(b, d, a), midpoint(d, h, a), midpoint(a, e, b) using axiom triangle mid par strict; instantiation: A → b, B → d, C → a, P → h, Q → e) 4. par(a, c, h, g) (by MP, from ¬col(a, c, d), midpoint(c, g, d), midpoint(d, h, a) using axiom triangle mid par strict; instantiation: A → a, B → c, C → d, P → g, Q → h)5. par(e, f, g, h) (by MP, from par(a, c, e, f ), par(a, c, h, g), ¬col(e, f, g) using axiom lemma par trans; instantiation: A → e, B → f , C → a, D → c, E → g, F → h)[START_REF] Braun | From Tarski to Hilbert[END_REF]. par(e, h, g, f ) (by MP, from par(b, d, e, h), par(b, d, f, g), par(e, f, g, h) using axiom lemma par trans; instantiation:A → e, B → h, C → b, D → d, E → g, F → f ) 7.pG(e, f, g, h) (by MP, from par(e, f, g, h), par(e, h, g, f ) using axiom defparallelogram2; instantiation: A → e, B → f , C → g, D → h) 8. Proved by assumption! (by QEDas)

  fof(defmidpoint,axiom, (! [A,B,C] : ((midpoint(A,B,C)) => ((betS(A ,B,C) & cong(A,B,B,C)))))). fof(defmidpoint2,axiom, (! [A,B,C] : ((betS(A,B,C) & cong(A,B,B,C) ) => ((midpoint(A,B,C)))))). Consider arbitrary a, b, c, d, e, f , g, h such that: -¬col(b, d, a), -¬col(b, d, c), -¬col(a, c, b), -¬col(a, c, d), -¬col(f, g, e), b ̸ = d, a ̸ = c, midpoint(a, e, b), midpoint(b, f, c), midpoint(c, g, d), midpoint(a, h, d).

1 .

 1 midpoint(b, e, a) (by MP, from midpoint(a, e, b), midpoint(a, e, b) using axiom defmid-point2; instantiation: A → b, B → e, C → a) 2. pG(e, f, g, h) (by MP, from ¬col(b, d, a), ¬col(b, d, c), ¬col(a, c, b), ¬col(a, c, d), ¬col(f, g, e), b ̸ = d, a ̸ = c, midpoint(b, e, a), midpoint(b, f, c), midpoint(c, g, d), midpoint(a, h, d) using axiom varignon th; instantiation:A → a, B → b, C → c, D → d, I → e, J → f , K → g, L → h)3. rectangle(e, f, g, h) (by MP, from pG(e, f, g, h), cong(e, g, h, f ) using axiom defrect-angle4b; instantiation: A → e, B → f , C → g, D → h)[START_REF] Bezem | Automating Coherent Logic. 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning -LPAR 2005[END_REF]. rectangle(e, f, g, h) (by MP, from rectangle(e, f, g, h), rectangle(e, f, g, h), rectangle(e, f, g, h), rectangle(e, f, g, h) using axiom defrectangle2e; instantiation:A → e, B → f , C → g, D → h)5. Proved by assumption! (byQEDas) 7.4 Problem 4: Partially Specified Goal The list of axioms used for Problem 4 is the same as presented in Section 7.1. Only the conjecture is different: the goal does not have the predicate symbol specified: fof(th_varignon,conjecture,(! [A,B,C,D,E,F,G,H] : (( (~(col(B,D,A) )) & (~(col(B,D,C))) & (~(col(A,C,B))) & (~(col(A,C,D))) & (( col(E,F,G))) & (B != D) & (A != C) & midpoint(A,E,B) & midpoint(B,F,C) & midpoint(C,G,D) & midpoint(A,H,D)) => _(E,F, G,H) ))).

  ¬col(b, d, a), -¬col(b, d, c), -¬col(a, c, b), -¬col(a, c, d), -¬col(e, f, g), b ̸ = d, a ̸ = c, midpoint(a, e, b), midpoint(b, f, c), midpoint(c, g, d), midpoint(a, h, d).

1 . 4 .

 14 par(a, c, e, f ) (by MP, from ¬col(a, c, b), midpoint(b, f, c), midpoint(a, e, b) using axiom triangle mid par strict; instantiation: A → a, B → c, C → b, P → f , Q → e) 2. par(a, c, h, g) (by MP, from ¬col(a, c, d), midpoint(c, g, d), midpoint(a, h, d) using axiom triangle mid par strict; instantiation: A → a, B → c, C → d, P → g, Q → h) 3. par(e, f, g, h) (by MP, from par(a, c, e, f ), par(a, c, h, g), ¬col(e, f, g) using axiom lemma par trans; instantiation: A → e, B → f , C → a, D → c, E → g, F → h) Proved by assumption! (by QEDas) 7.5 Problem 5: Partially Specified Proof

Notice the hidden link between the formulae Bi(⃗ a, ⃗ b) from the rule MP and the formula ax: the formulae Bi(⃗ a, ⃗ b) from the rule are instances of the formulae Bi(⃗ x, ⃗ y) from ax.

https://github.com/janicicpredrag/Larus

The corresponding C++ implementation is an improved version of the implementation presented earlier[START_REF] Janičić | Theorem Proving as Constraint Solving with Coherent Logic[END_REF].

Actually, underspecified arguments can be also handled using existential quantification.

Acknowledgement. The work related to this paper has been partially supported by the European Cost project CA20111 EUROProofNet.


Jean-Michel Le Que´re´a
email: jean-michel.lequere@rennes.inra.fr

Franc -Ois Husson

Catherine M G C Renard

Jo Primault

French cider characterization by sensory, technological and chemical evaluations

Keywords: Alcoholic beverages, Fermented products, Analytical data, Food composition, Multivariate analysis

A set of 90 ciders among them 50 ''brut'' (near dry), 30 ''demi-sec'' (half dry) and 10 ''doux'' (sweet) were collected and analysed to get a data base of about 180 variables including processing conditions, sensory descriptors and physicochemical variables. This data set was treated by a multiple factor analysis (MFA) using the sensory and analytical data as active variables whereas the ''processing conditions'' data were introduced as illustrative variables. Two MFAs was carried out separating the less sweet (''bruts'') from the sweeter (''demi secs'' and ''doux'') ciders. For both sets, the MFAs showed a strong polarization of the ciders characteristics: fruity/flowery flavours are associated with cooked flavours and opposed to the descriptors ''animal'' (animal), ''sous-bois'' (underwood), ''fond de cuve'' (vat dregs) themselves associated with bitterness and astringency and also ''pomme/cidre'' (cider/apple) flavours. The industrial ciders located on axis 1 near the fruity and cooked odours whereas the ciders of small scale producers were close to the second group of flavours and tastes.

Introduction

The differentiation labels that were created these last 10 years show that the cider makers want to segment their market. Because a commercial differentiation is more effective if it is supported by a perceptible difference, the first step for creating such a differentiation may be to estimate what differences can be perceived among the existing ciders both by sensorial and physicochemical analysis. The second step is to find the methods to produce reliably these different products.

From a theoretical point of view, sensorial perceptions are due to the physicochemical composition of ciders. A lot of work in beverages deals with the sensorial effect of the composition especially in wine and beer, some of its conclusions may be extrapolated to ciders.

Fruity flavours are mainly due to hexyl acetate, ethyl caprilate and isoamyl acetate while 2-phenylethyl acetate is both fruity and flowery [START_REF] Rapp | Wine aroma[END_REF]. Fruity aroma does not mean ''coming from the fruit'': most of these compounds are synthesized during fermentation [START_REF] Williams | The volatile aroma components of fermented ciders: Minor neutral components from the fermentation of sweet Coppin apple juice[END_REF], especially by some secondary yeasts that can produce high amount of acetate esters [START_REF] Inoue | Roles of esterase and alcohol acetyltransferase on production of isoamyl acetate in Hansenula mrakii[END_REF][START_REF] Rojas | Acetate ester formation in wine by mixed cultures in laboratory fermentations[END_REF]. Most of the higher alcohols have perception thresholds higher than their concentrations but they are linked with fermentation conditions and can be regarded as indicators. Some compounds like phenylethanol are sensory active having a rose-like flowery aroma. The vinyl and ethyl phenols, when present at high concentrations, are usually considered as off-flavours of alcoholic beverages especially ethyl phenols. They occur during or after fermentation and are produced by bio-transformation of hydroxycinnamic acids [START_REF] Chatonnet | Synthesis of volatile phenols by Saccharomyces cerevisiae in wines[END_REF][START_REF] Chatonnet | Influence of polyphenolic components of red wines on the microbial synthesis of volatile phenols[END_REF]. A particular yeast, Brettanomyces, seems to be the main responsible for the production of ethyl phenols via vinyl phenol [START_REF] Dias | Factors affecting the production of 4-ethylphenol by the yeast Dekkera bruxellensis in enological conditions[END_REF].

In cider bitterness and astringency are due to the polyphenols especially procyanidins which are polymers of catechins [START_REF] Lea | The phenolics of ciders: Bitterness and astringency[END_REF][START_REF] Noble | Astringency and bitterness of flavonoid phenols[END_REF]. The degree of polymerization (DP) is the main factor that influence the ratio between the two sensations [START_REF] Lea | The phenolics of ciders: Bitterness and astringency[END_REF][START_REF] Lea | Bitterness and astringency: The procyanidins of fermented apple ciders[END_REF]: small procyanidins (up to DPn 4) are rather bitter and higher (DPn 5-9) are rather astringent but both sensations are usually associated. There is often an interaction [START_REF] Vidal | Use of an experimental design approach for evaluation of key wine components on mouth-feel perception[END_REF] with other constituents of the beverage: alcohol and polysaccharides reduce astringency while pH can increase it without changing the bitterness [START_REF] Kallithraka | Red wine and model wine astringency as affected by malic and lactic acid[END_REF]. Sugars are also known to reduce acidity [START_REF] Leguerinel | Essai d'e´valuation des caracte´ristiques organoleptiques des cidres par analyses instrumentales[END_REF] and bitterness.

To understand and reliably reproduce these effects of composition on sensorial characteristics their causes must be identified. The composition may, in particular, be linked to fruits production and/or processing conditions. Some of the process conditions clearly can modify the composition of cider. Juice extraction usually begins by pressing and, for some ciders, this first step is completed by water extraction in a reverse-current extractor which will dilute the juice to some extent. French cider may also be partly made by fermenting a dilution of juice concentrate (authorized up to 50% of the total sugar involved) which might bring compounds and/or flavours usually generated by heat treatments.

Juice and cider can also be clarified and one of the clarification treatment consist in adding gelatine (''Collage'' in French). This treatment can be used either on the juice before fermentation or on cider before bottling. By removing selectively high DP procyanidins this treatment modifies both the total tannin content and the profile of the residual tannins, and thus may change the composition and the taste [START_REF] Lea | Bitterness and astringency: The procyanidins of fermented apple ciders[END_REF][START_REF] Maury | Influence of fining with different molecular weight gelatins on proanthocyhanidin composition and perception of wines[END_REF]. But the most common clarifying method in French cider making is the keeving process which use endogenous pectin as a clarifying agent: after demethylation [START_REF] Baron | Utilisation de la pectineste´rase dans les industries cidricoles[END_REF] of the pectin by an enzyme-the pectinemethyesterase-calcium is added to induce a formation of a calcium pectate gel that includes all particles of the cloudy juice. This gel is then separated by a ''natural'' flotation due to CO 2 bubbles of the beginning fermentation. This process produces a pectin-free clarified juice [START_REF] Lea | Cidermaking[END_REF] with a reduced nitrogen amount and results in slower fermentation and better stabilization.

French cider fermentation is usually conducted without yeast pitching and at temperatures from 5 to 20 1C depending on the season and the equipment of the cider maker. These low temperatures may have a significant effect on the metabolism of yeast strains spontaneously present, and later on the growth of lactic acid bacteria and Brettanomyces species. At the beginning of the fermentation most of the small cider makers and farmers proceed to one or more biomass reductions (performed by filtration or centrifugation and usually followed by a new yeast growth) to deplete the cider in nutrients, slow the fermentation and keep residual sugars. When such a nutrient depletion is achieved, the growth of micro-organisms is very limited and the ciders can be commercialized without pasteurization. But ciders can also be prepared by blending dry ciders with juice, concentrated juice or partly fermented cider. This kind of cider must then be pasteurized. Cider are commercialized as sparkling beverages and two methods are used for carbonating: Farmers usually bottle a cider that contains enough yeasts to produce up to 5 g/l CO 2 in the bottle whereas most of the other cider makers dissolve exogenous carbonic gas in the cider before bottling. Oxygen can be introduced during bottling (unpublished results) and can then oxidize some compounds and modify the flavour. This can be at least partially reversed by oxygen consumption by yeasts when present in bottle (unpasteurized cider) or by addition of antioxidant (SO 2 and ascorbic acid).

With so many different options possible, cider can be expected to be quite variable even when starting from the same apples. The relations between processing method, composition and sensorial perception are not easy to establish but the three kinds of data must be observed together to characterize the diversity of ciders. Such a data set may be also useful to know the actual composition of French ciders and then to observe the correlation between the different data as a first approach to a better causality understanding.

This data set was analysed by a multiple factor analysis (MFA) [START_REF] Escofier | Analyses factorielles simples et multiples; objectifs[END_REF] to extract the main global information and to determine the main associations that can be observed between the different groups of variables (sensorial, physicochemical and process conditions).

Material and method

Sample collection

To reach the fixed objectives the chosen ciders had to be as diverse as possible to describe the French cider diversity rather than to be representative of the production volumes. We asked a panel of 100 cider producers the processing conditions for 291 ciders. This was submitted to cluster analysis to constitute groups of ciders that could be considered as homogeneous for their process conditions. Ciders were chosen (Table 1) within those groups but without proportionality: as the smaller groups were also sampled these groups are over represented.

Processing conditions

They were collected by asking the producer to fill a form in which we had identified the process step that are known to modify the sensory perception or the physicochemical composition or which are indicators of a particular process method even if their effect is not known. The production scale (three classes: Farmer, Small cider maker, Industrial) was determined afterward on the basis of the volume of produced cider. Table 2 summarizes the variables that were asked and the possible answers.

Sensory analysis

In this study the sensory analysis excluded hedonic and visual appreciation. The 14 panellists were used to taste different foodstuffs and had been trained for ciders and cider apple juice evaluation (according to NF ISO 8586-2). Before this study, 10 specific training sessions were performed by tasting commercial ciders in order to generate sensory descriptors (listed in Table 3) and to get the best agreement between the assessors for these descriptors. The terms given in Table 3 are translations of these descriptors, some of them being difficult to translate: we use the term ''underwood'' for the French ''sous-bois'' to describe the humid, mouldy smell of the soil of a forest covered with decaying leaves. The same descriptors were used both for odour and flavour. Tests were performed in individual booths under red light; ciders were served at 10-12 1C in dark glasses. The assessors were asked to score the selected sensory descriptors before tasting (odour descriptors) and after tasting (flavour descriptors), by means of a linear scale from 1 to 10. Not detected attributes were scored as 0.

The ciders were kept at À5 1C from their sampling to their tasting. Designs to balance the effect of order of presentation and first-order carry-over effects were used throughout the sessions [START_REF] Mc Fie | Designs to balance the effect of presentation and first-order carry-over effects in hall tests[END_REF]. This allows avoiding confusion between session, assessor, product and presentation rank effects. The panel evaluated each sample in duplicate. Five ciders were tasted in each session; the experiment was performed in 36 sessions during 6 months.

Physicochemical data

Table 4 indicate the physicochemical variables witch were used in the statistical treatment.

The different polyphenolic compounds are determined by HPLC analysis after thiolysis according to [START_REF] Guyot | Direct thiolysis on crude apple materials for high-performance liquid chromatography characterization and quantification of polyphenols in cider apple tissues and juices[END_REF]. The degree of polymerization of flavan-3ols is determined by the ratio between extension units and terminal units.

Volatile compounds were analysed using GC with flame ionization detection. They are extracted by a method derived from (Hubert, Brunerie, Le Que´re´, & Drilleau, 1990) using ''Chemelut'' column (Grosseron) instead of Helium is used as carrier gas at 2 ml/min.

Methanol and ethanol are determined by GC after distillation according to [START_REF] Oiv | Recueil des me´thodes internationales d'analyse des boissons spiritueuses, des alcools et de la fraction aromatique des boissons[END_REF].

Sugars (glucose, fructose and sucrose), glycerol and sorbitol, L-malic, L-lactic, D-lactic and citric acid are determined by enzymatic assays of Boehringer Mannheim/R-Biopharm (R-Biopharm AG Landwehrstr. 54 D-64293 Darmstadt) according to producer specifications.

The colour parameters-Hue, Value and Chroma-are measured by a Minolta spectrophotometer CM 3600d (Minolta Co. Ltd, 3-13, 2-Chome, Azuchi-Machi, Chuo-Ku, Osaka 541, Japan) on centrifuged (7500g 15 min) and filtrated (Analypore Labosi-cellulose ester membrane-0.45 mm) cider. As some ciders darken when treated, the parameters are measured on both oxidized (aerated for 1 h) and reduced cider (by adding 0.4 g/l of sodium dithionate before measure). Browning capacity of the ciders is evaluated by the geometrical distance between the colour parameters of oxidized and reduced ciders. Turbidity is measured by WTW Turb-550 IR according to producer specifications.

Total residual nitrogen is analysed by Hach method [START_REF] Hach | A powerful Kjeldahl nitrogen method using peroxymonosulfuric acid[END_REF] for digestion and Berthelot/salicylate method for ammonia determination.

Biochemical analysis usually determined on wine and cider are determined according to (Afnor, 1989): volatile acidity by distillation and titration, total acidity by titration, alcohol by distillation and density measurement. Density of ciders and distillate was measured by a PAAR densimeter DMA 58 (Anton-Paar-Str. 20 A-8054 Graz, Austria) according to producer specifications.

Sulfates are determined gravimetrically according to NF V76-109 and total bisulfites by a sequential analyser using 5, 5 0 -dithio-bis-(2-nitrobenzoic acid) known as Ellman's reagent.

Minerals were determined by atomic absorption. Among them only Ca and Cu were used in statistical treatment. Samples were mineralized and atomized in the flame of the atomic absorption spectrometer (Varian SectrAA 220 FS) with modifiers for Ca. Concentrations were derived from the measures at the adapted wave length using external standards calibration curve.

Statistical analysis

The final data base is made of three groups of variables: The first group contains the sensory descriptors (among them 21 flavour, 21 odour, 5 taste descriptors). The second group is constituted by most of physicochemical variables (53 of the volatile compounds and 34 of the other biochemical compounds). Some variables are calculated variables (total sugars, the advancement of malolactic fermentation which is the percentage of malic acid transformed in lacic acid) and some variables that were initially included in the data base were eliminated because of their low variability (especially mineral compounds and minor phenols). The third group is constituted by the ''processing conditions'' (31 qualitative variables that include raw material, juice preparation, fermentation, cider preparation and finning, carbonation, cider category and date of sampling.

In order to simultaneously analyse sensory and physicochemical variables, we apply MFA on the data set which merges sensory and physicochemical variables. MFA allows to balance the role of the two sets of variables in a global analysis and gives visualization tools and specific indices of the grouping structure. Moreover, since MFA balances the data sets, it allows to simultaneously study quantitative and qualitative data sets: each quantitative data set is studied as PCA and each qualitative data set is studied as multiple correspondence analysis. A more complete description can be found in several papers devoted to MFA [START_REF] Escofier | Analyses factorielles simples et multiples; objectifs[END_REF][START_REF] Page`s | Inter-laboratory comparison of sensory profiles: Methodology and results[END_REF][START_REF] Page`s | Multiple factor analysis with confidence ellipses: A methodology to study the relationships between sensory and instrumental data[END_REF].

The first two groups (the sensory and the physicochemical) form the active variables of the MFA and the third group (the ''processing conditions''), is introduced in MFA as illustrative data.

Results and discussion

Two MFA were performed on two separate sets of ciders: set A contains the ciders called ''bruts'' (less than 28 g/l of residual sugar) and set B gathers the two others categories ''demi-sec'' (between 28 and 42 g/l of residual sugar) and ''doux'' (less than 3% vol. alcohol and more than 35 g/l of residual sugar).

For the set A of 50 ciders ''bruts'', factors 1 and 2 represent, respectively, 23.3% and 9.5% of the inertia. For the set B of 40 ''demi-secs'' and ''doux'' factors 1 and 2 represent, respectively, 25.4% and 11.9% of the inertia. These inertia can be regarded as high with such a number of variables. For both sets the next dimensions represent less than 6% and will not be used to describe our data.

Each variable was given a code (Tables 234) which is used on MFA figures. For the variables the more correlated with the axis 1 and 2 (distance from centre of the figure greater than 0.5) the complete names are written, except for volatile compounds (Fig. 2), too numerous to give the complete name. As it is difficult to read all the variables on the same graph, the active variables were divided in different categories to examine them sequentially. The maps result from the MFAs carried out with all the data; the only difference between the figures is which data are shown. Sensory data will be examined first on one figure (Fig. 1) and physicochemical variables are projected on two figures (Figs. 2 and3). For the same reasons the illustrative data are projected on three figures (Figs. 456).

Sensory descriptors

Sensory descriptors were classified into seven categories: the two main categories are fruity/floweryflavours (Fff) and a group of descriptors we called heavy flavours (Hvf) according to [START_REF] Chatonnet | Synthesis of volatile phenols by Saccharomyces cerevisiae in wines[END_REF]. Two other groups can be easily formed by the taste/mouthfeel descriptors (Tst) and the ''heated'' flavours (Hf). Although the other flavours are more difficult to classify they were arranged in three categories: Vegetal (Vf), Fermented (Ff) and Vinegar/ solvent flavours (Vsf).

Fig. 1(A) and (B) presents sensory data. It can be noted first that the paired descriptors (similar descriptors for odour and flavour) usually show coherent positions on axis 1 but often with an offset on axis 2.

There is a strong polarization of sensory characteristics for both sets of ciders: on the left of the graphs (negatively correlated to factor 1) we find the fruity and flowery flavours such as ''fruity'', ''apple/fruit'', ''exotic fruits'', ''vanilla'', ''flowery''. However these fruity flavours are associated with some other terms like ''cooked apple'', ''caramel'' that reminds us that ciders can be heated and also with ''butter'', a descriptor that is common in fermented beverages. These first groups of flavours are opposed to ''animal'', ''vat dregs'', ''underwood'', ''woody'' that can be called ''heavy flavours''. However, this group of variables, positively correlated with factor 1, is also associated with ''cider apple'' that can be considered as a specific fruity flavour of cider. The two sets of ciders show very similar results concerning axis 1. However the flavour opposition is more involved in the definition of axis 2 for set B.

Bitter and astringent tastes present also a positive correlation with factor 1. These tastes are situated near the heavy flavour indicating that the probability to find these flavours is higher in bitter ciders.

Physicochemical data

Fig. 2(A) and (B) shows the projection of the volatile compounds. Among them, the esters are often considered as responsible of the fruity flavour and might explain the observed sensorial polarization. Our data are not exactly what could be expected: some of the esters known for their fruit-like flavour, such as isoamyl acetate, hexyl acetate and ethyl isovalerate, (Fig. 2A) present a slight negative correlation with factor 1 that places them on the left of the graph with the fruity flavours. However, most of the esters are not on the left part of axis 1 and the circle that reminds of the fruity descriptors remains empty especially in Fig. 2B: on the contrary, a lot of the esters and of the other volatile compounds such as phenylethanol known for its flowery flavour are positively correlated with factor 1. They also can present a positive or negative correlation with factor 2 that place them on top or at the bottom of the graph. Among volatile compounds one of the sulfur compounds, methionol (Ooc in Fig. 2), is also positively correlated with factor 1.

Some other sensory variables can also be associated with their related analytical data: heavy flavours are close to volatile phenolic compounds (Fig. 3) especially 4-ethylguaiacol. Another volatile phenolic compound, p-ethylphenol, is also positively correlated with factor 1 but also with factor 2. It can be remarked that methionol is situated near the volatile phenols. This could be linked to a confusion between its flavour and those of volatile phenols, so that it might contribute to ''heavy'' flavours.

For bitter and astringent tastes there is also a logical association with polyphenols especially with procyanidins and their degree of polymerization (DP): procyanidins of apple are known to be both bitter and astringent [START_REF] Lea | Bitterness and astringency: The procyanidins of fermented apple ciders[END_REF]. Most of the phenolic compounds are correlated with axis 1 and are strongly correlated together. This correlation between all the phenolic compounds is usually observed in apple juice composition, i.e. apple juices which are high in polyphenols are high in all polyphenols with only minor variations of the proportions of the various classes. This probably explains why volatile phenols/heavy odour are associated with procyanidols/bitter-astringent: hydroxycinnamic acids, the substrates of volatile phenols synthesis are also statistically higher in bitter ciders.

Some technological consequences (Fig. 3) can also be correlated with factor 1: residual nitrogen and furfural are situated on the left side of the graph close to the sensory descriptors ''cooked apple'' and ''caramel''. This can be explained by the method used to obtain stability. French ciders contain enough residual sugars for bacteria or yeast growth after bottling. The most definitive solution (used for most of industrial ciders) to prevent these damages is to pasteurize the bottled cider between 50 and 60 1C and the second method (mainly used at small scale), consists in exhausting the nutrients, especially nitrogen, by several cycles of yeast growth. The presence of residual nitrogen thus indicates that the first solution was necessarily adopted, and it is therefore logical to find furfural, which is generated during heat treatments from sugars, near residual nitrogen. The sensory descriptors ''cooked apple'' and ''caramel'' might be a sensory result of this treatment.

Sulfates are also present in the same place and can be explained by an oxidation of sulfites during cider processing. This reaction will take place when cider is left for a long period without fermentation or after bottling.

On the other side of the graph the variable ''total alcohol'', often used by French cider makers, is correlated with factor 1. This variable is calculated as the addition of analysed alcohol and the potential alcohol resulting from calculated conversion of residual sugars (17 g/l for 1% vol.). The position of this calculated variable on the right part indicates that this side concerns ciders that are made from juices richest in sugars, i.e. not diluted juice.

Processing conditions

The processing conditions are projected on the first two axes (Figs. 456) as illustrative variables.

The fruit production conditions (Fig. 4) include the type of apples, the type of orchard and harvest but most of the terms that appear on the graph concern the production area-region and micro-region-because answer to this question was an open list. On the left of the graph the answers ''with dessert apple'', ''non-specific region'', ''non-specific micro-region'' are the most negatively correlated with factor 1. These answers show that the production area cannot be defined with such a precision for the left side ciders, which is a characteristic associated with industrial ciders. On the right side there are a lot of micro regions. Such a precise origin (and manual harvesting methods) can only be at small scales.

Among the methods of juice preparation and cider fermentation and finning (Fig. 5) located on the left of axis 1 we can remark the clarifications by gelatine treatment of juices and ciders, and the use of concentrated juice both in juice and in cider. These technological choices are usually specific of industrial scale.

The terms related to carbonation and ciders categories are less correlated with the two axis: the term ''carbonation in tank'' is used by industrial and small cider makers but only three ciders were concerned. For the commercial differentiation terms, terms such as ''IGP Normandie'' (Fig. 6B) that is only used at industrial scale was situated on the left side for set B, while the French origin certification ''AOC'' which is only used by farmers appeared (Fig. 6A) on the right side for set A only.

As these projections of illustrative variables strongly suggested that the sensory and physicochemical classification may be linked to processing scale, we examined the occurrence of the main processing conditions in the different scales of cider. We can see (Table 5) that the smaller production scales are usually characterized by a negative answer for most of possible techniques, carbonation being the main difference between farmers and small cider makers. The other technical operations are mainly used at industrial scale. In this study it is thus impossible to distinguish the role of each of these ''industrial'' operations on the polarization shown by FMA.

Ciders positions

The projection of the ciders on the graph defined by the two first dimensions (Fig. 7) confirms the above observations: the left side concern industrial ciders and the right the ciders produced by small cider makers and farmers. The ellipses are only drawn to indicate each cider maker family without any statistical signification. The center of the graph presents an overlapping of the three scale of ciders makers. Because the processing methods are not homogeneously used by the different families of cider makers, it is not possible to draw any hypothesis from this work concerning the effect of these different methods. The link between processing scale and the sensorial and analytical classification is the only conclusion that can be drawn. As the contribution of sensorial and physicochemical data are balanced for the first dimension in MFA, we can say that the industrial ciders present both a different sensorial perception and a different composition from the two types of small scale ciders; these two last categories remaining undifferentiated. As this observation was done ''bruts'' and B ''sweeter'') this result seems to be robust.

Global discussion

The industrial scale ciders could be differentiated from smaller scales ciders both on a sensory and an analytical basis with however a continuous gradation between these two extremes. The first dimension which highlight this differentiation explains enough of the total inertia to be highly significant with such a number of variables.

This differentiation of the ciders can be explained first by a strong polarization of sensory perceptions: two groups of flavours, the ''fruity/flowery'' flavours and the ''heavy flavours'', respectively, present a negative and a positive correlation with factor 1. To this polarization can be added bitter taste, astringent mouthfeel and also a specific fruity flavour ''cider apple'', which are associated with the ''heavy flavours''. On the other hand some flavours such as ''caramel'' and ''cooked apple'' which are usually attributed to heat treatments, are associated with the ''fruity/flowery'' flavours.

Among the analytical data some compounds can explain the sensory polarization: procyanidins, which are known to be responsible for bitterness and astringency, and volatile phenols which are considered responsible of some of the ''heavy flavours'' are actually close to the correspondent descriptors. The presence of furfural can also be related to heat treatments and then to the cooked flavour while high residual nitrogen indicates the necessity of this treatment in the concerned ciders.

The relation between esters and fruity flavour is less clear: isoamyl acetate, hexyl acetate and ethyl isovalerate are slightly (negatively) correlated with factor 1 close to fruity flavour but, factor 1 is also positively correlated with a lot of esters and only one fruity descriptor, ''cider apple'' is close to these volatile compounds. This suggest that the fruity flavours may be disguised by the presence of ''heavy flavours'' when these flavours are high enough and that the perception of fruity flavours in the left side ciders is explained more by the absence of ''heavy flavours'' than by the presence of related compounds.

The specific variable ''total alcohol'', often used by cider makers and which gives an indication of the initial sugar concentration of the juice, is also positively correlated with factor 1 indicating that the small scale ciders are not or less diluted than the industrial ciders. The relation between low ''total alcohol'' and fruity flavours (or between heavy flavours and high ''total alcohol'') may appear surprising. In fact, as the technological methods are not independent of the production scale, this higher initial density of the juice cannot be separated from the first differentiation we discuss about: industrial ciders characterized by fruity, flowery, and cooked flavour are also the more diluted because partially made from water-extracted juice whereas small scale ciders, characterized by heavy flavour bitterness and astringency usually are pure juice.

Conclusions

All these observations show the complexity of the differentiation associated with axis 1: on the industrial side more diluted ciders that are perceived by the panel as fruity but also as heated products. On the other side more ''concentrated'' ciders that are also more bitter and astringent but with ''heavy flavours'' that are often considered as off flavours in the other beverages. A possible interaction between these ''heavy flavours'' and fruity/flowery might be examined to better understand the signification of this polarization.

This work cannot explain the relations between the different variables but it can be used to formulate some hypotheses from their positions. The characteristics which were perceived as different by the assessors were notably the heavy and fruity flavours and also bitterness and astringency. The main observation is that the methods chosen by industry give ciders that are different from those made by the methods chosen by the smaller scale cider makers for these characteristics. We were limited by the non-independence of the processing conditions. Experimental studies will have to be performed to identify within this succession of choices that constitute each technological path which points efficiently modify these characteristics. However, some of the processing conditions used at industrial scale can be identified to be examined first: finning with gelatine at the two steps where it can be used because of the reduction of phenols contents, heat treatments in relation with nutrients depletion, and fermentation temperature because of the control of microbial alterations.

'

  'Extrelut'' column (Merck) for solvent extraction. Injections are made in split mode ð 1 20 Þ on a capillary column of 50 m, 0.25 i.d. coated with a 0.20 mm film of polyethyleneglycol (CP-WAX 57-CB-Chrompack Varian). Oven temperature program: 35 1C (5 min); 35-55 1C (31/min); 55 1C (3 min); 55-105 1C (41/min); 105-120 (21/min); 120-200 (71/min); 200 (12 min); 200-225 (1.51/min).

Fig. 1 .

 1 Fig. 1. Projection of sensorial data for A and B set of ciders on the two first factors. The ellipses are manually drawn and show the positions of the main groups of sensory characteristics (& Tastes (Tst)-J Heavy flavours (Hvf)-Flowery/fruity flavours (Fff)-B Heated flavours (Hf)-Ṽ egetal flavours (Vf)-m Fermented flavours (Ff)-n Vinegar/solvent flavours (Vsf)).

Fig. 6 .

 6 Fig. 6. Projection of cider categories cider sampling and carbonation conditions as illustrative variables on the two first factors for sets A and B (n Sampling (SP)-J Cider categories (CC)-~Carbonation (CB)).

Table 3

 3 Sensory descriptors used to characterize the ciders

	Class Variables	Code
	Flowery/fruity flavours (Fff)
	Flowery A	Fff-1a
	Flowery O	Fff-1o
	Fruity A	Fff-2a
	Fruity O	Fff-2o
	Exotic fruits A	Fff-3a
	Exotic fruits O	Fff-3o
	Cider apple A	Fff-4a
	Cider apple O	Fff-4o
	Apple fruit A	Fff-5a
	Apple fruit O	Fff-5o
	Vanilla A	Fff-6a
	Vanilla O	Fff-6o
	Heavy flavours (Hvf)
	Animal A	Hvf-1a
	Animal O	Hvf-1o
	Woody A	Hvf-2a
	Woody O	Hvf-2o
	Vat dregs A	Hvf-3a
	Vat dregs O	Hvf-3o
	Medicinal/chemical A	Hvf-4a
	Medicinal/chemical O	Hvf-4o
	Underwood A	Hvf-5a
	Underwood O	Hvf-5o
	Tastes (Tst)
	Acid T	Tst-1
	Bitter T	Tst-2
	Astringent T	Tst-3
	Sweet T	Tst-4
	Texture T	Tst-5
	Heated flavours (Hf)
	Caramel A	Hf-1a
	Caramel O	Hf-1o
	Cooked apple A	Hf-2a
	Cooked apple O	Hf-2o
	Vegetal flavours (Vf)
	Straw/Hay A	Vf-1a
	Straw/Hay O	Vf-1o
	Vegetal A	Vf-2a
	Vegetal O	Vf-2o
	Fermented flavours (Ff)
	Butter A	Ff-1a
	Butter O	Ff-1o
	Mushroom A	Ff-2a
	Mushroom O	Ff-2o
	Yeasty A	Ff-3a
	Yeasty O	Ff-3o
	Vinegar/solvent flavours (Vsf)
	Calvados/brandy A	Vsf-1a
	Calvados/brandy O	Vsf-1o
	Solvent A	Vsf-2a
	Solvent O	Vsf-2o
	Vinegar A	Vsf-3a
	Vinegar O	Vsf-3o

Table 4

 4 Physicochemical data analysed on the sets of ciders

			Table 4 (continued )
			Class Variables	Code
	Class Variables	Code
			D-lactate	Iai-5
	Acetate esters (Ae)		Ethanal	Iai-6
	Amyle acetate	Ae-1	p-Ethylphenol	Iai-7
	2-Phenylethyle acetate cis-3-Hexenyle acetate Hexyle acetate Isoamyl acetate	Ae-2 Ae-3 Ae-4 Ae-5	Other biochemical variables (Obv) Copper Dihydrochalcones Flavonols	Obv-1 Obv-2 Obv-3
	Fatty acid esters (Fae) Ethyl 2-hydroxycaproate Ethyl 2-methylbutyrate Ethyl 3-hydroxybutyrate Ethyl butyrate Ethyl caprate Isoamyle caprate Isobutyle caprate Ethyl caproate Ethyl caprylate Isoamyle caprylate Ethyl isobutyrate Ethyl isovalerate	Fae-1 Fae-2 Fae-3 Fae-4 Fae-5 Fae-6 Fae-7 Fae-8 Fae-9 Fae-10 Fae-11 Fae-12	Taste effect variables (Tev) Acidity Measured alcohol DP-Flavan-3-ols Glycerin Initial L-malate Density PH Procyanidins Sorbitol Malolactic advancement Total sugars	Tev-1 Tev-2 Tev-3 Tev-4 Tev-5 Tev-6 Tev-7 Tev-8 Tev-9 Tev-10 Tev-11
	Ethyl laurate	Fae-13	Technological choice indicators (Tci)
	Isoamyle laurate	Fae-14	Total alcohol	Tci-1
	Ethyl myristate	Fae-15	Total nitrogen	Tci-2
	Ethyl oleate	Fae-16	Calcium	Tci-3
	Ethyl palmitate	Fae-17	Disulphite	Tci-4
	Ethyl propionate	Fae-18	Furfural	Tci-5
	Ethyl stearate	Fae-19	Sulphates	Tci-7
	Other esters (Oe)		Visual effect variable (Vev)
	Ethyl formiate	Oe-1	Caffeic acid	Vev-1
	Ethyl furoate	Oe-2	Caffeoylquinic acid	Vev-2
	Ethyl lactate	Oe-3	Ferulic acide	Vev-3
	Other odourous volatile compounds (Ooc) Acetoı¨ne Diacetyl Methionol Phenylethanol	Ooc-1 Ooc-2 Ooc-3 Ooc-4	p-Coumaric acid p-Coumaroylquinique acid Browning capacity Catechines Value Chroma	Vev-4 Vev-5 Vev-6 Vev-7 Vev-8 Vev-9
	Other volatile compounds (Ovc)		Hue	Vev-10
	1-Butanol	Ovc-1
	1-Octen-3-ol	Ovc-2
	1-Octen-3-one	Ovc-3
	2,3-Butanediol	Ovc-4
	2-Methyl butanol-1	Ovc-5
	Isobutyrique Acide	Ovc-6
	Allylique alcohol	Ovc-7
	Amylique alcohol	Ovc-8
	Benzylique alcohol	Ovc-9
	Isoamylique alcohol	Ovc-10
	Total high alcohols	Ovc-11
	Butanol-2	Ovc-12
	Butyrolactone	Ovc-13
	cis-3-Hexenol	Ovc-14
	Diethyl succinate	Ovc-15
	Hexanol	Ovc-16
	Isobutanol	Ovc-17
	Methanol	Ovc-18
	Propanol	Ovc-19
	Identified alteration indicator (Iai)
	4-Ethylgaı¨acol	Iai-1
	4-Vinylgaı¨acol	Iai-2
	4-Vinylphenol	Iai-3
	Volatile acidity	Iai-4

Table 5

 5 Main technological operations in cider process that might differentiate ciders, and their representation in the sets of collected ciders

	Main technological operations

Acknowledgements

This work was carried out by INRA and CTPC with support from ONIVINS and Re´gion Bretagne.

Thanks are due to S. Tisso-Le Pre`tre, M. D'Haussy, J.P. Simon, Y. Gilles, A. Lepage and industrial units quality managers for collecting data and sample.

Thanks are also due S. Sibiril and H. Guichard from ADRIA Normandie for their implication in sensorial and volatile compounds analysis.

No No No No No Fermentation in tank 1 No No No No No No