D Klein

J Bitounis

V Pourchez

L Forest

G Leclerc

X Sarry

M Roblin

Cottier

Leslie Rinaldi
email: leslie.rinaldi@gmail.com

G Barabino

J.-P Klein

D Bitounis

J Pourchez

V Forest

L Leclerc

G Sarry

X Roblin

M Cottier

J.-M Phelip

Metals distribution in

Keywords: elemental analysis, environmental risk, magnesium, colorectal cancer

published or not. The documents may come

Introduction

Colorectal cancer accounts for over 9% of all cancer incidences. In the European Union, it is the third most common cancer diagnosis among men and women [START_REF]Cancer colorectal n[END_REF]. This worldwide mortality is approximately half that of the incidence (i.e. about 4.5%). Several risk factors are associated with the incidence of colorectal cancer. Among them, the nonmodifiable risks (i.e., those that an individual cannot control) include age and genetic.

Hereditary factors, which are involved in 5% of colorectal cancers, are represented by family susceptibility, familial adenomatous polyposis, and Lynch syndrome. Some digestive diseases are predictive factors of colorectal cancer, including chronic bowel diseases (Crohn's disease and hemorrhagic rectocolitis). However, colorectal cancer is also considered to be an environmental disease. Thus, several lifestyle-related factors have also been identified, such as nutritional practices, physical activity and obesity, cigarette smoking, and heavy alcohol consumption. Although numerous environmental risk factors may play an important role, those risk factors identified do not fully explain the frequency of colorectal cancer.

Occupational studies have tentatively linked colorectal cancer to asbestos [2,[START_REF] Newhouse | The asbestos industry and statutory control of its hazards[END_REF] and to metal dust [START_REF] Berg | Editorial: Genetic damage and carcinogenic drugs[END_REF]. Hence, a new field is receiving increasing attention, namely the study of environmental risk factors associated with the presence of chemical elements [START_REF] Lavilla | Elemental fingerprinting of tumorous and adjacent non-tumorous tissues from patients with colorectal cancer using ICP-MS, ICP-OES and chemometric analysis[END_REF][START_REF] Bocca | Determination of 30 elements in colorectal biopsies by sector field inductively coupled plasma mass spectrometry: method development and preliminary baseline levels[END_REF], such as exogenous micro-and nanoparticles [START_REF] Gatti | Biocompatibility of micro-and nano-particles in the colon. Part II[END_REF]. Some elements are essential for numerous metabolic and physiological processes in the body, as well as the synthesis and structural stabilization of enzymes, proteins, and nucleic acids. For example, Zn is essential for the functioning of more than 300 enzymes [START_REF] Tudor | Zinc in health and chronic disease[END_REF] and elements such as Cu, Fe, Mg, Ni, and Zn form compounds with proteins that have important catalytic functions. Cancer is fundamentally a disease of tissue growth regulation.

During tumorigenesis, some metal ions (e.g., Fe, Mg, Ni, Zn) induce binding competition with chromatin (e.g., DNA, histones, transcription factors, DNA repair enzymes) and other regulatory molecules that first give rise to tumors and then are responsible for controlling tumor growth. In addition, many studies have identified metal-induced carcinogenicity, demonstrating strong oxidative stress induced by elements such as Cd, Co, Cr, Cu, Fe, and Ni. Free radicals are highly reactive chemical species that have the potential to harm cells, including damage that may lead to cancer. In fact, the generation of reactive oxygen species (ROS) can cause DNA damage and enhance lipid peroxidation. The first-line antioxidant defense of the organism interacts with and neutralizes the effects of ROS, thus preventing them from causing damage. Antioxidants are also known as "ROS scavengers." However, many antioxidant enzymes, such as superoxide dismutases, have an active metal center (Cu, Mn, or Zn). So, the metal element concentrations in tissues can have a strong impact both on the oxidative stress and the antioxidant defense system. In other words, an imbalance in the optimum level of certain elements may lead to colon carcinogenesis due to a poor redox regulation. However, data on the elemental concentration ranges in human colorectal biopsies are scarce and fragmentary. As a result, a main challenge is to improve our knowledge of the elemental fingerprint of tumor tissue compared to non-cancer tissue.

The aim of this study was to evaluate the element distribution in colorectal adenocarcinoma biopsies, adjacent non-tumor tissues, and healthy controls. To do so, we investigated the elemental distribution in colorectal biopsies of cancer patients (i.e., in tumor and adjacent non-tumor tissues) compared to those of healthy controls (occlusion or ischemic colons). We used the same patients for evaluating the concentrations of various elements (Al, B, Cd, Cr, Cu, Fe, Mg, Mn, Ni, Pb, Se, Si, Ti, V, and Zn) in cancer and non-cancer tissue, this way allowing for a reliable comparison with potential biases such as genetic, environmental, or dietary factors being eliminated.

Methods

Patients

This case-control study was performed in the Digestive Surgery and Gastroenterological Departments of the University Hospital of Saint Etienne (France). To avoid the bias of selection, the clinical protocol was proposed to each collectomized patient between March 2011 and June 2013 at the University Hospital of Saint Etienne. Patients were considered for the study if they were at least 18 years old and an affiliated member of the social security system at the time of the surgical procedure, which included total or partial colectomy.

Before inclusion, each patient provided written informed consent. The exclusion criteria were refused consent, patients under guardianship, rectal cancers initially irradiated, adenomatous polyposis, inflammatory bowel disease (i.e., Crohn's disease or hemorrhagic rectocolitis), familial adenomatous polyposis, or Lynch syndrome. Data on patients' treatment were collected.

A total of 104 patients were included. The colorectal cancer group comprised 76 patients. A first colorectal biopsy was performed within the tumor area, and a second was performed within adjacent non-tumor (i.e., peritumor) tissues. Patients were eligible for inclusion in the colorectal cancer group if the histological findings confirmed the cancer as an adenocarcinoma, regardless of the tumor staging. The control group comprised 28 patients with occlusion or ischemic colons. Patients were eligible for inclusion in the control group if they underwent a colectomy for any etiology except colorectal cancer or inflammatory bowel diseases. Histological analysis of all colorectal biopsies included in this study was performed at the Anatomopathology Department.

Sampling and conservation of samples

The colorectal biopsies were transported to the Anatomopathology Department in sterile packaging without being fixed. The colectomies were put on a sterile sheet and manipulated with sterile and disposables scissors, pliers, and bistouries. Pieces of colectomy were opened following the central line of haustrations. In case of tumor invasion of this line, the tumor was avoided in order not to disseminate tumor cells remotely. For the patients in the colorectal cancer group, we performed a mucosal biopsy (about 1 cm 2 and 0.2 g) in the tumor area and in the adjacent non-tumor tissue; in the latter case, the biopsy was taken at least 10 cm away from the tumor tissue area. For the control group, one mucosal colic biopsy (about 1 cm 2 and 0.2 g) was performed. Consequently, three groups of biopsies were collected: (1) colorectal biopsies from tumor tissue, (2) colorectal biopsies from adjacent non-tumor tissue, and (3) colorectal biopsies from non-cancer patients (i.e., healthy tissue). Colorectal biopsies were rinsed thoroughly with sterile water, placed into sterile standard containers, and snap-frozen with liquid nitrogen at -196°C until later analysis.

Element analysis

To avoid classification bias, the multi-element analysis was performed in a blind manner by a technician. Acid digestion procedures are necessary to quantify elements in organic samples using atomic spectrometric methods such as inductively coupled plasma atomic emission spectrometry (ICP-AES). This mineralization step allows complete transfer of the analytes into solution, so that they can be dosed in liquid form. As a result, the goal of the digestion procedure is to obtain the complete dissolution of the analytes and complete decomposition of the organic matrix, while avoiding loss or contamination of analytes.

Each colorectal sample was thawed and weighed. For the acid digestion, biopsies were placed individually in a small Petri dish previously rinsed with 70% alcohol. First, a mechanical dissolution was performed by dilacerating biopsies with disposable sterile scalpels. Then 3 M HCl was introduced, and samples were incubated overnight under soft agitation. The next day, the supernatant and remaining tissue debris were placed into Salivex tubes for ICP-AES analysis. Tubes were heated on a hotplate (99°C) until all the liquid had evaporated. Finally, samples were put into suspension in 10 ml of 2 M HCl and preserved at 4°C until ICP-AES analysis. There was no further analytical dilution.

ICP-AES was used to quantify the concentrations of minor elements in each colorectal biopsy. Based on previously published data [START_REF] Bocca | Determination of 30 elements in colorectal biopsies by sector field inductively coupled plasma mass spectrometry: method development and preliminary baseline levels[END_REF] we investigated the presence of 15 elements. Each element has a specific limit of detection (LoD, concentration of elements expressed in parts per billion i.e. in ng per g of wet tissue): aluminum (LoD of 14.1 ng/g), boron (LoD of 1.5 ng/g), cadmium (LoD of 1.3 ng/g), chromium (LoD of 2.8 ng/g), copper (LoD of 2.4 ng/g), iron (LoD of 1 ng/g), magnesium (LoD of 0.1 ng/g), manganese (LoD of 0.2 ng/g), nickel (LoD of 4.1 ng/g), lead (LoD of 25.1 ng/g), selenium (LoD of 58.3 ng/g), silicon (LoD of 4.4 ng/g), titanium (LoD of 0.6 ng/g), vanadium (LoD of 3.6 ng/g), and zinc (LoD of 0.8 ng/g). Results of concentration of minor element in each colorectal biopsy are expressed in parts per million (i.e. ppm or µg of element per g of wet tissue). A negative control was performed for each series of analyses. This negative control aimed at evaluating the background noise due to the presence of metallic impurities into the biopsy tubes and all the devices in contact with the biopsy especially in the operating room (scalpel …) and/or the possible contamination of analytes during the acid digestion procedure just before the ICP quantification. This negative control can be a crucial step in order to differentiate the elements coming from colorectal biopsies from a possible pollution of samples during the analytical procedure.

Statistical analysis

Statistical analysis was performed on the elements that had detectable concentrations and were above the negative control. We compared the elemental fingerprints between three sets of biopsies: (1) healthy tissue versus tumor tissue, (2) tumor tissue versus adjacent non-tumor tissue, and (3) adjacent non-tumor tissue versus healthy tissue. The normality of the variable distribution was assessed with the Kolmogorov-Smirnov test. The median and mean concentrations that had a normal distribution were compared between groups with the Z-test, whereas the others were compared by using the Wilcoxon test for matched series and the Mann-Whitney test for independent series. The significance of relationships between variables was examined by using Student's t-test on the correlation coefficients. The comparison between colorectal cancer patients and the control group was performed with the Z-test or the Mann-Whitney test. For all analyses, a p value < 0.05 was considered to be significant.

Results

The characteristics of the two patient groups were comparable except for age (p < 0.001) (Table 1). The significant age difference between the two groups can be explained epidemiologically: the mean age of colorectal cancer patients is around 70 years (this study, 75 years), whereas it is around 55 years for occlusion or ischemic colons (control group mean, 60 years). In addition, the two groups had a similar proportion of males to females, and both reflected the fact that colorectal cancer as well as occlusion or ischemic colons are more prevalent in men than in women.

Among the 15 elements of interest, only B, Cr, Mg, Si, and Zn occurred at concentrations above the trace element quantification obtained for the negative control. For these 5 elements, the concentrations found in our study were 1 000 000 times the LoD for Mg, 10 000 times the LoD for Zn, 1000 times the LoD for Si and Cr, and 10 times the LoD for B. It should be noted that Cu and Fe were quantified but their median concentrations for all samples (4.5 [Interquartile Range = 3.8] µg/g and 89;2 [69.1] µg/g respectively) were found to be close to concentrations obtained in the negative control experiments (background noise) which make them impossible to interpret.

Concentrations in tumor tissue versus healthy tissue

A significantly higher Mg and Si concentrations were found in the colorectal tumor tissue than in the healthy tissue (Fig. 1, 2 and 3, Table 2). Although the Zn and Cr concentrations were also higher in the tumor tissue than in the healthy tissue, the differences were not significant (p = 0.51 and p = 0.30, respectively). Finally, the median concentration of B was lower than 0.5 µg/g in each group and was similar in the tumor and healthy tissues (p = 0.62).

Concentrations in tumor tissue versus adjacent non-tumor tissue

The Mg concentration was significantly greater in the tumor tissue than in the adjacent nontumor tissue, with median concentrations of 147.0 [52.2] and 114.6 [38.8] µg/g respectively (p = 0.0008: Fig. 2; Table 2). Zn was also higher in the tumor tissue than in the adjacent nontumor tissue; however the differences did not reach the level of significance (p = 0.1143). The Cr concentration followed an opposite trend: 7.9 [8.8] µg/g in the tumor tissue and 10.0 [9.1] µg/g in the adjacent non-tumor tissue (p = 0.0433). Si and B concentrations exhibited no significant difference between the two tissue types (p = 0.4445 and p = 0.6182, respectively).

Correlation analyses

Because there was a predictable difference of age between the two patient groups, we examined whether there was a link between the age of patients and the Mg, Zn, and Si concentrations. No relationship was noted for Mg, Cr or Si concentrations (Mg vs. age: r = 0.13, p = 0.18; Cr vs. age: r = -0.15, p = 0.14; Si vs. age: r = 0.1, p = 0.32), whereas a weak inverse correlation was found for Zn (r = -0.24, p = 0.01): the more a patient aged, the greater the Zn deficiency was (Fig. 4).

Discussion

The aim of our study was to evaluate the element distribution in colorectal adenocarcinomas, adjacent non-tumor tissues, and healthy controls. Among the 15 elements analyzed by ICP-AES, only B, Cr, Zn, Si, and Mg were found in colorectal tissue at clearly detectable concentrations. It should be noted that Cu and Fe were quantified but their concentrations were found to be close to concentrations obtained in the negative control experiments. Comparison between groups showed that patients with colorectal cancer had higher Mg, Zn, Si and Cr concentrations in their biopsies than others, even if these differences were only statistically significant for Mg and Si. The differences of concentration between colorectal tumor biopsies and adjacent non-tumor biopsies were clearly elementdependent. As a matter of fact Mg concentration was significantly higher in tumor biopsies while Cr was significantly lower. Besides, there were no significant statistical differences between Si and Zn concentration quantified in tumor tissues and adjacent non-tumor tissues .

However, a slight tendency seemed to indicate a Zn concentration higher in tumor biopsies than in adjacent non-tumor biopsies. Even if our study design does not allow us to draw conclusions about a possible involvement of Mg, Cr, Si and Zn elements in the development of colorectal tumor, the rise of their concentration in colorectal biopsies intrigues. Some other studies have already examined the element fingerprints of colorectal biopsies. Overall the amount of elements found in these studies was slightly higher than in ours. A possible explanation is that most studies worked on dry tissue while we worked on wet tissue. Bocca [START_REF] Bocca | Determination of 30 elements in colorectal biopsies by sector field inductively coupled plasma mass spectrometry: method development and preliminary baseline levels[END_REF] used ICP spectrometry to determine the concentrations of 30 elements in colorectal biopsies of healthy patients. Median Mg, Zn and Cr concentration were respectively 1090 µg/g; 86.5 µg/g and 343 ng/g. Lavilla et al. [START_REF] Lavilla | Elemental fingerprinting of tumorous and adjacent non-tumorous tissues from patients with colorectal cancer using ICP-MS, ICP-OES and chemometric analysis[END_REF] assayed 18 elements in biopsies from 38 patients with colorectal cancer, revealing that the tumor tissue may accumulate trace of minor elements, especially Mg (573 µg/g in tumor tissues vs. 296 µg/g in healthy controls). In Lavilla et al. study, there was no significative difference for Zn (90 µg/g in tumor tissue vs. 79 µg/g in healthy tissue). Their findings are consistent with our results.

Alimonti et al. [START_REF] Alimonti | A study on metals content in patients with colorectal polyps[END_REF] examined the involvement of metals in colorectal polyps and found that Mg median concentration (from 1045 to 1283 µg/g) and Zn median concentration (89 to 102 µg/g) were not significantly different between polypes, adjacent non-polype tissues and healthy controls. Although, Cr has only been found at trace level, it was significantly lower in polype than in adjacent non-polype tissues (455 vs. 163 ng/g). In two different studies, Kucharzewski et al. determined the concentrations of Fe, Se, Zn and Cu in colorectal polype and cancer. They found that Fe and Zn mean concentration were higher in cancer than in polype (46.1 µg/g vs. 43.2 µg/g and 14.8 µg/g vs. 9.84 µg/g respectively). Overall, the results of those previous studies are quite consistent with ours.

Several Japanese studies revealed that a diet with a low Mg content is a potential risk factor of colon cancer, although the results were not significant for rectum cancers [START_REF] Ma | High dietary intake of magnesium may decrease risk of colorectal cancer in Japanese men[END_REF][START_REF] Folsom | Magnesium intake and reduced risk of colon cancer in a prospective study of women[END_REF][START_REF] Kuo | Magnesium in drinking water modifies the association between trihalomethanes and the risk of death from colon cancer[END_REF][START_REF] Kuo | Trihalomethanes in drinking water and the risk of death from rectal cancer: does hardness in drinking water matter?[END_REF][START_REF] Qu | Nonlinear association between magnesium intake and the risk of colorectal cancer[END_REF]. Similar results were observed on the impact of Mg concentration in drinking water [START_REF] Chiu | Colon cancer and content of nitrates and magnesium in drinking water[END_REF][START_REF] Yang | Colon cancer mortality and total hardness levels in Taiwan's drinking water[END_REF], whereas another study found no such influence of Mg on colorectal adenoma [START_REF] Alimonti | A study on metals content in patients with colorectal polyps[END_REF]. Studies on mice using a diet supplemented with Mg found a protective role of Mg, as an antioxidant that inhibits oncogenes [START_REF] Tanaka | Inhibitory effect of magnesium hydroxide on methylazoxymethanol acetate-induced large bowel carcinogenesis in male F344 rats[END_REF]. A meta-analysis of studies (8000 colorectal cancers in 338,797 patients) suggested a protective effect of Mg in colon cancers, although those results were not significant for rectal cancers [START_REF] Chen | Magnesium intake and risk of colorectal cancer: a meta-analysis of prospective studies[END_REF]. However, the role of Mg could be complex, with a protective effect at the beginning of carcinogenesis and a pro-oncogenic role at the ultimate stages promoting cellular division [START_REF] Hartwig | Role of magnesium in genomic stability[END_REF]. We know that the dissemination of neoplastic cells during surgery can lead to the development of metastasis via the adhesion of cells. This adhesion process is principally induced by integrins and matrix receptors that are influenced by divalent cations. A study suggested that the high content of Mg 2+ in endogenous wound fluid may potentiate tumor cell adhesion, whereas Ca 2+ may inhibit it [START_REF] Van Der Voort Van Zyp | Divalent cations influence colon cancer cell adhesion in a murine transplantable tumor model[END_REF]. Consequently, it was proposed that irrigating with dilute CaCl 2 could decrease local tumor recurrence by inhibiting the adhesion of tumor cells. Another explanation of the abundance of Mg in colorectal tumor could be an accumulation of Mg due to the cancerous process. In this case, Mg accumulation would be a consequence of the cancer not a cause.

Few studies have examined Zn profiles. Our results suggest a correlation between Zn concentration and the age of patients, and indeed Zn deficiency is more frequent in the elderly [START_REF] Meunier | Importance of zinc in the elderly: the ZENITH study[END_REF]. According to a literature review, the role of Zn in carcinogenesis is not well understood [START_REF] John | Diverse sensitivity of cells representing various stages of colon carcinogenesis to increased extracellular zinc: implications for zinc chemoprevention[END_REF]. Some authors proposed that Zn is not related to colorectal cancer [START_REF] Hara | Zinc and heme iron intakes and risk of colorectal cancer: a population-based prospective cohort study in Japan[END_REF], others that Zn could inhibit the growth of neoplastic cells [START_REF] Cilla | Polyphenolic profile and antiproliferative activity of bioaccessible fractions of zinc-fortified fruit beverages in human colon cancer cell lines[END_REF][START_REF] Christudoss | Zinc and zinc related enzymes in precancerous and cancerous tissue in the colon of dimethyl hydrazine treated rats[END_REF] and others found higher Zn blood concentrations in rats with colorectal cancer [START_REF] Gupta | Serum and tissue trace elements in colorectal cancer[END_REF]. Carter et al. showed that a diet low in Zn favors the development of adenoma and non-invasive cancers, whereas a diet enriched in Zn favors the development of invasive cancers [START_REF] Carter | Zinc deprivation promotes progression of 1,2-dimethylhydrazine-induced colon tumors but reduces malignant invasion in mice[END_REF]. The etiologic relationship could not be demonstrated, but the main assumptions concern the role of Zn in regulating oxidative stress and cell division, proliferation, and DNA replication. In the same way as for magnesium, the design of our study does not allow us to judge if the elevation of Zn in the tumor is a cause or a consequence of the colorectal cancer development. Indeed, it has been shown that metallothionein which bind Zn accumulate in rapidly proliferating human colonic cancer cells [START_REF] Nagel | Cell cycle regulation of metallothionein in human colonic cancer cells[END_REF].

The different elements found in colon biopsies could be from endogenous (e.g., ions from metabolic and physiological processes) or exogenous sources (e.g., inorganic and nonbiodegradable pollutants of environmental origin). Whereas Zn and Mg could be from endogenous sources, Si and Cr are more probably of exogenous origin. Indeed silica (silicon dioxide) is a common additive in the production of foods, and colloidal silica is also used as a wine, beer, and juice fining agent. Moreover, the detection of Si could suggest a potential role of exogenous micro-or nanoparticles in diseases that usual histopathology exams not take into account. In this context, exposure to ultra-fine particles could be of interest. As a matter of fact, ultra-thin particles are toxicants present in air pollution contributing to asthma, cardiovascular disease, and overall mortality [START_REF]Baseline Scenarios for the Clean Air For Europe (CAFE) Programme[END_REF]. Significant quantities of titanium dioxide and silicon dioxide are swallowed, both as natural contaminants of food and as additives.

More than 10 12 mineral particles per day are ingested, and it is possible that the ingested elements are not as innocuous as we have assumed [START_REF] Gatti | Biocompatibility of micro-and nano-particles in the colon. Part II[END_REF][START_REF] Schneider | Can microparticles contribute to inflammatory bowel disease: innocuous or inflammatory?[END_REF][START_REF] Buzea | Nanomaterials and nanoparticles: sources and toxicity[END_REF][START_REF] Urban | Dissemination of wear particles to the liver, spleen, and abdominal lymph nodes of patients with hip or knee replacement[END_REF][START_REF] Lomer | Fine and ultrafine particles of the diet: influence on the mucosal immune response and association with Crohn's disease[END_REF]. Recent studies have shown that the accumulation of debris from dental prostheses could cause multi-organ parenchymal granulomatosis [START_REF] Ballestri | Liver and kidney foreign bodies granulomatosis in a patient with malocclusion, bruxism, and worn dental prostheses[END_REF], and several studies have described a relationship between debris from hip prosthesis and local inflammatory reaction with granulomatosis [START_REF] Al-Saffar | Pathology of the bone-implant interfaces[END_REF][START_REF] Revell | Biological reaction to debris in relation to joint prostheses[END_REF]. Finally, some other studies, showed that the composition of drinking water and diet with higher or lower concentrations of elements such as Mg, Fe, Cr or Zn can be associated with colorectal cancer [START_REF] Kuo | Magnesium in drinking water modifies the association between trihalomethanes and the risk of death from colon cancer[END_REF][START_REF] Schneider | Can microparticles contribute to inflammatory bowel disease: innocuous or inflammatory?[END_REF][START_REF] Nelson | Dietary iron and colorectal cancer risk[END_REF][START_REF] Thompson | Investigation of the mode of action underlying the tumorigenic response induced in B6C3F1 mice exposed orally to hexavalent chromium[END_REF][START_REF] Wang | Arsenic and chromium in drinking water promote tumorigenesis in a mouse colitis-associated colorectal cancer model and the potential mechanism is ROS-mediated Wnt/β-catenin signaling pathway[END_REF].

Conclusion

Although alterations in element homeostasis and the etiology of cancer are of great interest, the elemental distribution in human colorectal biopsies remains unclear. This study demonstrated that various types of colorectal biopsies have specific elemental fingerprints.

We observed significantly higher Mg concentration and a nearly significantly higher Zn concentration in adenocarcinoma tissues than in adjacent non-tumor tissues, as well as higher Si and Cr concentrations in colorectal cancer than in healthy non-cancer biopsies. Mg and Zn

Figure 1 :Figure 3 :

 13 Figure 1: Median concentrations of Mg, Zn, Si and Cr expressed in µg of element per g of

Figure 4 :

 4 Figure 4: Correlation graph showing a weak inverse correlation between Zn concentration in

Table 1 .

 1 Patient characteristics of the two groups (pTNM: size, nodes, metastasis from the internal classification of tumors; PY: pack-years)

	Characteristics		Colorectal	Control
			cancer
	Sex	Male	54%	54%
		Female	46%	46%
	Mean age (years)		75 +/-11	60 +/-15
	Differentiation	Poor	13%
		Medium	46%
		Well	33%
		Undefined	8%
	pTNM	T1	9%
		T2	20%
		T3	46%
		T4	25%
		Tx	0
		N0	62%
		N1	22%
		N2	16%
		Nx	0
		M0	58%
		M1	34%
		Mx	8%
	Tobacco	N	41%	50%
		Mean consumption in PY	31 +/-21	28 +/-27
	Alcohol	N	33%	29%
		Mean drink (g/day)	55 +/-41	31 +/-28

could be from endogenous sources, whereas Si and Cr may be from exogenous sources.

Further clinical trials should be dedicated to investigating the impact of Zn, Si, Cr and Mg at the different steps of the adenoma-carcinoma sequence. Finally, the distribution of chemical elements in colorectal polyps should be investigated as well.


Guillaume Bury
email: guillaume.bury@inria.fr

David Delahaye
email: david.delahaye@cnam.fr

Integrating Simplex with Tableaux

Keywords: Tableaux, Linear Arithmetic, General Simplex Algorithm, Branch and Bound Method, Proof Checking, Zenon, Coq

We propose an extension of a tableau-based calculus to deal with linear arithmetic. This extension consists of a smooth integration of arithmetic deductive rules to the basic tableau rules, so that there is a natural interleaving between arithmetic and regular analytic rules. The arithmetic rules rely on the general simplex algorithm to compute solutions for systems over rationals, as well as on the branch and bound method to deal with integer systems. We also describe our implementation in the framework of Zenon, an automated theorem prover that is able to deal with first order logic with equality. This implementation has been provided with a backend verifier that relies on the Coq proof assistant, and which can verify the validity of the generated arithmetic proofs. Finally, we present some experimental results over the arithmetic category of the TPTP library, and problems of program verification coming from the benchmark provided by the BWare project.

Introduction

Program analysis and verification often involve to verify arithmetic constraints. For example, this is the case when verifying loop invariants over imperative programs. In general, these arithmetic constraints are not very complex, but they lie in more complex first order formulas where pure first order logic and arithmetic are actually mixed. To deal with this kind of formulas, we propose, in this paper, to integrate arithmetic reasoning with a tableau-based proof search method. Regarding the nature of arithmetic reasoning, we consider the linear fragment, also known as Presburger arithmetic (where we only consider the addition operation and equality), which is weaker than Peano arithmetic but has the advantage to be decidable. There exist several decision procedures for linear arithmetic, and we chose to rely on the general simplex algorithm [START_REF]Linear Programming[END_REF] (i.e. the usual simplex algorithm but without considering the optimization problem) to compute solutions for problems over rationals, as well as on the branch and bound method to deal with integer problems. This work is motivated by needs that arose in the framework of the BWare project [START_REF] Delahaye | The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations[END_REF][START_REF]The BWare Project[END_REF]. This project aims to provide a mechanized framework to support the automated verification of proof obligations coming from the development of industrial applications using the B method [START_REF] Delahaye | The B-Book: Assigning Programs to Meanings[END_REF] and requiring high integrity. The methodology used in this project consists in building a generic platform of verification relying on different automated theorem provers, such as first order provers and SMT (Satisfiability Modulo Theories) solvers. Among the considered provers, there is Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF], which is an automated theorem prover for classical first order logic with equality, and which is based on the tableau method. As Zenon is not able to deal with arithmetic, which may be required when verifying some proof obligations (involving mainly integer arithmetic in the benchmark of BWare), this is why we proposed to develop an extension of this tool to arithmetic, which will be described in this paper. This extension modifies not only the proof search rules of the prover, but also the backend as Zenon is able to produce proofs checkable by external tools, such as Coq [START_REF]Coq, version 8.4pl6[END_REF] for instance. This backend is part of the objectives of the BWare project, which requires the verification tools to produce proof objects that are to be checked independently.

To extend Zenon to arithmetic, the idea is to add new specific rules, which are completely orthogonal to the other usual analytic rules of tableaux, and which use the computations performed by the simplex procedure as oracles. These rules are intended to deal with arithmetic formulas that are universally quantified. As for arithmetic formulas that are existentially quantified, no new rule is needed, but the instantiation mechanism has to be modified in order to call the simplex procedure to find instantiations. However, these instantiations must help us close all the branches of the proof search tree and not only a part of them (this is not unsound but does not help us find a proof). To do so, we introduce a notion of arithmetic constraint tree, which is a tree labeled with sets of arithmetic formulas, and which is built from the proof search tree. From this arithmetic constraint tree, a set of formulas is selected in order to cover the tree, i.e. it is sufficient to find a solution for this set of formulas (its negation to be more precise) to get a solution that closes the arithmetic constraint tree and therefore the proof search tree. It should be noted that our extension is able to deal with pure universal or existential arithmetic formulas, i.e. we do not consider alternation of universal and existential quantifiers and the variables occurring in an arithmetic formula must be of the same nature (either Skolem symbols or free variables). It should also be noted that as Zenon deals with equality, the arithmetic reasoning can be naturally combined with the equational reasoning involving both uninterpreted functions and predicates. This paper is organized as follows: in Secs. 2 and 3, we first introduce respectively the proof search method of Zenon and the general simplex algorithm, as well as the branch and bound method; we then present, in Secs. 4 and 5, the arithmetic rules for Zenon and describe how the instantiation has to be modified to handle arithmetic; finally, in Sec. 6, we provide an overview of our implementation and the experimental results obtained on the benchmarks provided by the TPTP library and the BWare project, and propose some related work in Sec. 7.

The Zenon automated theorem prover relies on a tableau-based proof search method for classical first order logic with equality. The proof search rules of Zenon are described in detail in [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] and summarized in Fig. 1 (for the sake of simplification, we have omitted the unfolding and extension rules), where is Hilbert's operator ( (x).P (x) means some x that satisfies P (x), and is considered as a term), capital letters are used for metavariables, and R r , R s , R t , and R ts are respectively reflexive, symmetric, transitive, and transitive-symmetric relations (the corresponding rules also apply to the equality in particular). As hinted by the use of Hilbert's operator, the δ-rules are handled by means of -terms rather than using Skolemization. What we call here metavariables are often named free variables in the tableau-related literature; they are not used as variables as they are never substituted. The proof search rules are applied with the normal tableau method: starting from the negation of the goal, apply the rules in a top-down fashion to build a tree. When all branches are closed (i.e. end with an application of a closure rule), the tree is closed, and this closed tree is a proof of the goal. Note that this algorithm is applied in strict depth-first order: we close the current branch before starting work on another branch. Moreover, we work in a non-destructive way: working on one branch will never change the formulas of any other branch. We divide these rules into five distinct classes to be used for a more efficient proof search. This extends the usual sets of rules dealing with α, β, δ, γ-formulas and closure ( ) with the specific rules of Zenon. We list below the five sets of rules and their elements:

α α ¬∨ , α ∧ , α ¬⇒ , α ¬¬ , ¬ refl β β ∨ , β ¬∧ , β ⇒ , β ⇔ , β ¬⇔ , pred, fun, sym, trans * δ δ ∃ , δ ¬∀ γ γ ∀M , γ ¬∃M , γ ∀inst , γ ¬∃inst , ⊥ , , r , s
where "trans * " gathers all the transitivity rules.

To deal with arithmetic formulas, we use the ability of Zenon to perform typed proof search, which relies on a polymorphic type system. To simplify, we do not consider types in our presentation of Zenon and its extension to arithmetic, as they tend to make the presentation uselessly heavy since, in our case, types are actually just used to distinguish arithmetic formulas from the other ones.

The Simplex and the Branch and Bound Methods

We define linear arithmetic expressions as expressions built using addition and multiplication by numeric constants, while subtraction is seen as syntactic sugar for addition with multiplication by a negative constant. An arithmetic formula is a comparison of two linear arithmetic expressions, for example 2x + 1 < 7 -1 2 y. We consider 5 comparison operators, i.e. =, <, >, ≤, and ≥ 1 . An arbitrary comparison operator distinct from the equality may be noted , and its negation , with the following correspondence: < ≡ ≥, ≤ ≡ >, > ≡ ≤, and ≥ ≡ <.

¬(P ⇔ Q) β¬⇔ ¬P, Q | P, ¬Q P ∧ Q α∧ P, Q ¬(P ∨ Q) α¬∨ ¬P, ¬Q ¬(P ⇒ Q) α¬⇒ P, ¬Q P ∨ Q β∨ P | Q ¬(P ∧ Q) β¬∧ ¬P | ¬Q P ⇒ Q β⇒ ¬P | Q ∃x.P (x) δ ∃ P ( (x
(u, v) sym t = u | s = v ¬Rr(s, t) ¬ refl s = t Rt(s, t) ¬Rt(u, v) trans u = s, ¬Rt(u, s) | t = v, ¬Rt(t, v) Rts(s, t) ¬Rts(u, v) transsym v = s, ¬Rts(v, s) | t = u, ¬Rts(t, u) s = t ¬Rt(u, v) transeq u = s, ¬Rt(u, s) | ¬Rt(u, s), ¬Rt(t, v) | t = v, ¬Rt(t, v) s = t ¬Rts(u, v) transeqsym v = s, ¬Rts(v, s) | ¬Rts(v, s), ¬Rts(t, u) | t = u, ¬Rts(t, u)
In the following, arithmetic expressions can involve integers, rationals, or reals2 . However, we do not consider mixed problems, and assume that a given problem only involves one numeric type (either integers, rationals, or reals).

As a solving method, we consider the general simplex, as described in [START_REF] Kroening | Decision Procedures: An Algorithmic Point of View[END_REF], which is a variant of the simplex algorithm, designed to solve the satisfiability problem on linear systems, rather than the optimization of a given objective function under a system of constraints.

The general simplex accepts only two forms of constraints: equations of the form v = i a i x i , with a i ∈ Q, and bounds on variables

l i ≤ v ≤ u i , with l i , u i ∈ Q ∪ {-∞, +∞}.
A system that contains only formulas of either form is said to be in general form. This representation does not restrict expressivity, given that any linear system can be translated into this representation. To do so, two transformations are required:

1. Any equality e = e , where neither e nor e is a variable, is replaced by e ≤ e ∧ e ≤ e; 2. Any comparison e e is rewritten as f k, where f is a non-empty sum of variables with coefficients3 , and k a numeric constant, s.t. e-e = f -k. The comparison can then be replaced by x = f ∧ x k, with x a fresh variable.

This transformation into general forms allows us to get an interesting property of the system: all variables on the left-hand side of equalities do not appear on the right-hand side of equalities. In the following, we suppose that all general forms satisfy this property, i.e we only consider general forms that come from the application of the process described above to a linear system.

The simplex method performs a series of pivot operations over the system4 , and stores the result in an internal state. This internal state allows the algorithm to be incremental, i.e we can easily add new equalities and bounds to this state, and get a new state that we can try to solve. When the given system is satisfiable, the simplex algorithm returns its new state together with a solution, and it is straightforward to check that it is a correct solution of the linear system. When the algorithm meets an unsatisfiable system S, it returns an equality x = i a i y i , which is implied by the equalities in S, s.t. the following properties hold5 :

-There exists l (resp. u)

s.t. x ≥ l ∈ S (resp. x ≤ u ∈ S); -There exist numeric constants l i , u i s.t. for all i, if a i > 0, then y i ≤ u i ∈ S (resp. y i ≥ l i ∈ S), and if a i < 0, then y ≥ l i ∈ S (resp. y i ≤ u i ∈ S); - ai>0 a i u i + ai<0 a i l i < l (resp. u < ai>0 a i l i + ai<0 a i u i ), resulting in a contradiction, since l ≤ x = i a i y i ≤ ai>0 a i u i + ai<0 a i l i (resp. ai>0 a i l i + ai<0 a i u i ≤ i a i y i = x ≤ u) should hold according to S.
In order to deal with integer systems, we adopt a branch and bound strategy. An integer linear system can be seen as a rational system where all variables are required to have an integer value. For this reason, we can accept rational coefficients in the system: given a constraint with rational coefficients, we multiply it by the least common multiple of the denominators of the coefficients in order to get an equivalent constraint with only integer coefficients. Given an integer system S, we call relaxed system of S, noted relaxed(S), the system S without the condition that the variables must have an integer assignment.

Given a system S, the branch and bound algorithm works as follows:

-If relaxed(S) is unsatisfiable (as a rational system), then return false; -If the system has a rational solution then:

• If all the variables have an integer assignment, then return true;

• If a non-integer value v is assigned to an integer variable x, then call the branch and bound twice with the two systems S ∪ {x ≤ v } and S ∪ {x ≥ v + 1}, and return the disjunction of the two returned values.

Unfortunately, this algorithm is not complete: if we consider the system 1 ≤ 3x + 3y ≤ 2, the branch and bound algorithm will loop. More generally, the branch and bound will not terminate on unsatisfiable integer systems with unbounded rational solutions (but no integer solution). However, if the system is satisfiable, then a solution will be found by the algorithm, provided that we use a breadth-first search.

To ensure termination, we can use global bounds, as found in [START_REF] Nemhauser | Integer and Combinatorial Optimization[END_REF]. Given an m × n rational matrix A = (a i ), a vector b ∈ Q m , and the set of rational solutions P = {x ∈ Q | Ax ≤ b}, if the set of integer solutions S = P ∩ Z n is non-empty, then there exists an integer solution x ∈ S s.t.

|x j | ≤ ω A,b for all 1 ≤ j ≤ n, with ω A,b = (2n 2 θ) n
, where n = max(n, m) and θ = max ij (|a ij |).

Arithmetic Proof Search Rules

In this section, we present the arithmetic proof search rules for Zenon, which rely on the simplex and branch and bound methods, and discuss the soundness and completeness of these rules.

Rules

The arithmetic proof search rules for Zenon are summarized in Fig. 2. These rules do not use global bounds because in practice, these bounds grow too quickly to be useful on non-trivial systems. Among these rules, there are two rules, i.e. Branch and Simplex-Lin, which need parameters and therefore require the proof

Branch x an integer variable, k ∈ Z x ≤ k | x ≥ k + 1 e1 = 0, . . . , en = 0 Simplex-Lin ∀i, ai ∈ Q n i=1 aiei = 0 x ≤ k, x ≥ k Conflict k < k numeric constants {xj ≤ uj | j ∈ N + }, {xj ≥ lj | j ∈ N -}, x = j∈N + ∪N -ajxj Leq x ≤ j∈N + ajuj + j∈N -ajlj {xj ≥ lj | j ∈ N + }, {xj ≤ uj | j ∈ N -}, x = j∈N + ∪N -ajxj Geq x ≥ j∈N + ajlj + j∈N -ajuj
where aj > 0, if j ∈ N + , and aj < 0, if j ∈ N - Fig. 2. Proof Search Rules for Arithmetic search method to choose these parameters. In the following, we describe how Zenon relies on the branch and bound method to make use of these rules.

Each time Zenon processes a new formula, there are two cases. Either the formula is a bound on a variable, in which case it is simply added to the current simplex state. Or it is not, and the rule Var can be applied so that a new variable is generated, and the resulting constraints (which are in general form) can be added to the current simplex state. For every addition to the simplex state, Zenon tries to solve the system of the simplex state. If this yields an unsatisfiable statement, then the explanation is translated into proof search rules and introduced in the proof search tree, effectively closing the current branch. Thanks to the fact that the simplex is incremental, we have a persistent simplex state, which allows us to keep all the work previously done up to a point when the proof search tree branches.

When the simplex algorithm returns an unsatisfiability explanation of the form x = i a i y i , we use three proof nodes to close the current branch. First, we use the Simplex-Lin rule to introduce the formula xi a i y i = 0. We can

¬∀u ∈ Z.∀v ∈ Z.∀w ∈ Z.2u + v + w = 10 ∧ u + 2v + w = 10 ⇒ w = 0 δ ¬∀ ¬∀v ∈ Z.∀w ∈ Z.2 0 + v + w = 10 ∧ 0 + 2v + w = 10 ⇒ w = 0 δ ¬∀ ¬∀w ∈ Z.2 0 + 1 + w = 10 ∧ 0 + 2 1 + w = 10 ⇒ w = 0 δ ¬∀ ¬(2 0 + 1 + 2 = 10 ∧ 0 + 2 1 + 2 = 10 ⇒ 2 = 0) β¬⇒ 2 0 + 1 + 2 = 10 ∧ 0 + 2 1 + 2 = 10, ¬¬ 2 = 0 α∧ 2 0 + 1 + 2 = 10, 0 + 2 1 + 2 = 10 ᬬ 2 = 0 Eq 2 0 + 1 + 2 ≤ 10, 2 0 + 1 + 2 ≥ 10 Var a = 2 0 + 1 + 2, a ≤ 10 Var b = 2 0 + 1 + 2, b ≥ 10 Eq 0 + 2 1 + 2 ≤ 10, 0 + 2 1 + 2 ≥ 10 Var c = 0 + 2 1 + 2, c ≤ 10 Var d = 0 + 2 1 + 2, d ≥ 10 Eq 2 ≤ 0, 2 ≥ 0 Branch 1 ≤ 3 Simplex-Lin a = 2d -3 1 -2 Geq a ≥ 11 Conflict 1 ≥ 4 Simplex-Lin c = 1 2 b + 3 2 1 + 1 2 2

Geq c ≥ 11

Conflict where:

0 = (u).¬∀v ∈ Z.∀w ∈ Z.2u + v + w = 10 ∧ u + 2v + w = 10 ⇒ w = 0 1 = (v).¬∀w ∈ Z.2 0 + v + w = 10 ∧ 0 + 2v + w = 10 ⇒ w = 0 2 = (w).¬(2 0 + 1 + w = 10 ∧ 0 + 2 1 + w = 10 ⇒ w = 0) Fig. 3. Proof of Problem ARI178=1
then use either the Leq or Geq rules to deduce a new bound on x using the equality x = i a i y i (which is equivalent to xi a i y i = 0 using some simple rewrite rules; see the next paragraph). Finally, we use the Conflict rule to close the tree, since the simplex guarantees that the newly deduced bound will be in direct conflict with a pre-existing bound of x. For integer systems, the branch and bound strategy returns a tree where nodes are split cases on integer variables, i.e. choices of the form x ≤ k ∨ x ≥ k + 1 (see Sec. 3), and leaves are usual simplex explanations. This structure can be easily translated into proof search rules using the Branch rule and the explanation in three steps for the simplex.

It should be noted that the equalities involved in the premises of the arithmetic proof search rules are either of the form e = 0, where e is an expression (see the Simplex-Lin rule), or of the form x = e, where x is a variable and e an expression (see the Leq and Geq rules). This means that the equalities of the premises must be seen modulo rewriting over a ring structure, which mainly consists in factorizing multiplicative coefficients of expressions (usually variables), computing the result of constant expressions, and moving an expression from one side of a comparison to the other side. In order to keep a compact proof search tree, these steps of rewriting are not included in the tree (but should be considered when producing a proof object to be checked by an external tool).

As an example of proof with these rules, let us consider the following formula, which comes from the ARI178=1 problem of the ARI category (which is the arithmetic category) of the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF]:

∀u ∈ Z.∀v ∈ Z.∀w ∈ Z.2u + v + w = 10 ∧ u + 2v + w = 10 ⇒ w = 0
Using the proof search rules of Fig. 2, we can obtain the proof of Fig. 3, where the parameters for the Branch rule come from the application of the branch and bound algorithm (see Sec. 3).

Soundness

Provided their side conditions are met, the rules presented in Fig. 2 are sound for integer, rational, and real arithmetic. The proof is trivial for all the rules, except for the following rules, which perform more complicated operations:

-Simplex-Lin, which introduces a linear combination of equalities; -Conflict, which uses transitivity of orders, e.g. a ≤ x ∧ x < b ⇒ a < b, and applies the comparison of ground numeric constants; -Leq and Geq, for which we need the compatibility of addition and multiplication with orders, e.g.

x ≤ a ∧ y ≥ b ⇒ 2x -y ≤ 2a -b.

Completeness

The set of rules of Fig. 2 is complete for the satisfiability of rational and real linear arithmetic systems, but not for integer systems since we do not use global bounds (which ensure the termination of the branch and bound algorithm).

Completeness for rational arithmetic comes from the termination and soundness of the simplex algorithm. For real arithmetic, since most of the input languages for automated theorem provers only allow real numeric constants to be rationals 6 , we can consider the restriction of a real system S to the rationals and try to solve it with the simplex method, which appears to be complete in this particular case. In fact, there are two possibilities: either the simplex finds a rational solution, then it is also a real solution; or the simplex finds the real system to be unsatisfiable, then we can build a proof search tree using our rules (which are sound for real arithmetic), which proves that the real system is unsatisfiable.

Using simplex optimizations such as Gomory's cuts [START_REF] Gomory | An Algorithm for Integer Solutions to Linear Problems[END_REF], which reduce the search space, would require to complicate the explanation procedure, i.e the procedure that translates an unsatisfiable result from the simplex into a proof search tree. It might also require to add new arithmetic rules in order to keep the proof search tree as simple as possible. This is why no optimization of the simplex has been considered yet.

Arithmetic Instantiation Mechanism

In order to find instantiations leading to contradictions, we try to find instantiations that satisfy a selected set of formulas. To do so, we introduce arithmetic constraint trees and the notion of counter-example for these trees.

Arithmetic Constraint Trees

Arithmetic constraint trees (referred to as trees in the following) and the notion of counter-example for these trees are defined as follows:

Definition 1 (Arithmetic Constraint Trees). An arithmetic constraint tree is a tree whose nodes and leaves are labeled with sets of arithmetic formulas.

Definition 2 (Cover of Nodes of a Tree). Given a tree T , and a set of formula E, the set of nodes of T covered by E is the least set of nodes N s.t. for all n ∈ N , either label(n) ∩ E = ∅, where label(n) is the set of formulas labeling the node n, or all children of N are covered by E.

Definition 3 (Cover of a Tree).

A set of formulas E is said to cover a tree T iff the root of T belongs to the set of nodes covered by E.

Definition 4 (Counter-Example of a Tree).

A counter-example of a tree T is an assignment of the metavariables of T s.t. there exists a set of formulas E that covers T and s.t. all the negation of the formulas of E are satisfied.

In order to find a counter-example of an arithmetic constraint tree T , we simply need to solve the negation of a system (a set of formulas) that covers T . To do so, we enumerate a sufficient set of systems that covers T and try to solve each of them until we find a counter-example. We can enumerate a sufficient set of covering sets with the following formula:

cover(T ) = {{f } | f ∈ label(T )} ∪ { 1≤i≤n s i | s i ∈ cover(T [i])}
where label(T ) is the label of the root of T , and T [i] the i-th children of the root of T . This set is sufficient in the sense that any cover set of a tree T must be a superset of at least one set in cover(T ).

Interleaving with Zenon

In Zenon, a proof search tree can be seen as a tree labeled with sets of formulas. To use this tree to find instantiations, we first have to allow Zenon to return a tree with open branches in the case where it did not find any contradiction. We then filter all the formulas in the tree, and keep only the arithmetic constraints to build an arithmetic constraint tree. Finally, we try to find a counter-example of this tree, and once found, we can prove the initial formula by using the γ ∀inst Open Proof Search Tree and γ ¬∃inst rules (see Fig. 1) to instantiate the metavariables with the values of the counter-example. Let us illustrate this mechanism with an example:

¬∃x ∈ Z.(x ≥ 0 ∨ x ≥ 1) ∧ (x ≥ -5 ∧ x ≤ 0) γ ¬∃M ¬((X ≥ 0 ∨ X ≥ 1) ∧ (X ≥ -5 ∧ X ≤ 0)) β¬∧ ¬((X ≥ 0 ∨ X ≥ 1)) α¬∨ ¬(X ≥ 0), ¬(X ≥ 1) Neg(≥) X < 0 Int-Lt X ≤ -1 * Neg(≥) X < 1 Int-Lt X ≤ 0 * ¬(X ≥ -5 ∧ X ≤ 0) β¬∧ ¬(X ≥ -5) Neg(≥) X < -5 Int-Lt X ≤ -6 * ¬(X ≤ 0) Neg(≤) X > 0 Int-Gt X ≥ 1 * Arithmetic Constraint Tree [] [X ≤ -1 † ; X ≤ 0] [] [X ≤ -6 † ] [X ≥ 1 † ] Closed Proof Search Tree ¬∃x ∈ Z.(x ≥ 0 ∨ x ≥ 1) ∧ (x ≥ -5 ∧ x ≤ 0) γ ¬∃Inst ¬((0 ≥ 0 ∨ 0 ≥ 1) ∧ (0 ≥ -5 ∧ 0 ≤ 0)) β¬∧ ¬((0 ≥ 0 ∨ 0 ≥ 1)) α¬∨ ¬(0 ≥ 0), ¬(0 ≥ 1) Neg(≥) 0 < 0 Const ¬(0 ≥ -5 ∧ 0 ≤ 0) β¬∧ ¬(0 ≥ -5) Neg(≥) 0 < -5 Const ¬(0 ≤ 0) Neg(≤) 0 > 0 Const
∃x ∈ Z.(x ≥ 0 ∨ x ≥ 1) ∧ (x ≥ -5 ∧ x ≤ 0) (1)
To prove this formula, we first consider its negation, then decompose it using the proof search rules to obtain the open proof search tree of Fig. 4. From this tree, we can get the arithmetic constraint tree of Fig. 4 by keeping the formulas of the open proof search tree that are labeled with "*", and by collapsing the empty nodes. During the enumeration of covering sets, we reach the set S that contains the formulas that are labeled with " †" in the arithmetic constraint tree. We can then solve the system that is formed by the negation of the formulas in S, and which yields the counter-example X → 0. Finally, we can produce the closed proof search tree of Fig. 4 by instantiating X by 0.

With this mechanism, Zenon alternates between regular proof search with the usual proof search rules, and arithmetic solving over open proof search trees to get counter-examples that provide instantiations to close the proof search trees. This approach is sound as instantiations cannot introduce inconsistencies. This approach is also complete for the validity of purely existential arithmetic formulas, where all the variables are existentially quantified 7 . Given such a formula, if the negation of this formula is unsatisfiable, then there exists a substitution σ of the variables s.t. the resulting ground formula is unsatisfiable. Since the formula is ground, it means that after applying the propositional proof search rules, we have a tree T s.t. there is an unsatisfiable comparison of numeric constants in each branch of the proof search tree. The substitution σ is a counter-example of T , with a covering set E s.t. each comparison e f ∈ E is absurd after substitution by σ. Our enumeration of potential covering sets is s.t. there exists E ∈ cover(T ) s.t. E ⊆ E. This means that there is a counter-example σ of T , with the covering set E s.t. it also closes all branches after substitution, and σ will be found during the proof search since the branch and bound always terminates when there exists a solution.

Limitations of the Simplex Method

The main limitation of the simplex method is that it is not able to perform abstract computations, i.e. it is only able to handle numeric constants. For instance, if we want to prove the formula ∃x ∈ Q.x ≤ a, where a is a rational constant, we cannot feed the simplex with the formula X ≤ a, where X is the metavariable corresponding to the existential variable x, because in this context, X and a are fundamentally different: we cannot change the value of a, while we can choose the value of X, but the simplex is not able to make this difference. By extension, this prevents us from dealing with formulas containing both metavariables and -terms, and therefore with formulas involving alternations of quantifiers.

Experimental Results and Proof Certification

We have implemented our extension of Zenon to arithmetic according to what is described in Secs. 4 and 5, using arbitrary precision rationals through the Zarith OCaml library 8 , and we have performed some tests using problems from the ARI category (i.e. the arithmetic category) of the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF]. We consider 500 problems of this category that only involve linear arithmetic. These tests have been run on an Intel Xeon E5-2660 v2 2.20GHz computer, with a timeout of 60 s and a memory limit of 2 GiB. The results are summarized in Tab. 1, where Zenon extended to arithmetic 9 is compared to two first order automated theorem provers able to deal with arithmetic and the TPTP input formats, i.e. Princess casc-2014-07-04 [START_REF] Rümmer | A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic[END_REF] and Beagle 0.9 (2/7/2014) [START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF]. The execution time for a prover is the sum of the user and system times taken by the prover, i.e the total CPU time used by the process and its children. As can be observed, Zenon is able to prove less problems than Princess and Beagle, but it is noticeably faster over the problems that it succeeds in proving, while proving a reasonable amount of problems. This trend can be seen in Fig. 5, which presents the cumulative times of the provers according to the numbers of proved problems. To obtain the curve for each prover, we consider its run times over all the problems that it proves, sort these times in increasing order, and then plot the cumulative sum of these times. The speed of Zenon is confirmed by the times computed w.r.t. the problems that are proved by all the tools (labeled with "(2)" in Tab. 1). These times show that the time difference between Zenon and the other provers is not due to the other provers taking more time over the problems that are not proved by Zenon, but rather because Zenon is typically faster over the problems that are proved by all the tools.

If we exclude the problems involving alternation of quantifiers, the typical problems not proved by Zenon actually make use of uninterpreted functions. This is due to the lack of exchange of information between the arithmetic extension and the rest of the proof search rules (the equality rules in particular). In fact, the non-trivial arithmetic proof search rules are only applied when the simplex detects an unsatisfiable system, which prevents the propagation of potentially relevant information to other parts of the proof search algorithm.

In the framework of the BWare project [START_REF] Delahaye | The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations[END_REF][START_REF]The BWare Project[END_REF], this extension of Zenon to arithmetic has been integrated to another extension of Zenon, called Zenon Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF], which extends Zenon to deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF]. Zenon Modulo extended to arithmetic has been benchmarked over a set of 12,876 proof obligations coming from the development of industrial applications using the B method [START_REF] Delahaye | The B-Book: Assigning Programs to Meanings[END_REF] and requiring high integrity. It has allowed us to go from 10,340 proved problems (without the extension to arithmetic) to 12,281 proved problems (with the extension to arithmetic), and obtain an increase of almost 20%. This shows that our implementation is scalable, and effective for program verification in particular. Zenon is a certifying automated theorem prover in the sense that it is able to produce proofs checkable by external tools, such as Coq [START_REF]Coq, version 8.4pl6[END_REF] for example. This Coq backend has been extended to support the addition of the arithmetic proof search rules. The main challenge was to translate the implicit rewriting steps that are performed over the arithmetic formulas in the proof search rules. Using this extended backend, all the proofs found by Zenon for the problems of the ARI category have been successfully produced by Zenon and checked by Coq.

