External links

Quasi-decidability of the first-order theory of real functions

GA21-09458S [Registered results] 2021 - 2024

Decision procedures for predicate logical theories play an increasingly important role in computer science, especially in combination with Boolean satisfiability solvers, that is, in SAT modulo theory (SMT) solvers. While there is a vast amount of current research on decision procedures for integers, real numbers, arrays, and many other theories, there is almost no results for the case of real functions, although such functions play a fundamental role in many areas of computer science and mathematics. We conjecture that the reason for this situation is the difficulty of the problem which we propose to overcome by designing so-called quasi-decision procedures for real functions. A quasi-decision procedure relaxes the decision problem in such a way that it is not required to terminate in borderline cases where the satisfiability of the input formula changes under small perturbations of this formula. In many applications, such borderline cases are actively avoided, and hence quasi-decision procedures can solve precisely those cases that are important in such applications.