Sana Stojanović Ðurević

Julien Narboux
email: narboux@unistra.fr

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

Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry

Keywords: Automated theorem proving, Interactive theorem proving, Tarski's geometry

The power of state-of-the-art automated and interactive theorem provers has reached the level at which a significant portion of nontrivial mathematical contents can be formalized almost fully automatically. In this paper we present our framework for the formalization of mathematical knowledge that can produce machine verifiable proofs (for different proof assistants) but also human-readable (nearly textbook-like) proofs. As a case study, we focus on one of the twentieth century classics -a book on Tarski's geometry. We tried to automatically generate such proofs for the theorems from this book using resolution theorem provers and a coherent logic theorem prover. In the first experiment, we used only theorems from the book, in the second we used additional lemmas from the existing Coq formalization of the book, and in the third we used specific dependency lists from the Coq formalization for each theorem. The results show that 37% of the theorems from the book can be automatically proven (with readable and machine verifiable proofs generated) without any guidance, and with additional lemmas this percentage rises to 42%. These results give hope that the described framework and other forms of automation can significantly aid mathematicians in developing formal and informal mathematical knowledge.

Introduction

For decades, or even centuries, mathematicians have dreamed of an automated system, usable in everyday practice, that can be used as help in proving math-ematical theorems. It would be beneficial to have computer programs not only capable of proving open or very complex mathematical conjectures, but also the technical, yet non-trivial, lemmas and theorems that appear in the development of large mathematical theories. Over the past few decades, significant progress has been made in both interactive and automated theorem proving and they are nowadays used in many areas of mathematics and computer science. In this paper we explore and demonstrate the benefits of integrating interactive and automated theorem proving in the formalization of mathematical knowledge (e.g., mathematical heritage, textbooks, etc.). For that task, we use our framework that proves given theorems and generates both machine-verifiable and humanreadable, nearly textbook-like proofs. The framework uses a fragment of first order logic, known as coherent logic, as an underlying logic. It combines several approaches and tools, including resolution theorem provers, a coherent logic theorem prover, interactive theorem provers, and a set of XML tools for coherent logic (used for translation of proofs to machine verifiable proofs and to natural language).

Within our framework we use coherent logic because it is suitable for expressing many mathematical theories while allowing for the construction of natural, intuitive, human readable proofs (in the style of forward reasoning and a variant of natural deduction) [START_REF] Bezem | Automating coherent logic[END_REF]. Coherent logic is essentially the modified Horn fragment which allows having a whole disjunction of existentially quantified conjunctions of atoms within the conclusion. Coherent logic can be considered as an extension of resolution logic, but in contrast to the resolution-based proving, the conjecture being proved is left unchanged and is proved directly (refutation, Skolemization, and transformation to clausal form are not used). Proofs in coherent logic are suitable for formalization projects as they can easily be translated into the input language of different proof assistants and in a natural language form. Several authors independently point to coherent logic or similar fragments of the first order logic as suitable for expressing significant portions of standard mathematics (specifically geometry), for instance, Avigad et.al. in the context of a new axiomatic foundations of Euclidean geometry [START_REF] Avigad | A formal system for Euclid's Elements[END_REF], Ganesalingam and Gowers in the context of importance of automated generation of readable proofs [START_REF] Ganesalingam | A fully automatic problem solver with humanstyle output[END_REF], Tarski in the context of geometry [START_REF] Tarski | Tarski's system of geometry[END_REF], etc.

In this paper, we focus on one case-study -a computer supported development of the first part of a book on foundations of geometry: Metamathematische Methoden in der Geometrie, by Wolfram Schwabhäuser, Wanda Szmielew, and Alfred Tarski [START_REF] Schwabhuser | Metamathematische Methoden in der Geometrie[END_REF]. In the rest of this paper we will refer to this text as SST. This book is a culmination of a series of Tarski's axiomatizations along with a decision procedure for that theory [START_REF] Tarski | What is elementary geometry?[END_REF]. According to Beeson [START_REF] Beeson | Proof and computation in geometry[END_REF], the first part of the book has been adapted from the Szmielew's lecture notes. It also includes results from the PhD thesis of Gupta [START_REF] Gupta | Contributions to the axiomatic foundations of geometry[END_REF]. The theory is described in terms of first-order logic, it uses only one primitive object -the point, has only two primitive predicates, and only eleven axioms. This choice for our case study is motivated by the following reasons:

-The book is one of the twentieth century mathematical classics.

-The book is self-contained as all the theorems in it are provable from the set of starting axioms. -The used axioms are simple and all of them are expressed in terms of primitive notions only. -The proofs in the book are very rigorous.

-The theory developed belongs to first-order logic.

-All sentences can be expressed in coherent logic (directly or using trivial transformations) [START_REF] Tarski | Tarski's system of geometry[END_REF]. -The set of theorems in the book is well-rounded, starting from easy ones to very complex ones, forming a non-trivial, important mathematical knowledge base.

-Computer proofs of SST, using both automated theorem proving [START_REF] Quaife | Automated development of Tarski's geometry[END_REF][START_REF] Beeson | Proof and computation in geometry[END_REF][START_REF] Beeson | OTTER proofs in Tarskian geometry[END_REF] and interactive theorem proving [START_REF] Narboux | Mechanical theorem proving in Tarski's geometry[END_REF][START_REF] Braun | From Tarski to Hilbert[END_REF], have already been developed. These developments can be used as a reference point but also for guiding the search within our framework.

Our study, presented in the rest of this paper, shows that our framework can produce proofs for 37% of the theorems from chapter 1 to 12 of SST completely automatically (using all preceding theorems from the book as premises). One of the outputs of our framework is a digital version of SST, with all axioms, definitions, theorems, and generated proofs filled-in, all in a natural language form.

Overview of the paper:

We first provide some background information (Section 2); then we describe our framework that links automated theorem provers and machine verifiable proofs (Section 3); then we present its performance on a case study -Tarski's geometry (Section 4). In Section 5 we discuss related work, and in Section 6 we draw final conclusions and discuss future work.

Context

Interactive theorem proving. In all areas of mathematics and computer science, with a history of a huge number of flawed published proofs, formal, machineverifiable proofs, given in an object-level form, have been gaining more and more importance. Interactive theorem provers (or proof assistants) are trusted tools used for proving mathematical theorems in a rigorous and machine verifiable way. Many extremely complex conjectures about software correctness or mathematical theorems were proved using interactive theorem provers [START_REF] Hales | Introduction to the Flyspeck project[END_REF][START_REF] Gonthier | A machine-checked proof of the Odd Order Theorem[END_REF]. There are growing efforts to develop repositories of proved theorems (within large corpora of formalized mathematics that can be used as building-blocks in new developments), and many software tools for producing and checking formal proofs. Among the most popular theorem proving assistants nowadays are Isabelle, Coq, Mizar, and HOL-light [START_REF]The seventeen provers of the World[END_REF]. Despite many successful results, proof assistants are still not widely used by a scientific community. This may change with recent efforts aimed at bridging the gap between internal notions of a proof and the abstractions necessary to make them user friendly at a higher level. Automated theorem proving. Automated theorem provers, both general purpose (like provers based on the resolution method [START_REF] Robinson | A machine oriented logic based on the resolution principle[END_REF]) and solvers for specific firstorder theories, have reached high levels of maturity and can be used to prove (or disprove) extremely difficult or huge conjectures (involving hundreds of thousands of variables) coming from various areas of mathematics and industrial applications.