Related Work

The closest work from our approach is probably the one of the Princess automated theorem prover, which integrates the Omega test [START_REF] Rümmer | A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic[END_REF] with a tableau-based proof search method. Compared to our work, Princess offers a complete procedure for integer problems involving purely universal and purely existential formulas. In our case, we do not ensure this property in the case of purely universal formulas, as we do not use global bounds, which appear to be ineffective in practice. Moreover, Princess proposes a better integration of arithmetic with the other proof search rules, as it is able to deal with uninterpreted predicates (and also with uninterpreted functions by extension). However, compared to Princess, we provide a more efficient implementation (as pointed out by the experimental results of Sec. 6), which is partly due to the fact that the simplex method is more efficient than the Omega test in practice. But the main difference is that our approach is proof producing along the lines of what is proposed in [START_REF] Barendregt | Autarkic Computations in Formal Proofs[END_REF], which allows us to increase the level of confidence in our implementation.

Arithmetic is also the area of expertise of SMT solvers. A large part of them, such as CVC4 [START_REF] Barrett | CVC4[END_REF] or Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF], proposes linear (and also non-linear for some of them) arithmetic as a built-in theory, as well as very efficient implementations. Compared to SMT solvers, we offer a better support for the first order layer of arithmetic problems, as SMT solvers relies on pattern-matching (controlled by a system of triggers) rather than unification to deal with instantiation, which is not complete in general. In addition, our experimental results (see Sec. 6) let us hope that our implementation could compete, in terms of time, with some of the most efficient SMT solvers, even though no experiment has been realized yet. Finally, as mentioned previously, our implementation is able to produce proofs, which is not the case of most SMT solvers.

