Invited Talks

• Predrag Janicic, Faculty of Mathematics, University of Belgrade

Title: "Geometrization of Geometry"

Abstract: Coherent logic (CL) or geometry logic is a (semi-decidable) fragment of FOL that can be considered to be an extension of resolution logic. CL is suitable for formalization and automation of various mathematical theories, including geometry. This talk will give an overview of developments in geometry based on CL: automated theorem provers for CL, CL-based formalizations of geometry, CL-based proof representation for geometry, links between CL and geometry construction problems, links between CL and geometrical illustrations, etc.

• Dominique Michelucci, University of Bourgogne.

Title: Solving Constraints without Equations, Why and How

Abstract: Classically, when we solve geometric constraints, the latter are represented with mathematical equations, or inequalities. These equations or inequalities are represented explicitly, with trees or DAGs or polynomials, etc. So it is easy to symbolically compute derivatives, etc. It is possible to make proofs of geometric theorems.

But, recently, we meet more and more frequently problems for which equations are not available for many reasons, e.g. when the shape is the result of a procedure (subdivision surfaces; fractals ). In this new framework, shapes or geometric figures are the results of the evaluation of black box procedures / algorithms / subprograms, feed with some parameters. These programs contain if-then-else constructs, loops, they compute fixed points, they call ODE and PDE solvers. Some parameters are free : how to compute their values to satisfy specified constraints ? How to solve without equations ?