Quasi-decidability of a Fragment of the First-order Theory of Real Numbers

TL;DR

This paper introduces a semi-decision procedure for a fragment of the first-order theory of real numbers involving continuous functions, which guarantees correct answers upon termination and always terminates for robust formulas, leveraging topological degree.

Contribution

It presents a novel semi-decision algorithm for a specific undecidable fragment, ensuring correctness and termination for robust formulas using topological degree.

Findings

Algorithm always produces correct answers when it terminates.

Algorithm terminates for all robust formulas.

Uses topological degree as a key tool in the decision process.

Abstract

In this paper we consider a fragment of the first-order theory of the real numbers that includes systems of equations of continuous functions in bounded domains, and for which all functions are computable in the sense that it is possible to compute arbitrarily close piece-wise interval approximations. Even though this fragment is undecidable, we prove that there is a (possibly non-terminating) algorithm for checking satisfiability such that (1) whenever it terminates, it computes a correct answer, and (2) it always terminates when the input is robust. A formula is robust, if its satisfiability does not change under small perturbations. As a basic tool for our algorithm we use the notion of degree from the field of (differential) topology.