Virtual Substitution & Real Equations

Synopsis

This chapter investigates decision procedures for real arithmetic, which serve as an important technology for proving the arithmetic questions that arise during cyber-physical systems analysis. The fact that first-order properties of real arithmetic are even decidable is one of the big miracles of logic on which CPS analysis depends. While a blackbox use of quantifier elimination often suffices, this chapter looks under the hood to understand why and how real arithmetic can be decided. This leads to a better appreciation of the working principles and complexity challenges in real arithmetic. The focus in this chapter will be on the case of linear and quadratic equations, which conceptually elegant virtual substitution techniques handle.