# Invited Talks

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.

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 ?

Abstract: This talk will focus on two separate topics. The first one concerns the geometry of point-reflections, and the various axioms that one can add to an axiom system for point-reflections valid in absolute geometry to get a hierarchy of geometries that are intermediate between absolute an affine geometry. The dependencies and independencies involved were all established with the aid of Tipi, an aggregate of automatic theorem provers designed by Jesse Alama. Several open problems remain.

The second part is a walk through results known to be true, regarding statements that are known to be equivalent to established axioms, but for which we have only algebraic proofs, or even proofs using Tarski's principle and other deep model-theoretical results. The challenge would be to find syntactic proofs by means of automatic theorem provers. Examples are: Szmielew's proof that the circle axiom implies the Pasch axiom in a certain axiom system for semi-ordered Euclidean geometry, the fact that the Erdos-Mordell theorem is equivalent to the statement that the angle sum in a triangle is not larger than two right angles, the equivalence of Lagrange's axiom with Bachmann's Lotschnittaxiom.