Specifications, constraints and Proofs
This theme deal with geometry formalisation to proove theorems, build figures or, more generally, geometric scenes, and to certify geometric algorithms.
More precisely, we focus on the formal definition of the geometric universe, proof of properties, automatic generation of geometric objects defined by a specification and deriving certified geometric algorithms. We work on computer science methods allowing to assist proofs, garanty the correctness and the feasibility and, when possible, to insure automatically some task using Coq tactics or, geometric constraint solving. The results of this researches can be exploited in geometric modeling, computational geometry, pure geometry, mathematics teaching and surgical planification.
During the last years, the research activity dealt with four fedarative different themes:
- Geometry formalisation and proofs of geometric theorems;
- Specification and proofs of geometric algorithms using combinatorial maps;
- Specification of figures and constraint solving;
- Formalisation and planification of percutaneous intervention for hepatic tumors removal and radiology intervention.
Permanents staff
- 2 Professors: Jean-François Dufourd and Pascal Schreck
- 4 Assistant professors: Caroline Essert, Nicolas Magaud, Pascal Mathis, Julien Narboux
Other participants
- 1 Associate researcher: Gabriel BRAUN (MC UFR LSHA, 09/2009-)
- 1 Delegated associate professor: Laurent FUCHS (MC Poitiers, 09/2010-09/2011)
- 3 Post-doctoral: Claire BAEGERT (ATER, 01/2010-08/2010), Christophe BRUN (ATER, 01/2011-08/2011), Simon THIERRY (ATER, 10/2010-08/2011)
- 1 PhD candidate: Rémi IMBACH (Ministry of Research grant, 10/2010-)
- 3 Former PhD candidates: Claire BAEGERT (Région Alsace-IRCAD, 10/2005-12/2009), Christophe BRUN (Ministry of Research grant, 12/2007-12/2010), Simon THIERRY (Ministry of Research grant, 10/2006-09/2010).
Formalisation and Theorem proving in geometry
We are interested in proof, automatic or computer assisted, in geometry. Among the classical researchs themes as, for example, ad hoc axiomatisations, foundations formalisations, algebric proofs or combinatorial proofs, we focus mainly on the formalisation and the extraction of axioms of geometric models.
To obtain robust geometric constraint solvers (see next section), we first focused on really simple geometry such as projective geometry of incidence. We first took an appropriate axiomatic framework to conceive automatic proovers based on fondamental incidence properties such as Desargues or Pappus configurations, the Pascal hexagram or matroid structures. We collaborated with D. Michelucci, PR from the University of Bourgogne to setup prototypes to allow automatic combinatorial proofs, i.e. which does not require any numerical computation, of alignments or coincidence.
We then worked on the foundations of incidence geometry. It constituted a part of the ANR project GALAPAGOS (2008-2011) on assisted proof in geometry. In this context, we specified and implemented in Coq some axiomatics to study projectives spaces (see 4-MNS08).
Among the obtained results, a complete formal proof in Coq of the Desargues theorem has been made using only matroid theory through the rank function notion to which we added properties linked to the dimension (the Desargues property becomes true in incidence geometry only from dimension 3) 4-MNS09. We currently work on other theorem in dimension 3, like the Beltrami theorem, in order to conceive a proof software for incidence geometry as complete as possible.
Concerning automatic proofs, Julien Narboux made the first formalisation in Coq of an automatic demonstration in geometry (the area method), it leaded to a collaboration with Pedro Quaresma and Predag Janicic in a reference publication on the method (2-JNQ10). This development has been integrated in an interactive proof environment in the dynamic geometry software GeoGebra (4-PBN11).
More fondamentally, we work in collaboration with Laurent Fuchs, assistant professor in the University of Poitiers, to formalize in Coq a discrete model of the continuous domain: the Hartong-Reeb line. This works could lead to an implementation of the continuous domain on computer 7-MCF10a. Later, we plan to proove formally the results on functions arithmetic and ellipse connectivity.
Finally, in a more pragmatic goal to have an efficient proover in euclidian geometry, we started work concerning the Coq certification of algebric methods based on the proof of belonging of a polynomial to an ideal and the Nullstellensatz of Hilbert. We started to study this problems with two classical methods: the Ritt-Wu method and a method using the Gröbner basis.
Specification, proofs of algorithms and implementation
This research considers modeling and geometric algorithmic through formal specification and assisted proof by computer. One part leans on geometric modeling using topology and space partition using combinatorial hypermaps, the other part leans on the inductive construction calculus and the Coq system of the INRIA. This way to tackle the problem has no equivalent. This work is a part of the ANR project GALAPAGOS (2008-2011) on assited proof in geometry. Through the topological aspects, it is tightly bounded to the theme "Modeling and Acquisitions" or the research group.
After a work with algebric specification, we did, since the 90s, formalized hypermaps and their derivative (combinatorial maps and generalized combinatorial maps) and built a Coq library on this structures. Formal proofs have been produce for great results in combinatorial topology : theorem of surface classification, theorem of the gender, Euler-Poincaré formula 2-Duf08a.
During the present quadriennal, we stated and proved the discrete Jordan curve theorem, giving a deconnexion criterion on hypermaps usefull to prove algorithms on hypermaps 4-Duf08b 2-Duf09. We proposed a functional algorithm for the segmentation of 2D picture using a pattern-matching on the inductive structure of the combinatorial maps describing the pictures. We proved its correctness in Coq and implemented an efficient imperative program (in C), which has been experimented on color pictures (2-Duf07).
We also studied problems linked to geometric algorithmic. Thus, we worked on algorithm for convex hull construction. Two versions has been studied and proved in Coq. The first one, using structural induction, leans on similar idea as the segmentation presented previously. The second one, using noetherian induction, simulate a traditional incremental algorithm. This proofs have been automatically extracted in Ocaml, and, the second version has been implemented in C++ and integrated to the CGoGN platform (Thesis work of C. Brun, advised by J.-F. Dufourd and N. Magaud 2-BDM11a 7-BDM11b).
An intensive work has been performed on the formalisation of subdivision surfaces, using merge and split operation on hypermaps cells. It has been treated on triangulated mesh with the classical definition of the edge flip. It lead to the first formalisation and proof of a Delaunay triangulation construction. This construction use rotations until all edges validates the Delaunay criterion. (Work of J.-F. Dufourd and Y. Bertot, head of the team Marelle of INRIA-Sophia 4-DB10).
Specification and constraint solving
The specification of data objects from their dimensions (functional dimension or manufacturing dimension) is an important issue in the field of design and computer aided design (CAD). It is closely related to the production of figures meeting the constraint system given by users. Since the 80s, several methods have been developed to solve geometrical constraint systems. There are three main approaches: numerical methods that solve iteratively equation systems, methods based on graph to make planning and the rule-based approach that solve systems constructively (ruler and compass construction). These latter lead to a formalisation of the geometry on which our team has always worked. There are also symbolic algebraic methods such Gröbner bases, but their complexity usually disqualifies them for CAD systems.
Two main features have guided the work of experts in the field in recent years:
- the large size and sparse character of constraint systems
- displacement invariance (or more generally by groups of transformations)
The first point has led teams interested in the decomposition of constraint systems and the second to reflect the displacement invariance in these decompositions. We then obtain special methods that do not necessarily resemble the methods of flow encountered in the methods of decomposition of equation systems.
These issues of invariance and decomposition have been theorized by our team (see MATH10), which helped to develop methods taking into account several groups. A implementation was made in the form of a multi-agent system that combine several different solvers. Moreover, a probabilistic approach has led us to suggest an incremental method to decompose constraint systems (work done in collaboration with Dominique Michelucci, MSTF10).
The problem of decomposition of geometric constraint systems often implies that the isolated subsystems are well-constrained modulo a given transformation group. Indeed, the classical solvers usually only manage systems with a finite number of solutions, possibly after quotiented the solution space by an equation related to the action of a transformation group. Unfortunately, many simple examples show that in 3D, the decomposition is no more convenient: most of the polyhedra are rigid and generically indecomposable. Therefore in the thesis of Arnaud Fabre, we were interested in a notion of quasi-decomposability in which we allow, in a first step, the change of the constraint system. Constraints removed in this step are then caught up by using a numerical method (see FASC07 and FASC08).
Following that approach led to consider under-constrained systems even when considering classical transformation groups (TSMF08 and TMS07). It was the issue addressed in the thesis of Simon Thierry (THIE10), whose purpose was to study under-constriction of constraint systems and their specific transformation groups. An original approach has also been established by Simon Thierry who can solve (in some sense) system constraints under or even over-constrained (see THIE11).
Formalisation and planning of surgical interventions
In these work, we propose an original approach to assist automatically the planning of a position of a surgical tool. Our method allows for elaborating an optimal strategy of intervention, specific to the patient and to the type of intervention, thanks to an automatic computation which is based on the expertise of the field and the preoperative data.
To this end, we put into play some approaches coming from declarative modeling and geometric constraint solving, to compute automatically optimal trajectories for rigid and straight surgical tools. The computation of the trajectory is performed in several steps. First, the expertise of the surgeon on a given type of intervention is transcribed under the form of mathematical equations (equalities, cost functions). Then those equations are formalized into geometric constraints, written under the form of terms combining geometric and arithmetic operators and the data coming from the medical images (MRI, CT). A first computation solves the so-called "strict" geometric constraints (boolean constraints) to provide the space of possible solutions. Finally a second computation solves the so-called "soft" geometric constraints called (numerical constraints) thanks to a numerical optimization, to provide the optimal solution.
We tested our approaches on 2 types of interventions : the ablation of hepatic tumors by radiofrequency (hyperthermia) in collaboration with Pr. Gangi from the service of radiology of the Hôpital Civil of Strasbourg, and the implantation of electrodes of deep brain stimulation in collaboration with Dr. Haegelen from the service of neurosurgery of Renne's University hospital Pontchaillou.
The PhD thesis of Claire Baegert dealt with this topic 8-Baeg09. Various papers were published regarding radiofrequency 4-EBS09, 2-BESS07, 4-BESS07, 4-BESS07b, 4-BESS07c and deep brain stimulation 4-EHJ10. These works also leaded to a collaboration with DKFZ Heidelberg on the acceleration of occlusions solving thanks to GPU 5-ESFR10, 2-SESR11.
These works gave rise to the ANR project ACouStiC, which started in january 2011 for 4 years, and in which IGG team is a partner. This research topic is part of the IHU of Strasbourg.
Perspectives
Formalisation and Theorem proving in geometry
We would like to study other fundamental theorems in incidence geometry such as the Beltrami theorem and to use these researches to design a certified prover for incident geometry.
Works on automatic generation of proof will be reinforces with the formalisation of algebric methods such as the Wu method. From the development view of the proof, we will use a method based on certificates. This thematic is shared with the INRIA Camus. Julien Narboux and Nicolas Magaud participates in the formal proof of parallel compilation of algorithm and program optimisation using polyedric models.
Finally, we combine our works concerning automatic theorem proofs and geometric constraint solving with the formalisation in Coq of this concepts. The goal is to generate certified constraint resolution algorithms and to broaden the domain of application of automatic demonstrations in geometry (all existing methods assume the existence of a geometric construction).
Specification, proofs of algorithms and implementation
The work on formalisation of combinatorial topological structure will be strengthened and amplified. The hypermap library will be extended to the dimension n to describe and manipulate the subdivision of nD spaces. Links will be established with current calculus algorithms on homology groups and manifolds of dimension n.
The experimentation of proofs in geometric algorithms will be continue. We will emphasize the work on the Delaunay triangulation and the Voronoï algorithm in dimension 3, which remain challenges when considering constraints. Numerical approximations will also be tackled. Until now, numerical approximations has been ignored and we only treated exact computation within the real domain. This position will have to be reevaluated, by examining different hypothesis : exact computation on rationals numbers, approximated computations by intervals, discrete geometry, etc.
Finally, the sophistication of our abstract hypermaps structures in practical structure in memory will have to be study. The translation of our abstract algorithm to imperative programs with pointers will be addressed, with a proof of correctness. A preliminary work on linear and cyclic structures already gave good results.
Specification and constraint solving
To solve geometric constraint systems, our team mainly worked on geometrical methods. Besides their ability to provide all the solutions, they offer a diagnostic failure. However, geometrical approaches fail in solving some specific 2D cases and many 3D problems.
We currently study reparametrization consisting in the transformation of a system S into a system S' that can be solved geometrically. Solutions of S are computed from solutions of S' with numerical methods. This current work addresses two problems. The first concerns the relationship between the transformation of a system and its decomposition in order to facilitate the numerical solving. The second concerns the adaptation of numerical methods based on all available geometric information (the sketch provided by the user, the construction plan produced by the resolution).
Besides this work, which attempts to combine the numerical methods used in industry and geometric method preferred by the academic world, we work on the implementation of a solver framework. This work is based on a description language for constraint systems, both their syntax as their semantics, initiated some years ago by the team.
Formalisation and planning of surgical interventions
Regarding surgical interventions planning, in the framework of ACouStiC project among others, we are beginning an extension of the field of possible solutions, by studying curved, multiple and volumetric trajectories. This will allow us to extend the posible applications to deformable surgical tools, within deformable tissues, or multiple tools used simultaneously (for instance cryoablation of hepatic tumors), or even access volumes such as craniotomy in the context of exeresis of cerebral lesions. We will also work on constrained surgical navigation within the solution space, in order to restrain the interactive modification of the proposed trajectory into a space of possible/reasonable solutions. To this end, the link will be done with "Visualization and interactions" axis of our team, in particular the haptic interfaces topic.