Team IGG : Computer Graphics and Geometry

Specifications, Constraints and Proofs in Geometry

From Team IGG : Computer Graphics and Geometry
Jump to navigation Jump to search

Objectives / Challenges

Even if it can appears scattered, our problematic is quite focused. The core of our research is about the issue of proof in geometry in relation with computer science. We study this question from the fundations of geometry revisited with the proof assistant Coq to various fundamental applications such as geometric constraint solving, specification and proof of algorithms in computational geometry, computer aided education and planification in percutaneous surgery. In these domains, we developped several pieces of software like geometric solvers and provers, a whole framework for percutaneous surgery and stereotactic neurosurgery, Coq tactics to mechanize tedious parts in geometric proofs.

The main goal of our studies consists in providing user oriented tool helping him to formally specify geometric problems and to construct a formal proof by using automatic provers and solvers.


Participants

Results

Formalization and theorem proving in geometry

main publications (to be used in the text)

With Laurent Fuchs, University of Poitiers and Agathe Chollet, University of La Rochelle, we have been working on the formalization using Coq of a discrete model of the continuum based on non-standard analysis: the Harthong-Reeb line 2-MCF15. We established, on the one hand, that the axiom system describing this line verifies Bridges axioms and, on the other hand, that its implementation based on Laugwitz-Schmieden integers allows to perform efficient computations. We applied these results to simple problems in the field of discrete geometry. We then investigated how to use the Harthong-Reeb line to describe linear real transformations by using sequences of linear rational transformations 5-ADFL14.

Specification, proofs of algorithms and implantation

This subject comes downstream of the previous theme and is strongly related to it. We worked on modelling in Coq useful data structures and algorithms for topology and geometry 2-DD14. Indeed, reliability is of paramount importance when dealing with computational geometry algorithms. However issues related to specifications and formal certification have not been studied extensively yet. We proved some results of convex hull computations in the plane 2-BDM12 and on the incremental construction of Voronoï diagrams where cells are described using topological models such as those developed in CGoGN. In this specific case, we formally proved the correction of the implementation in an imperative language featuring pointers 4-Dufo14 4-Dufo14a 2-Dufo15.

Specification and resolution of geometric constraints

In the last few years, we studied various aspects of geometric constraint solving. We got striking results in the three following domains:

  • Specification: we propose new algorithms to translate CAD geometric problems into constraint systems thanks to the distance geometry. These algorithms are more efficient than the ones used in CAD or structural chemistra [4-MS13, 2-MS14a].
  • Numerical resolution: Rémi Imbach's thesis was devoted to the study of methods able to guide homotopic methods by using geometry. We obtained new results both in terms of efficiency and stability [4-MSI12,2-ISM14, 8-Imba13].
  • Symbolic resolution: we also tackle the issue of straightedge and compass constructibility which arises in educational domain. Using algebraic tools, we develop algorithms to automatically check RC-(un)constructibility of problems in Wernick's and Connelly's corpora [4-MJS15, 2-SMxx].


Illustration, problem W108 (Wernick): compass and ruler construction of a triangle ABC when are known: the orthocenter, H, the foot Ta of internal bissector issued from A, and the center of [BC], Ma:

  • Geometric transcription of a solution algebraically found

  • Direct construction

Formalization and planning of surgical interventions

The works in this theme are at the interface of formalization and solving of geometric constraints, geometric modeling, optimization, and medical image processing. They find their applications in the automated assistance to decision making for preoperative planning and simulation of surgery. More particularly, the automatic computation of optimal and safe trajectories for percutaneous surgery and stereotactic neurosurgery.

During the past four years, the work was focused on :

  • Taking into account the deformability of the tissue, organs, and surgical tools in the trajectory computation, thanks to the inclusion of biomechanical simulations in the optimization loop ([2-HPCE16][4-HBDC15][4-BEDC12])
  • The optimization of multiple trajectories simultaneously taking into account interactions between multiple tools and their effects, and computing the resulting effect by thermal propagation ([2-JE15][4-JE14])
  • The precise definition and solving of geometric constraints for deep brain stimulation ([2-EHLA12]), accounting for anatomo-clinical data ([4-DZHJ14]), and definition of an automated preprocessing pipeline for brain images ([2-DHEF15][4-DHEF14]).
  • In-depth study of optimization parameters: weights of the constraints ([2-EFCH15][4-EMFB12]), and influence of the choice of the optimization technique (mono/multi-criteria) on the repartition and relevance of the results [4-HVCJ16].

  • Inclusion of biomechanical simulations in the optimization loop [2-HPCE16]

  • Constraint solving for deep brain stimulation electrode placement [2-EHLA12]

  • Thermal propagation computation for cryoablation [2-JE15]

  • Possible insertion points on a Pareto front [4-HVCJ16]

Perspectives

The Harthong-Reeb line offers one original perspective to describe in a simple manner algorithms in the field of discrete geometry. We shall use the Harthong-Reeb line and its formalism to represent real transformations as limits of sequences of rational transformations and study these properties under which assumptions they hold. This work will take place at both the mathematical level and the implementation level, writing algorithms in Coq in order to certify them.

Retrieved from "https://igg.icube.unistra.fr/en/index.php?title=Specifications,_Constraints_and_Proofs_in_Geometry&oldid=3945"