Bi-Weekly Talk: Jasper Nalbach: A Compositional Proof System for Cylindrical Algebraic Decomposition

Wednesday, January 24, 2024, 10:30am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: Jasper Nalbach

 

Abstract: 

Cylindrical algebraic decomposition (CAD) is the only complete method implemented in Satisfiability-modulo-theories solvers for solving non-linear arithmetic. Due to its doubly exponential complexity, modern algorithms compute only parts of its projection operation, making solving some practical instances of NRA tractable.

There is a variety of cases where savings in the projection are possible, and often there are multiple alternatives for the projection.

To manage the maintainability of an algorithm when incorporating special cases, we developed a proof system for modern CAD-based SMT algorithms.

This proof system is extensible, separates heuristic decisions (which projection to take) from the correctness of the projection and can be employed in different algorithms. Further, the proof system could be a step towards formal proofs for real algebra.