Conclusion

In this paper, we have proposed an extension of the Zenon tableau-based first order automated theorem prover to linear arithmetic. This extension relies on the general simplex algorithm to deal with rational systems, as well as on the branch and bound method to deal with integer systems. This extension has been implemented, and this implementation appears to be quite efficient compared to similar first order automated theorem provers, as pointed out by the experimental results over arithmetic problems coming from the TPTP library, and even though it is able to prove less problems than these other provers. As shown by the tests over the benchmark of the BWare project, this implementation also appears to be scalable. In addition, this implementation includes an extension of the Coq backend of Zenon as well, which allows us to produce Coq proofs from arithmetic automated proofs.

As future work, we plan to investigate the introduction of Gomory's cuts [START_REF] Gomory | An Algorithm for Integer Solutions to Linear Problems[END_REF], which reduce the search space, and which appear to be very effective in combination with the branch and bound method (called the branch and cut method in this case), even though we think that it would require to complicate the explanation procedure. We also aim to realize a better integration of arithmetic with the other parts of the proof search method, in particular to deal with arithmetic formulas involving uninterpreted functions and predicates, even though our implementation is already able to prove difficult problems in this domain (see the problem ARI619=2 with a TPTP ranking of 0.7810 for example). Finally, we would like to consider mixed problems (involving expressions of distinct arithmetic types) and non-linear arithmetic, which would allow us to deal with all the problems of the arithmetic category of TPTP (i.e. 557 problems).