Integration of interactive and automated theorem proving. Proof arguments of automated theorem provers are not fully trusted because there can be a bug in the implementation of the prover. This problem is avoided if the prover works in conjunction with a proof assistant (which verifies the prover's outputs). Because of this, following the progress in both worlds, over the past few years much effort has been invested in combining the power of automated and interactive theorem proving: interactive theorem provers are now equipped with trusted support for SAT solving, SMT solving, resolution method, etc. These combinations open new frontiers for the application of theorem proving in software and hardware verification, but also in the formalization of mathematics and for helping mathematicians in everyday practice. Automated theorem provers can handle technical conjectures and can also reveal what axioms and lemmas are sufficient for proving some theorem. At the same time a human user, having deeper insights in the subject matter, can aid the automated theorem prover by supplying it with additional lemmas that could prove critical in the proof generation process.

One of very successful examples of cooperation between a proof assistant and an automated theorem prover is the Sledgehammer system [START_REF] Blanchette | Extending sledgehammer with SMT solvers[END_REF][START_REF] Blanchette | Automatic proof and disproof in Isabelle/HOL[END_REF]. This system works within the proof assistant Isabelle and can invoke an external resolutionbased theorem prover such as Vampire [START_REF] Riazanov | The design and implementation of Vampire[END_REF], E [START_REF] Schulz | E -a brainiac theorem prover[END_REF], or SPASS [START_REF] Weidenbach | Spass version 3.5[END_REF]. If a conjecture is successfully proved by an external prover, the list of axioms used in the proof can be passed to the resolution-based internal prover Metis (otherwise helpless, because it is not as efficient as external provers). Metis can then construct a verified proof for the given conjecture.

Readable proofs. In formalizing mathematical knowledge, apart from the issue of trusted proofs (guaranteed by proof assistants) and the issue of automation (provided by automated theorem provers), there is also an issue of readable proofs. Readable proofs (e.g., textbook-like proofs), are often not critical in fields such as software verification (although can also be useful in such areas -e.g. for proving an understandable argument why some command leads to a bug), but are very important in mathematical practice. For mathematicians, the main goal is often, instead of only a yes or no answer, a clear and intuitive proof, that serves not only as a justification, but more importantly as an explanation as well. The Intelligible semiautomated reasoning (Isar) approach to readable formal proof documents [START_REF] Wenzel | Isar -a generic interpretative approach to readable formal proof documents[END_REF] is one of the systems following this direction -Isar allows the user to express proofs in a human-friendly way, but they are still automatically verifiable by the underlying proof system.

Coherent Logic and ArgoCLP. Certain fragments of first-order logic allow automated theorem proving with a simple production of readable proofs -one of them is coherent logic. Coherent logic (CL), initially defined by Skolem, has gained new attention in recent years [START_REF] Bezem | Automating coherent logic[END_REF][START_REF] Fisher | Skolem machines and geometric logic[END_REF][START_REF] Bezem | On the mechanization of the proof of Hessenberg's theorem in coherent logic[END_REF]. It consists of formulae of the following form:

A 1 (x) ∧ . . . ∧ A n (x) ⇒ ∃y(B 1 (x, y) ∨ . . . ∨ B m (x, y)) (1)
which are implicitly universally quantified, and where 0 ≤ n, 0 ≤ m, x denotes a sequence of variables x 1 , x 2 , . . . , x k (0 ≤ k), A i (for 1 ≤ i ≤ n) denotes an atomic formula (involving zero or more of the variables from x), y denotes a sequence of variables y 1 , y 2 , . . . , y l (0 ≤ l), and B j (for 1 ≤ j ≤ m) denotes conjunction of atomic formulae (involving zero or more of the variables from x and y). For simplicity, we assume that there are no function symbols with arity greater than zero (so, we only consider symbols of constants as ground terms). The definition of CL does not involve negation. For a single atom A, its negation ¬A can be represented in the form A ⇒ ⊥, where ⊥ stands for the empty disjunction, but more general negation must be expressed carefully in coherent logic. In order to deal with negation in general, new predicate symbols are used to abbreviate subformulae. Furthermore, 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 postulated (cf. [START_REF] Polonsky | Proofs, Types and Lambda Calculus[END_REF]):

∀x(R(x) ∧ R(x) ⇒ ⊥), ∀x(R(x) ∨ R(x)).
A number of theories and theorems can be formulated directly and simply in CL. It can be proved that any first-order formula can be translated into a set of CL formulae (in a different signature) preserving satisfiability [START_REF] Polonsky | Proofs, Types and Lambda Calculus[END_REF] (however, this translation itself is not always constructive). Coherent logic is semi-decidable and there are several implemented semi-decision procedures for it [START_REF] Bezem | Automating coherent logic[END_REF]. The weakness of theorem provers for coherent logic is that they are not very efficient and cannot prove complex mathematical theorems.

ArgoCLP [START_REF] Stojanović | A coherent logic based geometry theorem prover capable of producing formal and readable proofs[END_REF] is a generic theorem prover for coherent logic, which is based on a simple proof procedure with forward chaining and iterative deepening. ArgoCLP can read problems given in TPTP form1 and can export proofs to a custom XML representation. This proof representation can further be translated, by a simple XSLT stylesheet, to Isabelle/Isar proofs, Coq proofs, and proofs in natural language (English) formatted in L A T E X or in HTML [START_REF] Stojanović | A vernacular for coherent logic[END_REF]. Here we list one theorem (4.19) from SST and its proof in natural language form (formatted in L A T E X) generated automatically by ArgoCLP and our XML tools (for better readability, ∼ = was used as the layout of the predicate cong):

Theorem 1 (th 4 19). Assuming that bet(A, B, C) and AB ∼ = AD and CB ∼ = CD it holds that B = D.

Proof:

1. It holds that bet(B, A, A) (using th 3 1). 2. From the fact(s) bet(A, B, C) it holds that col(C, A, B) (using ax 4 10 3). 3. From the fact(s) AB ∼ = AD it holds that AD ∼ = AB (using th 2 2).

Framework Description

All of the proving systems described in Section 2 have their strengths and weaknesses: proof assistants are trusted, but the level of automation within them is often low; resolution provers are automated and efficient, but they do not produce machine-verifiable or human-readable proofs; coherent logic provers are automated and can export both machine-verifiable and readable proofs, but are not efficient enough for proving complex mathematical theorems. Combining the power of these systems, we aim to produce a framework for automation of formalization of mathematical theories with all axioms and conjectures expressed in coherent logic.

The framework combines the power and features of resolution theorem provers (Vampire, E, and Spass), an automated theorem prover for coherent logic (Ar-goCLP), and a set of XML tools for dealing with proofs in coherent logic.

Given a list of axioms and theorems, proving conjectures in the presented framework work as follows:

1. The available axioms and theorems are passed (in TPTP form) to resolution based automated theorem provers. 2. The resolution provers try to prove the conjecture using the given list of axioms and theorems both in normal and in reversed order (the order of premises can have a significant impact on the proving process). If one or more resolution provers proves the conjecture, the smallest list of used axioms/theorems (returned by the resolution prover) is used for proving the conjecture again, in the same manner. This process is repeated until the list of used axioms/theorems remains unchanged between two consecutive iterations.2 3. With the obtained list of axioms, ArgoCLP prover is invoked, and (if successful) the proofs are exported in the XML form, which can further be translated to the Isar, Coq, and a natural-language form.

In the first step, the input premises can be either all axioms and theorems that precede the conjecture within a development of some mathematical theory, or some smaller set or relevant formulae. In the last step the ArgoCLP prover is used to generate machine verifiable and natural-language proofs. One could potentially construct such proofs directly from traces of the resolution provers [START_REF] Blanchette | Redirecting proofs by contradiction[END_REF], but it is not a trivial task and instead we used our prover ArgoCLP. One negative of ArgoCLP is that it may fail to prove some theorems even if the list of all axioms/theorems, that was successfully used by the resolution provers, is given.

The described framework is implemented in C++ and can be used in a wider context of building a mathematical theory -for proving a sequence of conjectures and also in completing a mathematical textbook in L A T E X form, with axioms and theorems in TPTP form, a new (completed) version can be generated with automatically generated proofs filled-in.

Case Study: Tarski's Geometry

In this section we focus on using the framework described in Section 3 on the first part of SST (the second part is concerned with metamathematical issues). Our goal is to produce readable and machine verifiable proofs of theorems from SST automatically. Just like in the Coq formalization [START_REF] Braun | From Tarski to Hilbert[END_REF], we will focus only on the theorems found in the first 12 chapters of SST that belong to plane geometry. Those chapters, covering 120 pages of the book, contain 203 theorems, while 179 of them belong to plane geometry.

Tarski's Axioms

Tarski's axioms are expressed in terms of first-order logic with equality, without sorts (only primitive objects are points, denoted by small Latin letters), and with two primitive predicate symbols: D (for congruent) and B (for between). For the use of the dominant naming scheme and better readability, we will denote points by capital Latin letters, we will denote sets of points by capital Greek letters, and we will denote the predicate symbols D and B by cong (in prefix form) and bet. We will use this notation in the following text, even when citing the original Tarski's material. Tarski's axioms are as follows (it is assumed that all axioms are universally closed):

Axiom A1 (symmetry): cong(A, B, B, A) Axiom A2 (pseudo-transitivity): cong(A, B, P, Q) ∧ cong(A, B, R, S) ⇒ cong(P, Q, R, S) Axiom A3 (cong identity): cong(A, B, C, C) ⇒ A = B Axiom A4 (construction): ∃X (bet(Q, A, X) ∧ cong(A, X, B, C)) Axiom A5 (five segments): A = B ∧ bet(A, B, C) ∧ bet(A , B , C ) ∧ cong(A, B, A , B ) ∧ cong(B, C, B , C ) ∧ cong(A, D, A , D ) ∧ cong(B, D, B , D ) ⇒ cong(C, D, C , D ) Axiom A6 (bet identity): bet(A, B, A) ⇒ A = B Axiom A7 (Pasch): bet(A, P, C) ∧ bet(B, Q, C) ⇒ ∃X (bet(P, X, B) ∧ bet(Q, X, A)) Axiom A8 (lower dimension): ∃A ∃B ∃C (¬bet(A, B, C) ∧ ¬bet(B, C, A) ∧ ¬bet(C, A, B)) Axiom A9 (upper dimension): P = Q ∧ cong(A, P, A, Q) ∧ cong(B, P, B, Q) ∧ cong(C, P, C, Q) ⇒ (bet(A, B, C) ∨ bet(B, C, A) ∨ bet(C, A, B)) Axiom A10 (euclid): bet(A, D, T ) ∧ bet(B, D, C) ∧ A = D ⇒ ∃X ∃Y (bet(A, B, X) ∧ bet(A, C, Y ) ∧ bet(X, T, Y )) Axiom A11 (continuity): ∀Φ ∀Ψ ∃A ∀X ∀Y ((X ∈ Φ∧Y ∈ Ψ ⇒ bet(A, X, Y )) ⇒ ∃B ∀X ∀Y (X ∈ Φ ∧ Y ∈ Ψ ⇒ bet(X, B, Y ))
The axiom A8 states that there are three non collinear points. This implies that the dimension of the space is at least 2.

The axiom A9 states that if three points are at the same distance of two points then they are collinear. This implies that the dimension of the space is at most 2. This is actually only a special instance of the axiom A9 which has the following general form:

Axiom A9':   1≤i<j≤n P i = P j ∧ n i=2 cong(A, P 1 , A, P i ) ∧ n i=2 cong(B, P 1 , B, P i ) ∧ n i=2 cong(C, P 1 , C, P i ) ⇒ [(bet(A, B, C) ∨ bet(B, C, A) ∨ bet(C, A, B)]
One of the beautiful features of Tarski's geometry is that the dimension of the space is controlled by only one parameter (n) in only one axiom (the one above). We will use only the instance where n = 2 (as given by axiom A9), i.e., the plane geometry.

The axiom A10 is equivalent (in the context of the other axioms) to Euclid's parallel postulate. It is used onwards from Chapter 12 of SST.

The axiom A11 (the axiom of continuity) that involves sets of points Φ and Ψ can be reformulated into a schema of first-order axioms:

Axiom A11': ∃A ∀X ∀Y ((φ(X)∧ψ(Y ) ⇒ bet(A, X, Y )) ⇒ ∃B ∀X ∀Y (φ(X)∧ ψ(Y ) ⇒ bet(X, B, Y ))
where φ and ψ are any first-order formulae with no free occurrences of A or B.

Notice that all the axioms except A11 belong to coherent logic. The axiom 11 is not used in the first 12 chapters of SST.

Gupta has shown several independence results about this axiom system [START_REF] Gupta | Contributions to the axiomatic foundations of geometry[END_REF]. Recently Timothy Makarios proposed a further simplification of this system [START_REF] Makarios | A further simplification of Tarski's axioms of geometry[END_REF]. Swapping two points in the axiom A5 allows omitting the axiom A2. All axioms are shown to be independent except the axioms A3 and A7, which remain open problems.

Expressing Tarski's Geometry in Coherent Logic

Most of the contents of SST can be simply expressed in coherent logic. In this part of the text we discuss how we formulated all the axioms, definitions, and theorems, as faithfully to the original formulations as possible. This process resulted in 238 coherent logic theorems, a slight increase from the starting 179. This process was not always straightforward and we had to make some adaptations and decisions which are described next (some of these adaptations were also used within other formalizations of SST).

Treatment of Negations. As mentioned before, in coherent logic there is no negation, so typically for every predicate symbol R there is a new predicate symbol R that corresponds to ¬R, and the following two axioms: R(x)∧R(x) ⇒ ⊥, R(x) ∨ R(x). In the concrete case of Tarski's geometry, it can be proved that this general approach can be simplified. Indeed, Boutry and Narboux have recently shown that, in the context of Tarski's axiom system, both cong(x) ∨ cong(x) and bet(x) ∨ bet(x) are equivalent to the excluded middle axiom for equality. The Coq formalization has been rebuilt since the first version [START_REF] Braun | From Tarski to Hilbert[END_REF] and it does not use excluded middle in its general form anymore. The first 12 chapters can be formalized assuming only decidability of equality and intersection of lines [START_REF] Boutry | A short note about case distinctions in Tarski's geometry[END_REF].

Treatment of Function Symbols. Apart from function symbols related to lines and planes (for instance, L(P, Q) corresponds to the line determined by two distinct points P and Q), the use of function symbols is very limited in SST and the first time that the authors use a function symbol is in Chapter 7, Definition 7.5, page 49, for the definition of the mirror image of a point: S A (P ) = P := is midpoint(P, A, P ), where is midpoint(P, A, P ) is defined as bet(P, A, P ) ∧ cong(A, P, A, P ). Function symbols are not used in coherent logic, so we use an additional predicate symbol is symmetric defined as follows:

is symmetric(P, P , A) := is midpoint(P, A, P ).

With this definition at hand, some changes in formulations of theorems (theorems 7.13, 7.15, 7.16, 7.18, 7.19) had to be made. Each time when S A (P ) is used implicitly (without stating the symmetric point), a new point P with the property is symmetric(P, P , A) has to be introduced.

The next function symbol is introduced in Chapter 10, Definition 10.1:

M (A, B) = X := is midpoint(A, X, B).
Since there is already a predicate symbol that can mimic this function, we do not need to introduce a new predicate symbol. The use of this function symbol in the following formulae is analogous to the previous one.

There is only one more function symbol -is image, defined in Chapter 10, Definition 10.3.

Treatment of Sets. Tarski aimed at building elementary geometry within first-order logic and using only one primitive sort -intuitively points. In some definitions, however, sets are used and it is not explicit what set theory or which fragment of a set theory is required. For instance, in Chapter 6, half-lines (rays) are defined in the following way (Definition 6.8, p44):

H(P A) := {X|X P A},
where A P B (intuitively: the points A and B are on the same side of the point P ) is defined as A = P ∧ B = P ∧ (bet(P, A, B) ∨ bet(P, B, A)). Also, given P and Q are two distinct points, the line L(P Q) determined by P and Q is defined (Definition 6.14, p45) as follows (col(A, B, C) is defined as bet(A, B, C)∨ bet(B, C, A) ∨ bet(C, A, B)):

L(P Q) := {X|col(P, Q, X)}.
In addition, there is a predicate Ln (p45) that corresponds to lines, used in many of the subsequent theorems:

Ln(a) := ∃P ∃Q(P = Q ∧ Ln(a) = L(P Q)).
Within our formalization, sets are not used and, instead, additional predicates (that mimic dealing with sets of points) are introduced. For instance, in our development point on line(A, X, Y ) replaces A ∈ p and is defined as follows:

3 point on line(A, X, Y ) := (X = Y ∧ col(A, X, Y ))).
Similarly, same lines(P 1, P 2, Q1, Q2), replaces p = q (for the line p determined by points P 1 and P 2, and the line q determined by points Q1 and Q2) and is defined as follows:

same lines(P 1, P 2, Q1, Q2) :=

P 1 = P 2 ∧ Q1 = Q2 ∧ point on line(P 1, Q1, Q2) ∧ point on line(P 2, Q1, Q2).
There is a number of predicate symbols introduced this way, including (r/k denotes a predicate symbol r of arity k): point on plane3p/4, point on plane2l/5, line on plane3p/5, same planes2l/8. It can be proved (using a large number of theorems from the book) that all our new predicates are equivalent to the original predicates. Proving these conjectures formally (within Isabelle) is the subject of our current work and is beyond the scope of this paper.

Coherent Form. The first 10 axioms and all theorems (179) from the first 12 chapters of SST (after the modifications described above) can be divided into the following four groups:

1. Formulae that are in the coherent logic form. As expected, most of the theorems from SST (94) are already in coherent form (which is one of the reasons why coherent logic is used). 2. Formulae that can be easily translated into the coherent logic form. Theorems from this group [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF] can easily be transformed into one or more coherent logic formulae, using the following transformations (formulae are implicitly universally quantified; A, B, C, D denote conjunctions of atomic formulae;

x is not free in A in A ⇒ ∀xB, etc.):

A ⇔ B ≡ A ⇒ B ∧ B ⇒ A A ⇔ (B ∨ C) ≡ (A ⇒ B ∨ C) ∧ (B ⇒ A) ∧ (C ⇒ A) A ⇒ (B ⇔ C) ≡ (A ∧ B ⇒ C) ∧ (A ∧ C ⇒ B) A ⇔ B ∧ (C ∨ D) ≡ A ⇔ (B ∧ C) ∨ (B ∧ D) A ⇒ (B ∧ (C ⇒ D)) ≡ (A ⇒ B) ∧ (A ∧ C ⇒ D) A ⇒ ∀xB ≡ ∀x(A ⇒ B) A ⇔ ∃xB ≡ ((A ⇒ ∃xB) ∧ (∀x(B ⇒ A))) A ⇒ B ∧ ∃xC ≡ A ⇒ ∃x(B ∧ C) A ⇒ ∃ ≤1 xB(x) ≡ (∀x 1 ∀x 2 (A ∧ B(x 1 ) ∧ B(x 2 ) ⇒ x 1 = x 2 )) A ⇒ ∃ =1 xB(x) ≡ (A ⇒ ∃xB(x)) ∧ (∀x 1 ∀x 2 (A ∧ B(x 1 ) ∧ B(x 2 ) ⇒ x 1 = x 2 ))
3. Formulae that can be reformulated to fit into the coherent logic form. Typically, most of the theorems from this group (48) involve predicates that correspond to the sort line and deal with lines as sets of points and hence need (simple) reformulation. There is only one definition (Definition 8.11) that needs other type of reformulation (a and a are lines, per(U, X, V ) holds if the angle U XV is the right angle):

a ⊥ X a := X ∈ a ∧ X ∈ a ∧ ∀U ∀V (U ∈ a ∧ V ∈ a ⇒ per(U, X, V )).
The first step in the transformation is formulation in terms of pairs of points (instead of lines) and elimination of inner universal quantifiers (∀U ∀V ), based on a geometric property:

perp in(X, A, B, C, D) := (A = B ∧ C = D ∧ X ∈ lineAB ∧ X ∈ lineCD∧ ((A = X ∧ C = X ∧ per(A, X, C)) ∨ (A = X ∧ D = X ∧ per(A, X, D))∨ (B = X ∧ C = X ∧ per(B, X, C)) ∨ (B = X ∧ D = X ∧ per(B, X, D)))).
The above definition is then transformed (as described above) into eight coherent logic formulae, one of which is (written in TPTP form): Transformations like the above may introduce complex definitions, and obviously there is some trade-off between readability on one hand and using coherent form and avoiding using sets on the other. Still, the above ad-hoc transformation allows us to have more readable proofs than had we used a general encoding algorithm of first order logic into coherent logic as the one presented in [START_REF] Bezem | Automating coherent logic[END_REF] which would have created a number of auxiliary predicates. 4. Formulae that involve n-tuples (for arbitrary n). We treated the theorems from this group (5) only as special cases for n ≤ 2.

TPTP Form. The TPTP format 4 [31] supports first order logic and since coherent logic is a fragment of first order logic, the transformed Tarski's formulae (axioms and theorems) can be directly written in the TPTP form.

The list of all axioms, definitions, and theorems, used in our development (with information on kinds of formula and on matching with theorems from SST and from the Coq development) is available online. 5

Consistency of the Development

In developing a formalization of a mathematical theory, proof assistants ensure (to a very high degree) that proof derivations are correct, but the sole responsibility for the formulations of the axioms is on the human side. A human can unfaithfully formulate axioms from a mathematical theory, or can simply make a typo and make a system inconsistent. Furthermore, a human can introduce errors in definitions and theorems that could propagate and influence many theorems. For these reasons, availability of automated theorem provers can be very helpful in detecting possible inconsistencies.

While building a computer version of SST we used the resolution provers to check for inconsistencies (as a consequence of our errors) -within a given timelimit, we tried to derive ⊥ from the set of axioms and theorems. This is just a simple heuristic, but still, we discovered several errors in our formalization (most often typos or missing predicates). With that type of errors, some conjectures were not valid anymore, and, even worse, introduced inconsistencies with the axioms and theorems which led to the trivial proofs of the following theorems (because of the inconsistent premises).

Overview of the Existing Computer Developments

There are three existing computer developments of SST: one by Quaife based on automated theorem proving [START_REF] Quaife | Automated development of Tarski's geometry[END_REF], one by Beeson and Wos based on automated theorem proving [START_REF] Beeson | Proof and computation in geometry[END_REF][START_REF] Beeson | OTTER proofs in Tarskian geometry[END_REF], and one by Narboux and Braun based on interactive theorem proving [START_REF] Narboux | Mechanical theorem proving in Tarski's geometry[END_REF][START_REF] Braun | From Tarski to Hilbert[END_REF].

In his development, Quaife used the resolution-based prover Otter for proving theorems from the first five chapters of the book (his proving process took around two weeks). Beeson and Wos again used Otter (a newer version) for replaying and extending Quaife's work. By instructing Otter with "hints" and "resonators" they managed to prove all the theorems up to and including the theorem 9.6 and many key theorems up to Chapter 12 [START_REF] Beeson | Proof and computation in geometry[END_REF][START_REF] Beeson | OTTER proofs in Tarskian geometry[END_REF]. The formalization by Beeson and Wos can be considered semi-automatic as the authors provide many guidelines to Otter for the difficult theorems: they provide the points to be constructed and also long lists of proof steps. Beeson and Wos also provide intermediate lemmas not appearing in the original book, some of which seem to be inspired by the Coq formalization (see the lemma in Chapter 5 6 ). Within this development, neither formal proofs (verifiable by proof assistants) nor readable and natural-language proofs were considered.

Braun and Narboux proved most theorems (theorems about three-dimensional geometry are omitted) from the first twelve chapters within the proof assistant Coq (with minimal automation) [START_REF] Narboux | Mechanical theorem proving in Tarski's geometry[END_REF][START_REF] Braun | From Tarski to Hilbert[END_REF]. Recently, Braun, Narboux, and Boutry proved some high-level geometry theorems based on Tarski's axiom system: existence of the center of gravity, orthocenter, circumscribed circle as well as stan-dard properties of quadrilaterals [START_REF] Boutry | Using small scale automation to improve both accessibility and readability of formal proofs in geometry[END_REF]. Like the development presented in this paper, both the Coq and Otter formalizations do not use sets and all formulations from SST are changed accordingly. For instance, none of the above developments use the concept of lines -instead, lines are implicit and represented by pairs of points. However, unlike our approach, these approaches do not use additional predicates that mimic dealing with sets of points. These developments also do not use function symbols: n-ary functions are represented by predicates of arity n + 1. In both formalizations this requires proving some intermediate lemmas such as pseudo transitivity of collinearity:

A = B ∧ col(A, B, C) ∧ col(A, B, D) ⇒ col(A, C, D).
The chapters of SST are uneven in depth and difficulty of their contents and this is also reflected in the computer developments. One (of course, informal) illustration of depth and complexity of the chapters are the numbers of theorems in the computer developments. The total number of theorems is: 565 in the Coq development, 7 119 in the Otter development (up to Section 9.6), and 238 in our TPTP development in coherent logic. Figure 1 shows the number of theorems in SST and in the computer developments. As an informal measure of the difficulty of theorems, we use the number of lines in the proofs within the Coq development (of course, some theorems can be proved in some other way, so this measure is not perfect, but still can be used as an illustration). Figure 2 shows the distribution of theorems with respect to the proof lengths in the Coq development.

Merging Together Computer Developments

In order to use the existing Coq development for guiding our automated proving framework, we first needed to match it with the SST lists of theorems and with our TPTP list of theorems (we performed these tasks partly using our ad-hoc tools and partly manually). Most often, it was easy, but there were some challenges. For instance, in computer developments, many SST theorems were broken into several ones often belonging to coherent logic (although the authors of the Coq development did not intend to use any tool for coherent logic), so the matching with SST was not one-to-one. For one of our key experiments, we needed to integrate all the lemmas from the Coq formalization into our TPTP development. First, all the Coq lemmas were (if needed) translated to coherent logic and the TPTP format. Second, all the Coq lemmas (in CL form) had to be matched with corresponding SST theorems (SST theorems were not always uniformly named in the Coq formalization) and then inserted into our list of theorems. Using dependency files, the two formalizations were merged such that every Coq lemma (not existing in our original TPTP list) was positioned at the latest possible place (before the first theorem whose proof uses that lemma). Merging two computer developments (in this case -the Coq and the TPTP version) was rather challenging, not only because of different syntax, naming conventions, and available features, but also because of little differences in formulation of the original contents. SST is very rigorous, so it seems a bit unexpected that there are ambiguities and, consequently, differences in computer developments. 8 Looking closer reveals the main reason for these problems: as said above, in contrast to SST, neither of the exist-ing computer developments uses sets. It is even claimed that SST substantially does not use sets or that sets can be trivially avoided. Still, by avoiding sets, translations from SST are not always straightforward and some errors can be introduced. As an illustration, we will briefly present (using a common mathematical notation) an error that we discovered, in the existing Coq formalization of SST, while taking over the definitions and lemmas from the Coq development and integrating them in our TPTP list. In the Coq development, the predicate is image(P , P, A, B) (P and P are symmetric w.r.t. the line AB) was defined (following the first part of SST definition 10.3) as:

∃X(is midpoint(X, P, P ) ∧ col(A, B, X) ∧ (perp(A, B, P, P ) ∨ P = P ), where is midpoint(X, P, P ) holds if X is the midpoint of P P , col(A, B, C) holds if A,B,C are collinear, and perp(A, B, P, P ) holds if AB is perpendicular to P P . The Coq development contains the following lemma:

col(A, B, X) ⇒ is image(X, X, A, B).
But there is a special case when A = B in Definition 10.3 (is symmetric(P, P , A) holds if P and P are symmetric w.r.t. A):

is image(P, P , A, B) :=    ∃X is midpoint(X, P, P ) ∧ col(A, B, X) ∧(perp(A, B, P, P ) ∨ P = P ) ifA = B
is symmetric(P, P , A) if A = B So, from the fact that col(A, A, P ) holds it follows that is image(P, P, A, A) and then is symmetric(P, P, A) will hold, which is not the case in general (i.e., not in the case when P = A). The problem occurred because SST uses lines (as sets of points), while the Coq development uses only points and the translation from the original formulations to Coq was not completely straightforward. This small unfaithfulness to the SST definition actually led to the inconsistency which was discovered during integration with our formalization (use of resolution provers discovered the inconsistency). Changing the definition in the Coq development to be faithful to the SST definition gave us lemmas with fewer non-degeneracy conditions. Many conditions A = B could be removed thanks to the more general definition of the predicate is image.

The use of the automated provers in the merging process also helped in detecting some duplicated or redundant lemmas (for instance, if a lemma can be proved using only one other lemma, it can be eliminated as redundant).

Automation and Results

With all Tarski's axioms, definitions, and theorems (reformulated if needed, as described in Section 4.2) from the first twelve chapters of SST stored in TPTP form, we performed several experiments trying to explore how many theorems (out of the total of 238) can be proved automatically, with some sort of guidance. The existing developments can be used not only as a reference (for a comparison with an automated approach), but also as a simulation of real human guidance. We used information that we got from interactively developed proofs within Coq [START_REF] Narboux | Mechanical theorem proving in Tarski's geometry[END_REF][START_REF] Braun | From Tarski to Hilbert[END_REF].

The experiments were performed on a set of four 12-core servers with AMD Opteron 6168 CPUs. For each conjecture, all resolution provers were invoked twice (for premises given in normal and reversed order), with the time limit of 60s for each call,9 while ArgoCLP prover had the time limit of 1000s. 10Full Automation, No Human Guidance. In our first experiment, we applied our framework (described in Section 3) to the list of 238 theorems corresponding to the contents of the first twelve chapters of SST. The axioms, definitions, and theorems are listed in exactly the same way as in the book. When attempting to prove one theorem, all axioms, definitions, and theorems (proved automatically or not) that precede that theorem are used (i.e., passed to the provers). In addition, we used the following specifics:

for proving theorems from the first eleven chapters, we pass axioms A1-A9 to the provers; for proving theorems from Chapter 12, we also pass the axiom A10. We did not use the axiom A11. we pass the axioms of the form:

∀x(R(x) ∧ R(x) ⇒ ⊥), ∀x(R(x) ∨ R(x)),
for all primitive and defined predicate symbols R.

By this fully automated approach, out of 238 theorems, 114 (48%) were proved by (at least one of) the resolution provers, 87 (37%) of them were then proved by ArgoCLP, and for 41 (17%) of them all used theorems and lemmas were also proved by ArgoCLP. Detailed information (by chapters) is given in Table 1 and in Figure 3.

Automation with Implicit Guidance (automation with extended list of lemmas). In our second experiment, we expanded the list of theorems with the list of auxiliary lemmas used within the Coq formalization. The idea is that auxiliary lemmas could be easier to prove than original theorems, and with those lemmas at hand, the proving process of the following theorems should be easier. The experiment simulates a benefit that could be gained in an interaction between a human mathematician and a computer: a mathematician builds a theory, formulates additional lemmas and tries to prove lemmas/theorems first automatically, and if that does not succeeded, interactively. We call this and the next experimental setting "automation with guidance", because Coq lemmas 1. Numbers of theorems proved by our (basic) framework, numbers of theorems proved with auxiliary lemmas imported from Coq (extended), numbers of theorems proved using dependency lists imported from Coq proofs (dep.lists). For each category, 'res' stands for theorems proved by one of resolution provers, 'argo' stands for theorems proved then by ArgoCLP, and 'full' stands for theorems that were proved when all the theorems used as premises were also proved.

generated by a human are used as a guidance to the automated provers. We call this setting "with implicit guidance" because the resolution provers were not given a short list of axioms/lemmas/theorems actually used in the proof of the theorem being considered, unlike in the following experiment. The setting of this experiment was the same as for the first one. By this approach, out of 238 theorems, 130 (55%) were proved by (at least one of) the resolution provers, 99 (42%) of them were then proved by ArgoCLP, and for 41 (17%) of them all used theorems and lemmas were also proved by ArgoCLP. Concerning the lemmas taken from the Coq development, the performance is similar for all of 218 lemmas: 137/88/27, giving the following totals for 456 theorems: 267/187/68. Detailed information (by chapters) is given in Table 1 and in Figure 4.

Automation with Explicit Guidance (automation with direct dependency lists). In our third experiment, for a concrete theorem being proved, we used only its dependency list -the list of lemmas/theorems used for proving that theorem within the Coq formalization. This experiment simulates a scenario of formalizing a proof of a mathematical theorem when it is known what lem- mas are (directly) relevant, but still the task of constructing a formal, machine verifiable proof is non-trivial (for instance, in a textbook there may be only a proof-outline available, or a mathematician may have only a vague picture of a proof and can guess relevant lemmas). In this context, we initially used only definitions and lemmas/theorems given in the dependency lists, and all the axioms including the axioms of the form ∀x(R(x) ∧ R(x) ⇒ ⊥), for all primitive or defined predicate symbols R (if the proving process failed, then we also used all the definitions that precede the conjecture). By this approach, out of 238 theorems, 150 (63%) theorems were proved by (at least one of) the resolution provers, 95 (40%) were then proved by ArgoCLP, and for 52 (22%) of them all used theorems and lemmas were also proved by ArgoCLP. Concerning lemmas taken from the Coq development, the performance is similar for all 218 lemmas: 147/76/38, giving the following totals for 456 lemmas/theorems: 297/171/90. Detailed information (by chapters) is given in Table 1 and in Figure 5.

Discussion. As we expected, the presented results show that automated theorem provers can prove a significant portion of goals within a formalization task (out of the three used resolution provers, Vampire had the best performance). Also, inserting intermediate lemmas (from formalization developed by a human) helps the automated provers which is not surprising. It is also not surprising that giving the dependency lists (from the Coq formalization) to the resolution provers significantly increases their performance. However, we were surprised that ArgoCLP can prove less theorems (95) when provided the dependencies from the Coq proofs (via the resolution provers) than the dependencies discovered by a resolution prover (99). Looking deeper into the data reveals that for some theorems it happens that the dependencies from the Coq proofs contain more lemmas than proofs discovered by the resolution provers. This shows that resolution provers can be used to find shorter, alternative proofs, that can simplify some of the interactive proofs. Concerning the time spent, the experiment that spent the least overall time is the third one. This was expected, as the provers were given short lists of premises. This performance shows potential for usability of this when it is applicable.

Concerning the difficulty of the proved theorems, again as expected, our framework performed better on simple theorems (i.e., on theorems with shorted Coq proofs). Figure 6 shows the percentage of theorems proved by ArgoCLP, using the list of auxiliary lemmas against the lengths of corresponding Coq proofs.

Above we presented numbers of proved theorems with and without all premises proved. Although it might seem that only the latter ones are relevant, we believe that the former ones are also (or even more so) practically important and better estimate the needed amount of human's work in real-world tasks. Namely, these numbers reflect a realistic scenario in which a human, in a formalization project, uses synergy with interactive and automated theorem proving. The human could try, within a proof assistant, to prove conjectures sequentually, one by one, and he would first try to obtain a formal proof automatically, using all previous axioms and theorems. If that failed, he would have to prove the theorem himself (and for the next conjectures he would have all premises already proven).

Related Work

Our proving framework is closely related to the Sledgehammer approach [START_REF] Blanchette | Automatic proof and disproof in Isabelle/HOL[END_REF][START_REF] Blanchette | Extending sledgehammer with SMT solvers[END_REF], but Sledgehammer does not aim at producing readable proofs, it only suggests the axioms and theorems to be used. Sledgehammer can use additional tools that can redirect refutation proofs constructed by resolution provers [START_REF] Blanchette | Redirecting proofs by contradiction[END_REF], while our framework can be used for producing proofs for a range of proof assistants and also for producing proofs in readable, natural language form. Closely related to the spirit of our study is a study of Kaliszyk and Urban [START_REF] Kaliszyk | Learning-assisted automated reasoning with Flyspeck[END_REF]. They explored how many theorems an automated theorem provers (for first-order logic, for higher-order logic, and for SMT) can handle (in conjunction with the HOL Light theorem prover) out of 14185 theorems appearing within the Flyspeck project. They used a number of automated theorem provers within their study, with Vampire, E, and Z3 having the most important role. In the first approach, the dependencies from the formalization (lists of theorem/lemmas used within the existing formal proofs) were used and only the relevant theorems/lemmas were passed to the automated theorem provers. The success rate in this approach was 43.2% (for the time limit of 900s) and it serves as an upper limit for what one might expect from fully automated approach. In another approach, all theorems that precede (in chronological order) the current conjecture are considered, but only some of them would be selected by a set of special heuristics (for premise selection) and passed to automated theorem provers. With this approach, the success rate was 39.5% (with 192-fold parallelization and time-limit equal 30s, on a 48-core server with AMD Opteron 6174 2.2 GHz CPUs, 320 GB RAM, and 0.5M B L2 cache per CPU). The same authors also work on informal readable proofs [START_REF] Tankink | Communicating formal proofs: The case of Flyspeck[END_REF] and linking them with formal proofs. Their case study are the proofs from the Flyspeck project [START_REF] Hales | Introduction to the Flyspeck project[END_REF]. They also provide a tool for visualizing the proof steps dynamically from a tactic based formal proof (either from Isabelle or Coq).

Ganesalingam and Gowers work on automated generation of readable proofs [START_REF] Ganesalingam | A fully automatic problem solver with humanstyle output[END_REF], and they propose inference rules which are very similar to our coherent logic based proof system.

Conclusions and Future Work

In this paper we promote the use of state-of-the-art automated theorem provers in formalization tasks and within a wider framework that combines different sorts of provers. For one classical twentieth century mathematical book, it turned out that for 37% theorems, readable and machine verifiable proofs can be generated completely automatically. This shows that automated theorem proving can provide significant help in formalization tasks within proof assistants (of course, typically in proving less difficult theorems).

Apart from success rates presented above and a generally optimistic message, during our case study we learned some additional lessons:

automated theorem proving can help in detecting inconsistency (involving axioms, definitions, and unproved conjectures) within a computer development of a mathematical theory. automated theorem proving can help in merging available pieces of mathematical knowledge formalized within the same or different settings.

One of the products (available also from http://argo.matf.bg.ac.rs) of our work is a TPTP representation of SST, and a document with all axioms, definitions, theorems, and generated proofs filled-in, given in a natural language form. This material can also serve for training of machine learning techniques for choosing relevant axioms/definitions/lemmas for premises, in the spirit of techniques used within the Flyspeck project [START_REF] Kaliszyk | Learning-assisted automated reasoning with Flyspeck[END_REF].

The existing developments of Tarski's geometry can be considered interactive or semi-interactive. For future work we are planning to further explore potentials for full automation, for example to use information from resolution provers more deeply and guide our coherent prover more precisely. This way we should cover at least some of the theorems proved by the resolution provers and not by ArgoCLP. In particular, we would focus on the axioms ∀x(R(x)∨R(x)) that can heavily extend the search space. To further improve readability, we will consider using function symbols and work on extending ArgoCPL to deal with function symbols. We will explore ways for using our framework for simplifying existing proofs within proof assistants (by using dependencies from automated theorem provers). In particular, we will use the presented framework for formalizing other classical mathematical sources and we will explore if our framework sometimes gives simpler proofs than those available (so, some fragments of the formalized knowledge can be simplified). We will also try to use our framework to tackle theorems from SST that require using the continuity axiom (i.e., the schema of axioms).

4 .

 4 It holds that A = B or A = B. 5. Assume that: A = B. 6. From the fact(s) AD ∼ = AB and A = B it holds that AD ∼ = AA. 7. From the fact(s) AD ∼ = AA it holds that A = D (using ax 3). 8. From the fact(s) A = B and A = D it holds that B = D. 9. The conclusion follows from the fact(s) B = D. 10. Assume that: A = B. 11. It holds that A = C or A = C. 12. Assume that: A = C. 13. From the fact(s) bet(A, B, C) and A = C it holds that bet(A, B, A). 14. From the fact(s) bet(A, B, A) and bet(B, A, A) it holds that A = B (using th 3 4). 15. From the fact(s) A = B and A = B we get contradiction. 16. Assume that: A = C. 17. From the fact(s) A = C it holds that C = A. 18. From the fact(s) C = A and col(C, A, B) and CB ∼ = CD and AB ∼ = AD it holds that B = D (using th 4 18). 19. The conclusion follows from the fact(s) B = D. 20. The conclusion follows in all cases. 21. The conclusion follows in all cases. QED

  fof(ax_8_11_1_1, axiom, (! [X,A,B,C,D] : ((perp_in(X,A,B,C,D) & A!=X & C!=X) => (A!=B & C!=D & point_on_line(X,A,B) & point_on_line(X,C,D) & per(A,X,C))))).

Fig. 1 .Fig. 2 .

 12 Fig. 1. Numbers of theorems in the book and in the computer developments.

Fig. 3 .Fig. 4 .Fig. 5 .

 345 Fig. 3. The number of theorems proved by our framework

  The number of theorems proved by ArgoCLP and using the list of auxiliary lemmas against the lengths of corresponding Coq proofs.

	number of theorems
	120		Total number of theorems
	100		Theorems proved by ArgoCLP
	80
	60
	40		79%	63%	39% 35%
	20	78%			30%	8%	3%	4%
		0-2	3-4	5-8	9-16 17-32 33-64 65-128129-256 > 256	proof length
	Fig. 6.

http://www.cs.miami.edu/ ~tptp/

Of course, if a resolution prover has an option of returning minimal inconsistent set of clauses, this iterative process does not need to be applied.

This definition can trivially be broken into two implications that are in coherent form and therefore can be used within our framework.

http://www.cs.miami.edu/ ~tptp/

http://argo.matf.bg.ac.rs/?content=downloads

http://www.michaelbeeson.com/research/FormalTarski/index.php?include= archive5

Note that the whole of the available Coq formalization involves also some lemmas not used for proving theorems from SST, but for other tasks. Out of 565 lemmas and theorems, 456 are used for proving theorems from SST.

In formalizing mathematical knowledge, because of different ambiguities there is a general problem of finding the intended meaning of the author. This problem is notorious for some mathematical classics, e.g., Hilbert's Grundlagen der Geometrie[START_REF] Hilbert | Grundlagen der Geometrie[END_REF], as it was demonstrated within several formalization projects[START_REF] Meikle | Formalizing Hilbert's Grundlagen in Isabelle/Isar[END_REF][START_REF] Meikle | Mechanical theorem proving in computation geometry[END_REF].

The relatively low time limit is chosen to reflect possible real-world applications (Sledgehammer uses a time limit of 30s). Higher time-limits do not change the overall picture much: in the experiments without guidance, the resolution provers proved 48% theorems for the 1 minute time limit, 49% theorems for the 2 minutes time limit, 51% theorems for the 5 minutes time limit, 54% theorems for the 30 minutes time limit.

The time limit for ArgoCLP is relatively high, but it is not much higher than the time limit for the resolution provers (since they take 6×60s). The time limit of 1000s is acceptable for an offline formalization work. Actually, the framework is usable also in an interactive regime: 84% conjectures proved by ArgoCLP within 1000s were also proved within the 60s time limit.

Acknowledgements. We are grateful to Stephan Schulz for his help and comments about using the prover E, and to Filip Marić for his advice about Isabelle proofs and his feedback on earlier versions of this paper. We are also grateful to the anonymous reviewers for a very helpful feedback on earlier versions of this paper.

The research presented in this paper was partly funded by the Serbian-French Technology Co-Operation grant EGIDE/"Pavle Savić" 680-00-132/2012-09/12. The first and the third author are partly supported by the grant ON174021 of the Ministry of Science of Serbia. The final publication is available at Springer via: http://dx.doi.org/10.1007/s10472-014-9443-5.


Danielle Hilhorst

Philippe Laurençot

Thanh-Nam Nguyen

Large time behavior and Lyapunov functionals for a nonlocal differential equation

Keywords: 2010 Mathematics Subject Classification. 45K05, 35B40, 35R09 Nonlocal differential equation, ω-limit set, large time behavior, convergence to steady states

.

Introduction

Let Ω be an open bounded subset of R N , N ≥ 1, and consider the following nonlocal differential equation (P )

           u t = u 2 (1 -u) -u(1 -u) Ω u 2 (1 -u) dx Ω u(1 -u) dx , x ∈ Ω, t ≥ 0 , u(x, 0) = u 0 (x) , x ∈ Ω ,
which was proposed by M. Nagayama [START_REF] Nagayama | [END_REF] to describe bubble motion with chemical reaction when a volume constraint is included. The initial condition u 0 is here a bounded function in L ∞ (Ω). Note that Problem (P ) is of bistable type since it can be written in the form

u t = u(1 -u)(u -λ(t)),
where

λ(t) := Ω u 2 (1 -u)(x, t) dx Ω u(1 -u)(x, t) dx . (1)
A general form of Problem (P ) is actually studied in [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF] where the wellposedness and the large time behavior of solutions of (P ) are investigated. In particular, the structure of the ω-limit sets of solutions of (P ) is described in [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF] with the help of the rearrangement theory. Restricting our attention to the specific Problem (P ) given above, the aim of this paper is to provide additional information on the ω-limit sets with an alternative approach. Our approach is actually based upon the existence of infinitely many Lyapunov functionals, from which we deduce the limit of the nonlocal term and hence the ω-limit set.

As in [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF], we suppose that the initial condition u 0 satisfies one of the following hypotheses:

(H 1 ) u 0 ∈ L ∞ (Ω), u 0 (x) ≥ 1 for a.e. x ∈ Ω, and u 0 ≡ 1.

(H 2 ) u 0 ∈ L ∞ (Ω), 0 ≤ u 0 (x) ≤ 1 for a.e. x ∈ Ω, and u 0 (1 -u 0 ) ≡ 0.

(H 3 ) u 0 ∈ L ∞ (Ω), u 0 (x) ≤ 0 for a.e. x ∈ Ω, and u 0 ≡ 0.

In [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF], when u 0 satisfies either (H 1 ) or (H 3 ), the solution u of (P ) is shown to converge to a step function. The first contribution of this paper is to identify this function in terms of the initial condition u 0 . We obtain a less precise result when u 0 satisfies (H 2 ) but complete the analysis performed in [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF] in that case. Besides these qualitative results we also identify an infinite family of Lyapunov functionals for (P ).

For further use, we define

f (z) := z 2 (1 -z) , g(z) = z(1 -z) , z ∈ R .
Throughout the paper we denote the Lebesgue measure of a measurable set A ⊂ Ω by |A|.

The paper is organized as follows. In Section 2, we recall some results from [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF] dealing with the well-posedness of problem (P ) as well as with the existence of invariant sets. In Section 3, we show that problem (P ) possesses infinitely many Lyapunov functionals, and use this property to study the limit of the nonlocal term. Finally, in Section 4, we characterize the ω-limit set for initial data satisfying either (H 1 ) or (H 3 ), and improve the outcome of [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF] when (H 2 ) holds.

2 Well-posedness and ω-limit sets

We recall some results from [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF] and first make precise the notion of solution to (P ) to be used later.

Definition 2.1 ([3]). Let 0 < T ≤ ∞. A function u ∈ C 1 ([0, T ); L ∞ (Ω)
) is called a solution of Problem (P ) on [0, T ) if the following three properties hold:

(i) u(0) = u 0 , (ii) Ω g(u(x, t)) dx = 0 for all t ∈ [0, T ), (iii) u t (x, t) = f (u(x, t)) -λ(t)g(u(x, t
)) for a.e. x ∈ Ω and all t ∈ [0, T ), where λ(t) is defined in (1).

We note that solutions of (P ) on [0, T ) satisfy the mass conservation property:

Ω u(x, t) dx = Ω u 0 (x) dx , t ∈ [0, T ) . (2)
We summarize the well-posedness of (P ) in the next result.

Proposition 2.2 ([3]

). Assume that (H i ) holds for some i = 1, 2, 3. Problem (P ) possesses a global solution u ∈ C 1 ([0, ∞); L ∞ (Ω)). Moreover:

(i) If (H 1 ) holds, then for all t ≥ 0, 1 ≤ u(x, t) ≤ ess sup Ω u 0 a.e. in Ω. ( 3
) (ii) If (H 2 ) holds, then for all t ≥ 0, 0 ≤ u(x, t) ≤ 1 a.e. in Ω. (4)
(iii) If (H 3 ) holds, then for all t ≥ 0, ess inf Ω u 0 ≤ u(x, t) ≤ 0 a.e. in Ω.

(5)

Given u 0 satisfying (H i ) for some i = 1, 2, 3, we define the set I i by

I 1 := [1, ess sup Ω u 0 ], I 2 := [0, 1], I 3 := [ess inf Ω u 0 , 0] ,
according to the value of i. A consequence of Proposition 2.2 is that I 1 , I 2 , and I 3 are invariant sets for the flow associated to (P ). This property entails the boundedness of λ as shown below.

Corollary 2.3. Assume that u 0 satisfies (H i ) for some i = 1, 2, 3. Then λ(t) ∈ I i for all t ≥ 0.

Proof. The corollary is a consequence of the uniform bounds for u in Proposition 2.2 and the property f (z) = zg(z) for z ∈ R.

We finally recall that, given an initial condition u 0 satisfying (H i ) for some i = 1, 2, 3, and denoting the corresponding solution to (P ) given by Proposition 2.2 by u, the ω-limit set of u 0 is defined in [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF] as follows:

ϕ ∈ ω(u 0 ) if and only if      ϕ ∈ L 1 (Ω) and there is a sequence (t n ) n≥1 such that lim n→∞ u(t n ) -ϕ L 1 (Ω) = 0 and lim n→∞ t n = ∞ .
Several properties of ω(u 0 ) are obtained in [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF]:

Theorem 2.4 ([3]). (i) If (H 1 )
holds, then ω(u 0 ) = {ϕ} is a singleton and there are µ > 1 and a measurable subset A of Ω such that

ϕ = µχ A + χ Ω\A . (6)
(ii) If (H 2 ) holds and ϕ ∈ ω(u 0 ), then there are ν ∈ (0, 1) and two disjoint measurable subsets A 1 and A 2 of Ω such that

ϕ = χ A 1 + νχ A 2 . (7)
(iii) If (H 3 ) holds, then ω(u 0 ) = {ϕ} is a singleton and there are ξ < 0 and a measurable subset

A of Ω such that ϕ = ξχ A . ( 8
)
3 Lyapunov functionals and limit of the nonlocal term Proposition 3.1. Assume that (H i ) holds for some i = 1, 2, 3.

Let Φ ∈ C 1 (R) be such that Φ ′ is non-decreasing on I i . Then E i (u(t)) := (-1) i+1 Ω Φ(u(x, t)) dx
is a Lyapunov functional of Problem (P ). As a consequence, lim t→∞ E i (u(t)) exists as t → ∞.

Proof. We only prove the statement in the case i = 1. It follows from (P ) and ( 2)

that d dt E 1 (u) = Ω Φ ′ (u)u t dx = Ω Φ ′ (u)u t dx - Ω Φ ′ (λ)u t dx = Ω Φ ′ (u) -Φ ′ (λ) u t dx = Ω Φ ′ (u) -Φ ′ (λ) u -λ u(1 -u) dx.
Since u ≥ 1 and λ ≥ 1 by (3) and Corollary 2.3, the monotonicity of Remark 3.2. The above proposition implies that there are infinitely many Lyapunov functionals for Problem (P ).

Φ ′ on I 1 implies (Φ ′ (u) -Φ ′ (λ) u -λ ≥ 0. Therefore d dt E 1 (u(t)) ≤ 0 ,
Corollary 3.3. Assume that (H i ) holds for some i = 1, 2, 3. Then

l g := lim t→∞ Ω g(u(x, t)) dx and l f := lim t→∞ Ω f (u(x, t)) dx exist.
Proof. First we consider the case where (H 1 ) holds. Recall that in this case u(x, t) ∈ I 1 for a.e. x ∈ Ω and all t ≥ 0. Since the functions -g ′ (z) = 2z -1 and -f ′ (z) = 3z 2 -2z are non-decreasing on I 1 , we infer from Proposition 3.1 that

-l g = lim t→∞ Ω (-g)(u(x, t)) dx and -l f = lim t→∞ Ω (-f )(u(x, t)) dx
both exist. Hence the result of the corollary follows in the case that (H 1 ) holds.

The case where (H 3 ) holds is proved in a similar way. Finally we consider the case of hypothesis (H 2 ). As in the previous cases, the function -g ′ is non-decreasing on I 2 so that l g = lim t→∞ Ω g(u(x, t)) dx exists.

To complete the proof we simply note that f = f 1 -f 2 with f 1 (z) := z 2 and f 2 (z) := z 3 . Since f ′ 1 and f ′ 2 are non-decreasing on I 2 , using again Proposition 3.1 ensures the existence of the limits

lim t→∞ Ω f 1 (u(x, t)) dx and lim t→∞ Ω f 2 (u(x, t)) dx ,
from which we readily deduce that

lim t→∞ Ω f (u(x, t)) dx = lim t→∞ Ω f 1 (u(x, t)) dx -lim t→∞ Ω f 2 (u(x, t)) dx exists.
After this preparation we are in a position to study the behavior of λ(t) as t → ∞. Lemma 3.4.

(i) Assume that (H 1 ) holds. Then λ ∞ := lim t→∞ λ(t) exists and λ ∞ > 1.

(ii) Assume that (H 3 ) holds. Then λ ∞ := lim t→∞ λ(t) exists and λ ∞ < 0.

Proof. Owing to Corollary 3.3 we set

l g := lim t→∞ Ω g(u(x, t)) dx , l f := lim t→∞ Ω f (u(x, t)) dx .
(i) Since u ≥ 1 by Proposition 2.2, one has g(u(t)) ≤ 0 a.e. in Ω for all t ≥ 0, so that l g ≤ 0. Now we show that l g < 0. Assume for contradiction that l g = 0. Then

- Ω (u(x, t) -1) dx - Ω (u(x, t) -1) 2 dx = Ω g(u(x, t)) dx -→ t→∞ 0 . Therefore u(t) → 1 in L 2 (Ω) as t → ∞.
We then deduce from the mass conservation property (2) that

1 |Ω| Ω u 0 (x) dx = 1 ,
which contradicts (H 1 ). Therefore l g < 0 hence λ ∞ := lim t→∞ λ(t) exists. It follows from Corollary 2.3 that λ ∞ ≥ 1. Next we show that λ ∞ > 1. Assume for contradiction that λ ∞ = 1. Then

lim t→∞ Ω u(1 -u) 2 (x, t) dx = lim t→∞ Ω g(u(x, t)) dx -lim t→∞ Ω f (u(x, t)) dx = l g -l f = 0 ,
which gives, together with the lower bound u ≥ 1,

u(t) → 1 in L 2 (Ω) as t → ∞ .
Arguing as above with the help of (2), we end up with a contradiction to (H 1 ).

(ii) It is sufficient to establish that l g < 0 and l f > 0. First we show that l g < 0. By the mass conservation property (2), we have

l g = lim t→∞ Ω u(x, t) dx -lim t→∞ Ω u 2 (x, t) dx ≤ Ω u 0 (x) dx .
In view of (H 3 ), the right-hand side of the above inequality is negative so that l g < 0.

Next we prove that l f > 0. Since u ≤ 0 a.e. in Ω×(0, ∞), f (u) = u 2 (1 -u) ≥ 0 a.e. in Ω × (0, ∞) hence l f ≥ 0. Assume for contradiction that l f = 0. Then

0 ≤ lim t→∞ Ω u 2 (x, t) dx ≤ lim t→∞ Ω u 2 (1 -u)(x, t) dx = 0 , so that u(t) → 0 in L 2 (Ω) as t → ∞.
We combine this property with the mass conservation (2) to conclude that Ω u 0 (x) dx = 0 , which contradicts (H 3 ). Thus l f < 0.

Characterization of ω-limit set

We first recall some notation and results from [START_REF] Nguyen | On the ω-limit set of a nonlocal differential equation proposed[END_REF]. Given u 0 satisfying (H i ) for some i = 1, 2, 3, we denote the corresponding solution to (P ) by u and consider the unique solution Y (t; s) of the following auxiliary problem:

(ODE)    Ẏ (t) = Y (t) 2 (1 -Y (t)) -λ(t)Y (t)(1 -Y (t)), t > 0, Y (0) = s, (9)
where Ẏ := dY /dt and λ is defined by [START_REF] Hale | Ordinary differential equations[END_REF]. Clearly the function u satisfies u(x, t) = Y (t; u 0 (x)) for a.e. x ∈ Ω and all t ≥ 0.

(10)

For later convenience, we introduce the differential operator L:

L(Z)(t) := Ż(t) -Z(t) 2 (1 -Z(t)) + λ(t)Z(t)(1 -Z(t)) , t ≥ 0 . ( 11
)
The following comparison principle is quite standard in the theory of ordinary differential equations; see, e.g., [1, Theorem 6.1, page 31].

Proposition 4.1. Let T > 0 and let

Z 1 , Z 2 ∈ C 1 ([0, T ]) satisfy    L(Z 1 )(t) ≤ L(Z 2 )(t) for all t ∈ [0, T ], Z 1 (0) ≤ Z 2 (0). Then Z 1 (t) ≤ Z 2 (t) for all t ∈ [0, T ].

ω-limit set when (H 1 ) holds

We first identify two invariant sets with the help of problem (ODE).

Lemma 4.2. Suppose (H 1 ). We define the sets

Ω 1 (t) := {x ∈ Ω : Y (t; u 0 (x)) = 1} and Ω + (t) := {x ∈ Ω : Y (t; u 0 (x)) > 1} for each t ≥ 0.
Then

Ω 1 (t) = Ω 1 (0) and Ω + (t) = Ω + (0) for all t ≥ 0 .
Proof. Note that if s = 1, then the unique solution of (ODE) is given by Y (t; 1) = 1 for all t ≥ 0. Therefore, the conclusion of Lemma 4.2 follows from the uniqueness of solutions of (ODE).

Remark 4.3. Owing to the definition of Y (•, s) we note that

Ω 1 (0) = {x ∈ Ω : u 0 (x) = 1} and Ω + (0) = {x ∈ Ω : u 0 (x) > 1} .
We next state the main result of this section where we identify ω(u 0 ), recalling that we already know that it is a singleton by Theorem 2.4. Theorem 4.4. Suppose (H 1 ). There holds:

(a) For all x ∈ Ω 1 (0), Y (t; u 0 (x)) → 1 as t → ∞, (b) For all x ∈ Ω + (0), Y (t; u 0 (x)) → λ ∞ as t → ∞.
As a consequence, the only element ϕ in ω(u 0 ) is given by

ϕ = χ Ω 1 (0) + λ ∞ χ Ω + (0) ,
the value of λ ∞ being determined by the equation

|Ω 1 (0)| + λ ∞ |Ω + (0)| = Ω u 0 (x) dx .
Proof. The statement (a) is obvious. We prove the statement (b) and first recall that λ ∞ > 1 by Lemma 3.4. Let x 0 ∈ Ω + (0) and let ε > 0 be arbitrarily small such that λ ∞ -ε > 1. There exists t ε > 0 such that

λ(t) ∈ [λ ∞ -ε, λ ∞ + ε] for all t ≥ t ε .
We define Y (t) := Y (t; u 0 (x 0 )) for all t ≥ t ε and let α and β be the solutions to the ordinary differential equations

α = α(1 -α)(α -λ ∞ + ε) , t ≥ t ε , α(t ε ) = Y (t ε ; u 0 (x 0 )) , and β = β(1 -β)(β -λ ∞ -ε) , t ≥ t ε , β(t ε ) = Y (t ε ; u 0 (x 0 )) . Since x 0 ∈ Ω + (0) = Ω + (t ε ), we have α(t ε ) = β(t ε ) > 1 which implies that α(t) > 1, β(t) > 1 for all t ≥ t ε ,
and thus lim

t→∞ α(t) = λ ∞ -ε, lim t→∞ β(t) = λ ∞ + ε. ( 12
)
Let L be defined by (11); then L(Y )(t) = 0 for all t ≥ 0. Note that, for t > t ε ,

L(α)(t) = -α(t)(1 -α(t))(λ ∞ -ε -λ(t)) ≤ 0 (i) There is λ ∞ ∈ [0, 1] such that λ(t) → λ ∞ as t → ∞. (ii) For all s ∈ [0, 1], there is Y ∞ (s) ∈ {0, λ ∞ , 1} such that Y (t; s) → Y ∞ (s) as t → ∞.
(iii) If λ ∞ ∈ (0, 1), then the set Y -1 ∞ (λ ∞ ) contains at most one element. Proof. (i) Assertion (i) directly follows from the assumption l g = 0 and Corollaries 2.3 and 3.3.

(ii) Let s ∈ [0, 1] and set Y (t) := Y (t; s) for t ≥ 0. Recall that (ODE) implies that Y (t) ∈ (0, 1) for all t ≥ 0. Given ε ∈ (0, 1) there is

t ε > 0 such that λ ∞ -ε ≤ λ(t) ≤ λ ∞ + ε , t ≥ t ε . (13)
Case 1. Either there are ε ∈ (0, 1) and

t 0 ≥ t ε such that Y (t 0 ) ∈ [λ ∞ -ε, λ ∞ + ε]. Case 1.1. If Y (t 0 ) < λ ∞ -ε, then (ODE) and (13) guarantee that Ẏ (t 0 ) < 0 so that τ := sup{t ≥ t 0 : Y (t) < λ ∞ -ε} > t 0 .
Clearly Ẏ (t) < 0 for t ∈ [t 0 , τ ) from which we readily conclude that τ = ∞. Therefore Y (t) < λ ∞ -ε and Ẏ (t) < 0 for all t ∈ [t 0 , ∞) and we infer from (ODE) and (13) that Ẏ

(t) ≤ Y (t)(Y (t 0 ) -λ ∞ + ε) , t ≥ t 0 .
Since Y (t 0 ) -λ ∞ + ε < 0, we conclude that Y (t) decays exponentially fast to zero and thus that Y ∞ (s) = 0.

Case 1.2. If Y (t 0 ) > λ ∞ + ε then Ẏ (t 0 ) > 0 by (ODE) and (13) and a similar argument entails that Y (t) → 1 as t → 1. Thus Y ∞ (s) = 1 in that case.

Case 2. Or Y (t) ∈ [λ ∞ -ε, λ ∞ + ε] for all (ε, t) ∈ (0, 1) × (t ε , ∞), which means that Y (t) → λ ∞ as t → ∞ and completes the proof of (ii).

(iii) Assume for contradiction that there are 0 < s

1 < s 2 < 1 such that Y ∞ (s 1 ) = Y ∞ (s 2 ) = λ ∞ . We set Y i (t) := Y (t; s i ) for t ≥ 0 and i = 1, 2 and Z := Y 2 -Y 1 and notice that lim t→∞ Z(t) = 0, Z(t) > 0 for all t ≥ 0 . (14)
We further deduce from (ODE) that Z solves

Ż = (1 + λ)(Y 1 + Y 2 ) -λ -Y 2 1 -Y 1 Y 2 -Y 2 2 Z , while assertion (i) of Lemma 4.6 entails that lim t→∞ (1 + λ)(Y 1 + Y 2 ) -λ -Y 2 1 -Y 1 Y 2 -Y 2 2 (t) = λ ∞ (1 -λ ∞ ) > 0 .
Owing to (14), we realize that Ż(t) ≥ 0 for t large enough, which contradicts (14).

By Lemma 4.6 (i), there is λ ∞ ∈ [0, 1] such that λ(t) -→ λ ∞ as t → ∞.

If λ ∞ = 0 or λ ∞ = 1, then it follows from Lemma 4.6 (ii) that Y ∞ (s) ∈ {0, 1} for s ∈ [0, 1]. Consequently, u(1 -u)(x, t) = Y (t; u 0 (x))(1 -Y (t; u 0 (x)) → 0 as t → ∞ for a.e. x ∈ Ω which implies that l g = 0 and contradicts (16).

If λ ∞ ∈ (0, 1) then Y -1 ∞ (λ ∞ ) contains at most one element by Lemma 4.6 (iii) which, together with (15), implies that Y ∞ (u 0 (x)) ∈ {0, 1} for a.e. x ∈ Ω. Consequently u(1 -u)(x, t) = Y (t; u 0 (x))(1 -Y (t; u 0 (x)) → 0 as t → ∞ for a.e. x ∈ Ω which implies that l g = 0 and again contradicts (16).

Consequently l g = 0 and, since 0 ≤ f (u(x, t)) ≤ g(u(x, t)) for a.e. x ∈ Ω and all t ≥ 0 by Proposition 2.2 (ii), we readily obtain that l f = 0. Remark 4.8. Under the assumptions of Proposition 4.7 it is unclear whether λ(t) has a limit as t → ∞.

Proposition 4. 7 .

 7 Suppose that (H 2 ) holds and that |{x ∈ Ω : u 0 (x) = s}| = 0 for all s ∈ (0, 1).(15)Thenl g := lim t→∞ Ω g(u(x, t)) dx = 0 and l f := lim t→∞ Ω f (u(x, t)) dx = 0 .Proof. Assume for contradiction that l g = lim t→∞ Ω g(u(x, t)) dx = 0 .

and

Hence, in view of (12), λ ∞ -2ε ≤ Y (t) ≤ λ ∞ + 2ε for all t large enough, which completes the proof of (b). Recalling (10) we can then identify the unique element ϕ of ω(u 0 ) which is given by

By the mass conservation property (2), we have

which characterizes the value of λ ∞ .

ω-limit set when (H 3 ) holds

The following result is similar to Theorem 4.4. We omit its proof.

Theorem 4.5. Suppose (H 3 ). Then the unique element ϕ of ω(u 0 ) is given by

where Ω -(0) := {x ∈ Ω : u 0 (x) < 0} and λ ∞ is defined by

ω-limit set when (H 2 ) holds

We finally turn to the case where u 0 satisfies (H 2 ). As already mentioned, the results to follow are not as precise as in the other cases but still shed some light on the dynamics of (P ).

Lemma 4.6. Assume that (H 2 ) holds and that l g := lim t→∞ Ω g(u(x, t)) dx = 0 . Then