24th Conference on Applications of Computer Algebra

Santiago de Compostela, June 18-22, 2018

Invited plenary speakers

• James H. Davenport

  University of Bath, United Kingdom

Applications of Computer Algebra to Verification and Satisfiability Checking

Boolean Satisfiability Checking is one of the paradoxes of computer science: on the one hand it (as 3-SAT) is the quintessential NP-complete hard problem, on the other hand, problems with millions of instances are solved routinely. If we ask for (semi-)algebraic satisfiability over thre als, the quantified worst case complexity becomes doubly exponential. While computer algebraists wrestle with this complexity, the Satisfiability Modulo Theories community has been working away pragmatically, using very different success criteria, and applying their techniques, especially in software and system verification. However, they could learn more from Computer Algebra, and we could learn from them. This talk will outline some of these directions.

• Vijay Ganesh

  University of Waterloo, Canada

SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics

In recent years we have witnessed a dramatic improvement in the performance of Boolean SAT solvers, despite the fact that the Boolean satisfiability problem is NP-complete [1, 2]. While SAT solvers are powerful combinatorial search algorithms, they are weak when it comes to domain-specific mathematical knowledge. On the other hand, computer algebra systems (CAS) are deep repositories of mathematical knowledge and contain many sophisticated mathematical algorithms. However, computer algebra systems are not as strong at combinatorial search as SAT solvers. Motivated by problems that require both powerful search and deep knowledge, we propose a SAT+CAS combination method that brings together the best of both these worlds aimed at solving problems in combinatorial mathematics.

In this talk I will present a SAT+CAS system, MathCheck [3, 4], that we developed and used to counterexample many combinatorial conjectures, most notably the Williamson conjecture. I will discuss the internals of MathCheck, how it can be used, and most importantly, how mathematicians can extend such SAT+CAS tools to tackle a variety of problems. I will also argue that we are witnessing a new long-term paradigmatic shift, wherein, previously unrelated methods such as solvers and CAS are being profitably combined to tackle hard mathematical problems.

 

• Laureano González-Vega

  University of Cantabria, Spain

Dealing with real algebraic curves and surfaces for discovery: from experiments to theory and applications.

Geometric entities such as the set of the real zeros of a bivariate equation or the image in of a rational parametrization   can be treated algorithmically in a very efficient way by using a mixture of symbolic and numerical techniques. This implies that it is possible to know exactly which is the topology (connected components and their relative position, connectedness, singularities, etc.) of such a curve or surface if their equations are known in an exact manner (whatever this means) for moderate or high degrees. We would describe several different "experiments" coming from Algebraic Geodesy and Computer Aided Design that highlight how new visualisation tools in Computational Mathematics mixing symbolic and numerical techniques allow to perform experiments conveying either to mathematical discoveries and/or to new computational techniques useful in applications. 

• Dingkang Wang

  Chinese Academy of Sciences, People's Republic of China

Automatic Geometric Theorem Proving and Discovering using (Comprehensive) Groebner Bases

Automatic geometric theorem proving and discovering is to prove and derive mathematical theorems by computer programs, which has been studied for several decades. It can be traced back to the great work of Tarski, Seidenberg, Gelernter, Collins, Wu and so on. The extensive study in this research field is due to the introduction of Wu's method in later 1970s, which is surprisingly efficient for proving difficult geometric theorems. 

In this talk, I will firstly introduce our work on discovering geometric theorems by using the comprehensive Groebner systems, i.e. finding some complementary conditions such that the geometric statement will become true under the original hypotheses and these complementary conditions. Particularly, efficient algorithms for computing comprehensive Groebner systems/bases are also reviewed. Secondly, I will investigate the problem whether the conclusion is true on some components of the hypotheses for a geometric statement.  In that case, the affine variety associated with the hypotheses is reducible. A polynomial vanishes on some but not all the components of a variety if and only if it is a zero divisor in a quotient ring with respect to the radical ideal defined by the variety. Based on this fact, we present an algorithm to decide if a geometric statement is only true on components. Besides proving theorems, the parametrical extension of this method can also be used to discover new geometric theorems. That is, we can find out complementary conditions such that the geometric statement becomes true or true on components. Some illustrative examples will be presented to show how the method  works.

(This is joint work with Deepak Kapur, Yao Sun and Jie Zhou)