Fig. 1 .

 1 Fig. 1. Proof Search Rules of Zenon

  Const k = k Const where k and k are numeric constants Normalization Rules e = e Eq e ≤ e , e ≤ e e = e Neq e < e | e > e ¬e e Neg e e e < f Int-Lt e ≤ f -1 e > f Int-Gt e ≥ f + 1 where e and f are integer expressions Simplex Rules e c Var s fresh s = e, s c

Fig. 4 .

 4 Fig. 4. Proof of Formula 1

Fig. 5 .

 5 Fig. 5. Cumulative Times according to the Numbers of Proved Problems

Table 1 .

 1 It may differ from the real Experimental Results over the ARI Category of TPTP time for provers that use more than one thread, which is the case of Princess and Beagle. The total and average times labeled with "(1)" are computed w.r.t. all the problems, i.e. 500 problems. The total time for a given prover only considers the set of problems that the tool succeeds in proving, i.e. the problems over which the prover reaches the timeout are not included in the total time. The average time is computed as the total time divided by the number of proved problems. The total and average times labeled with "(2)" are computed w.r.t. the problems that are proved by all the tools, i.e. 453 problems.

	Prover	Proofs	Rate	Total (1) Time (s)	Average (1) Time (s)	Total (2) Time (s)	Average (2) Time (s)
	Zenon (arith.)	459	92%	23.33	0.05	23.08	0.05
	Princess	491	98%	2129.20	4.34	2048.20	4.52
	Beagle	495	99%	678.62	1.37	596.53	1.32

