Automated Geometric Reasoning with Geometric Algebra: Theory and Practice

Slides

Abstract:

Traditional Euclidean styled proofs of geometric theorems have trained generation after generation of people for their ability of making mathematical logical reasoning. They may be hard to contrive, but once constructed, usually they exhibit a style of mathematical beauty: succinct and rigorous, readable and enlightening. In contrast, proofs out of Cartesian analytic approach are usually boring or even impossible to read as there may be polynomial manipulations involving hundreds of thousands of terms. Unreadable proofs are indeed verification, but are short of mathematical beauty, and have rather limited value in inspiring mathematical creativity.
Is there any algebraic language and associated algebraic operations to describe and manipulate geometric problems in a readable, understandable way, so that on one hand, the algebraic expressions may be relatively easy totranslate into geometric terms, on the other hand, the algebraic operations are simple and lead to short expressions? Such a class of algebraic language should be righteously called " Geometric Algebra", and the associated analytic geometry be called "Computational Synthetic Geometry".
In this tutorial we shall introduce two typical Geometric Algebras: Grassmann-Cayley Algebra and Conformal Geometric Algebra, and their applications in automated geometric theorem proving. We shall show how and why such quotients of real tensor algebra can lead to amazingly simple algebraic proofs: the size of the expression under manipulation can be preserved to two terms for most theorems in projective geometry, and even to one term for many theorems in Euclidean geometry involving nonlinear constructions.

Algorithmic Approaches for Lattice Path Combinatorics

Abstract:

Lattice paths are fundamental combinatorial classes and they appear in many guises in physics, queuing theory, language theory, and pure mathematics. New formulas for the asymptotic enumeration of walks restricted to a quadrant have appeared in the past ten years, mostly driven by novel systematic, and analytic approaches.
In this tutorial we will present the universe of lattice path classes, and survey some of the strategies used to deduce enumerative formulas. The generating functions for several models of walks in cones satisfy nice differential equations, and algorithms to find, manipulate, and solve differential equations have been central to this study. We will discuss how to express the generating functions as diagonals of multivariate rational functions, and how to reconcile the results of different approaches to this computation.

Lattice reduction algorithms

Slides

Abstract:

Lattice reduction aims at finding a basis consisting of rather short vectors, from an arbitrary basis. The importance of lattice reduction stems from the observation that many computational problems can be cast as finding short non-zero vectors in specific lattices (e.g., in computer algebra, cryptography, algorithmic number theory).
In this tutorial, we will give an overview of lattice reduction algorithms. We will consider both polynomial-time algorithms that find relatively short bases, such as the LLL algorithm, and more expensive algorithms that find shorter bases, such as the BKZ algorithm. The algorithms will be illustrated using the (freely available) fplll library.