We use the notation e = e as syntactic sugar for ¬(e = e ).

For reals, numeric constants are represented as arbitrary precision rationals.

If f is the empty sum, then the comparison is either trivially false, in which case the system if unsatisfiable, or a tautology, in which case it is useless.

The termination of the simplex method is ensured using Bland's rule (see[START_REF] Dutertre | Integrating Simplex with DPLL(T)[END_REF]).

The new state of the simplex is of no use in this case, as if a system is unsatisfiable, then adding new equalities or bounds will not change anything to its satisfiability.

We therefore represent real numeric constants using arbitrary precision rationals.

It means that at least 78% of the tested automated theorem provers fail in proving the considered problem.

This work is supported by the BWare project [9,17] (ANR-12-INSE-0010) funded by the INS programme of the French National Research Agency (ANR). 7 This approach also handles formulas that are negations of purely universal arithmetic formulas, where all the variables are universally quantified. 8 See: https://forge.ocamlcore.org/projects/zarith/.

https://www.rocq.inria.fr/deducteam/ZenonArith/.


domain: info.info-au math spi

text:
Pierre Bernhard

Pursuit-Evasion Games and Zero-sum Two-person Differential Games

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Historical perspective

The history of Differential Games (DG in short) starts with Rufus Isaacs, who coined the phrase in his pioneering work of the early '50's [START_REF] Isaacs | Games of pursuit[END_REF], which was largely ignored until the publication of his book [START_REF] Isaacs | Differential Games, a Mathematical Theory with Applications to Optimization, Control and Warfare[END_REF]. Through the investigation of particular problems, Isaacs invented by himself (with his own names) the concepts of state and control variables, of feedback, his "tenet of transition" -better known as Bellman's optimality principle-, the (Hamilton-Jacobi-Caratheodory-)Isaacs equation, barriers, some difficult corner conditions ("equivocal lines"), singular arcs ("universal lines"), etc.

Another very early work was Kelendzerize's chapter "A Pursuit Problem " in the historical book by Pontryagin et al [START_REF] Pontryagin | The Mathematical Theory of Optimal Processes[END_REF], but it lacked closed-loop strategies.

John Breakwell and a few followers [START_REF]Lecture notes[END_REF][START_REF] Breakwell | Toward a complete solution of the homicidal chauffeur game[END_REF] picked up Isaacs' work where he had left it, still working on particular problems, but adding the power of the computer to analyze the solution of Isaacs' equation via the structure and singularities of fields of extremal trajectories, while most of the literature concentrated on making precise the concepts of closed-loop strategies and of Value of the game. Prominent figures in that quest are N. Krasovskii and A.I. Subbotin [START_REF] Krasovskii | Jeux Différentiels. MIR[END_REF], W. Fleming [START_REF] Fleming | The convergence problem for differential games[END_REF], A. Friedman [START_REF] Friedman | Differential Games[END_REF], A. Blaquière, F. Gérard and G. Leitmann [START_REF] Blaquière | Quantitatve and Qualitative Games[END_REF], Eliott and Kalton [START_REF] Elliot | The existence of value in differential games of pursuit and evasion[END_REF] and E. Roxin [START_REF] Roxin | The axiomatic approach in differential games[END_REF] and P. Varaiya [START_REF] Varaiya | Existence of saddlepoint in differential games[END_REF] who together invented the concept of non-anticipative strategies.

The major later innovation was Crandal and Lions' viscosity solutions of PDE's [START_REF] Lions | Generalized Solutions of Hamilton-Jacobi Equations[END_REF][START_REF] Crandal | Viscosity solutions of Hamilton Jacobi equations[END_REF] applied to DG's and its Isaacs equation by Evans and Souganidis [START_REF] Evans | Differential games and representation formulas for solutions of Hamilton-Jacobi-Isaacs equations[END_REF][START_REF] Lions | Differential games, optimal control, and directional derivatives of viscosity solutions of Bellman's and Isaacs' equations[END_REF].

We also refer the reader to the article [START_REF] Quincampoix | Differential games[END_REF] of another Springer Encyclopaedia.

General set-up

We shall be interested in (continuous time) two-person zero-sum DG's with complete information, this last phrase meaning that both players know exactly and instantly the state of the system, but (usually) not their opponent's control. The available space of a short article does not allow us to attempt to give the most general set-up of a zero-sum two-person perfect-information Differential Game. We shall therefore concentrate on a typical class, with a finite dimensional state space, as follows. The data are:

1. A two-player dynamical system with state x ∈ R n , control variables u ∈ U ⊂ R , v ∈ V ⊂ R m (U and V will often be assumed compact) and its dynamics

ẋ = f (t, x, u, v) , x(t 0 ) = x 0 .
Denoting U and V the sets of measurable functions from R to U and V respectively, one assumes regularity and growth conditions on f to guarantee existence and uniqueness of the solution x(•) for all (t 0 , x 0 ), and all (u(•), v(•)) ∈ U × V.

2. A termination condition, often given by a target set T ∈ R × R n , open or closed according to necessity, defining a final time as

t 1 = inf{t | (t, x(t)) ∈ T }. If T = {T } × R n ,
(u(•), v(•)) = Γ(t 0 , x 0 ; φ, ψ) ∈ U × V.
4. A performance measure, or pay-off, typically

J(t 0 , x 0 ; u(•), v(•)) =    K(t 1 , x(t 1 )) + t1 t0 L(t, x(t), u(t), v(t)) dt if t 1 < ∞ , ∞ if t 1 = ∞ .
We let G(t 0 , x 0 ; φ, ψ) := J(t 0 , x 0 ; Γ(t 0 , x 0 ; φ, ψ)) .

A concept of "solution"

, where the first player wants to minimize the performance index while the second one wishes to maximize it. (In our choice of definition of J, we have assumed that player one wants over anything else to make the game terminate. If we define J as the integral even for infinite end-time, Isaacs' tenet of transition may not hold).

If

inf φ∈Φ sup ψ∈Ψ G(t 0 , x 0 ; φ, ψ) = sup ψ∈Ψ inf φ∈Φ G(t 0 , x 0 ; φ, ψ) = V (t 0 , x 0 ) ,
then V is called the Value function of the game. Several concepts of upper Value and lower Value may be defined (including the first and second terms above) that have to coincide for a Value to exist.

Isaacs' condition

In the framework of this short article, we shall always assume that the game satisfies Isaacs' condition. It bears on the hamiltonian H(t, x, p, u, v) := L(t, x, u, v) + p, f (t, x, u, v) and reads

∀(t, x, p) ∈ R × R n × R n , inf u∈U sup v∈V H(t, x, p, u, v) = sup v∈V inf u∈U H(t, x, p, u, v) . (1)

Strategies and Value

In pursuit-evasion games, the concept of closed-loop strategies is of the essence, and it is extremely important for all DG's. Yet, allowing state feedback strategies such as Isaacs' K-strategies were a partial attempt to address this issue. More developed concepts were proposed, from limit of piecewise constant, or piecewise open-loop, controls (Fleming [START_REF] Fleming | The convergence problem for differential games[END_REF], Friedmann [START_REF] Friedman | Differential Games[END_REF]) to extensions of the notion of solution of a differential equation (Krasovskii,[START_REF] Krasovskii | Jeux Différentiels. MIR[END_REF]), also proving the existence of a Value. The equivalence of all these Values was an issue until the advent of viscosity solutions of Isaacs' equation.

u(t) = φ(t, x(t)), v(t) = ψ(t,
A tool used to accommodate state-feedback strategies [START_REF] Bernhard | Singular surfaces in differential games, an introduction[END_REF] is Lemma 1 (Berkovitz) If V ⊂ Ψ, then, ∀φ for which this expression is well defined,

sup ψ∈Ψ G(t 0 , x 0 ; φ, ψ) = sup v(•)∈V G(x 0 , t 0 , φ, v(•)) .
As a consequence, a saddle-point (φ , ψ ) solution is defined by As far as the existence of the Value is concerned, the problem for a large class of DG's is solved with non-anticipative strategies defined as Φ :

∀u(•) ∈ U, ∀v(•) ∈ V G(t 0 , x 0 ; φ , v(•)) ≤ V (t 0 , x 0 ) ≤ G(t 0 , x 0 ; u(•), ψ ) , (2)
V → U such that ∀t , [∀s < t v 1 (s) = v 2 (s)] ⇒ [φ(v 1 (•))(t) = φ(v 2 (•))(t)] ,
and likewise for Ψ, (notice that for this concept of strategies, (2) is the natural formulation of a saddle point), and with the notion of viscosity solution of Isaacs' equation. See theorem 1 below.

Games of pursuit evasion

An important class of DG's are games of pursuit-evasion. Typically, in these games the state x is composed of a sub-vector y of Pursuer state(s) and a sub-vector z of Evader state(s). The dynamical function f is separated likewise, the dynamics of the Pursuer depending on the Pursuer's control(s) and that of the Evader on the Evader's control(s). Typically, the pay-off is time until capture defined as (t, x(t)) ∈ T (the target is often called capture set). This form of DG automatically satisfies Isaacs' condition (1).

Qualitative game

In pursuit-evasion games, the main issue is to distinguish initial states, called capturable, for which a Pursuer's strategy causing finite-time capture against any defense exists, from those, called safe, for which the Evader has a strategy guaranteeing escape against any defense. This is the topic of the qualitative game or game of kind (Isaacs). A theorem of the alternative is one which states that for a particular (class of) game(s), every initial state is either capturable or safe. Such theorems have been proved for classes of Pursuit-Evasion games covering essentially all cases of interest, under Isaacs condition (1) with L = 0. (Krasovskii [START_REF] Krasovskii | Jeux Différentiels. MIR[END_REF], Cardaliaguet et al. [START_REF] Cardaliaguet | A differential game with two players and one target[END_REF][START_REF] Cardaliaguet | Pursuit differential games with state constraints[END_REF].)

Capturable states are separated from safe states by a barrier, a piecewise smooth manifold which has to be semi-permeable. This means that for all (t, x) on the barrier where this barrier is a smooth manifold with normal ν(t, x), it should hold that

min u∈U max v∈V ν(t, x), f (t, x, u, v) = max v∈V min u∈U ν(t, x), f (t, x, u, v) = 0 .
A minimax pair (u, v) = ( φ(t, x, ν), ψ(t, x, ν)) is called a pair of semipermeable strategies. If the boundary of the capture set is a smooth manifold with local outward normal n(t, x), its usable part is the region where inf u∈U sup v∈V n(t, x), f (t, x, u, v) < 0. The natural barrier is a semi-permeable manifold constructed backward from its boundary (the BUP), with n as final ν and using the characteristic equations:

ẋ = f (x, φ, ψ) , νt = -ν t ∂f (t, x, φ, ψ) ∂x .
(These trajectories are abnormal trajectories of the calculus of variations.) In most examples, only part of the manifold thus constructed is a barrier, and the complete barrier is made of manifolds pieced together according to a junction condition insuring that the corners "do not leak" (Breakwell), analogous to the corner conditions of the next section.

Quantitative game

The quantitative game, or game of degree (Isaacs), is played inside the capture zone, typically with time of capture as the pay-off. It is ruled by Isaacs' equation in a fashion similar to that of games of finite duration (see below). Yet, the interplay between the qualitative and the quantitative game may be quite subtle, and plays a prominent role in determining the actual capture zone. The Value function is usually discontinuous across other barriers inside the capture zone..

Other approaches

Other approaches have been developed to solve games of pursuit-evasion. An early approach by Pontryagin [START_REF] Pontryagin | Linear differential games I and II[END_REF], extended by Pshenichnyi [START_REF] Pshenichnyi | Linear differential games[END_REF], used geometric methods for linear pursuit-evasion games with convex compact controls sets. Krasovskii's stable bridges [START_REF] Krasovskii | Jeux Différentiels. MIR[END_REF] are a concept close to Isaacs' semi-permeability. Patsko and Turova [START_REF] Patsko | Level sets of the value function in differential games with the homicidal chauffeur dynamics[END_REF] have developed, for some families of DG's, an efficient numerical procedure to compute recursively hypersurfaces of constant time-to-capture, whose discontinuities display the barriers. Cardaliaguet, Quincampoix and Saint-Pierre [START_REF] Cardaliaguet | Set-valued numerical methods for optimal control and differential games[END_REF] have developed a theoretical and numerical procedure building on Aubin's viability theory, which requires less regularity on the data than other approaches.

Provided that care be applied, a quantitative game may be transformed into a family of qualitative games -an approach used by Krasovskii, Blaquière et al. and Cardaliaguet et al.-, and conversely, a fruitful approach is to investigate capturability of initial states as a function of a parameter defining the "size" of the capture set, imbedding the qualitative game into a quantitative game of the type game of approach.

Games of finite duration

Wherever termination of the game is not an issue, the major tool in investigating a DG is Isaacs' equation, a partial differential equation bearing on the Value function:

∀(t, x) / ∈ T , ∂V ∂t (t, x) + min u∈U max v∈V H(t, x, ∇ x V, u, v) = 0 , ∀(t, x) ∈ T , V (t, x) = K(t, x) . (3)
For any DG where all trajectories are transverse to the boundary ∂T , and with adequate regularity conditions on the data (and still under condition 1), it holds that Theorem 1 The DG has a Value in nonanticipative strategies, which is the only bounded, uniformly continuous viscosity solution of the equation obtained by changing signs in (3) as -∂V /∂t -min u∈U max v∈V H = 0. And all other Values coincide.

One possible way to solve Isaacs' equation is via the investigation of its field of characteristics. Their equations are Isaacs' retrograde path equations : let (û, v) = ( φ(t, x, p), ψ(t, x, p)) be the saddle point of H(t, x, p, u, v), assumed here to be unique, one integrates from the target set backward

ẋ = f (t, x, û, v) , (4) ṗ
= - ∂H(t, x, p, û, v) ∂x t . (5)
The above equations are similar to Pontryagin's maximum principle equations. However, a major difference lies in the corner conditions. While Pontryagin's theorem extends to control theory the Erdman-Weierstrass condition stating that the adjoint vector (here p) is continuous along an extremal trajectory, in (4)-( 5), p is to coincide with ∇ x V , and may be discontinuous along an extremal trajectory. These discontinuities cannot be found by a local analysis along an isolated trajectory, and require that a complete field of extremals be constructed, synthesizing a state feedback strategy. The analysis of the conditions that hold at such corners : equivocal manifolds (Isaacs), envelope manifolds (Breakwell), focal manifolds (Merz), has been a large part of the early, Isaacs-Breakwell, theory. It has been for its larger part synthesized by Bernhard [START_REF] Bernhard | Singular surfaces in differential games, an introduction[END_REF], except a general constructive analysis of focal manifolds which had to wait until [START_REF] Melikyan | Geometry of optimal trajectories around a focal singular surface in differential games[END_REF].

The absence of a "two-sided Pontryagin principle" for closed-loop Differential Games forces one to resort to the solution of Isaacs' equation, or an equivalent. This is the reason why no practical method of solution exists beyond a state dimension of 3 or 4, counting time if the game is not time-invariant. An exception is the linear quadratic game. (See that article.)

Conclusion

Except for very particular games, "solving" a DG remains a difficult task. Numerical methods suffer the famous "curse of dimensionality". Moreover, many of them strive to compute the Value function. But the optimal strategies typically depend on the gradient of the Value function, requiring a stronger convergence of the approximation algorithms than pointwise, or C 0 or L 2 , if they are to be computed as well. Further advances in numerical algorithms tackling this problem would be useful, as well as uncovering new classes of DGs for which further analytical results could be obtained.

  confronting the closed-loop saddle point strategies to open-loop controls only. (This proves useful in the analysis of Nash equilibria of nonzero-sum DG's.) Another consequence of Berkovitz' lemma is that if a DG has a saddle point in open-loop controls, it is a saddle point over closed-loop controls as well. (But the existence condition may be less stringent for the later.) The relationship between different forms of the strategies has been further clarified by Bas ¸ar [1, 2].

  final time is fixed and equal to T . The question of whether there is a finite t 1 is one of central interest in pursuit-evasion games.

	3. Sets of admissible closed-loop strategies Φ and Ψ. One should choose them in such a
	way that, replacing (u, v) by a pair (φ, ψ) ∈ Φ×Ψ in the dynamics always produces a
	(unique) admissible pair of control functions

  x(t)), poses a difficult problem : what classes Φ and Ψ of functions φ and ψ to allow ? The notations inf φ or sup ψ have no meaning if one does not answer that question. Experience tells us that discontinuous feedbacks are necessary to find the solution of many examples, but then existence, or uniqueness, of the solution of the dynamical equation cannot be guaranteed.